Amphiteatre Maison Jean Kuntzmann
18 September 2015 - 10h00
Automated Verification of Exam, Cash, Reputation, and Routing Protocols (Phd Defense)
by Ali Kassem from Verimag
Abstract: Security is a crucial requirement in the applications based on information and communication technology, especially when an open network such as the Internet is used. To ensure security in such applications security protocols have been used.
In this thesis we contribute to security protocol verification with an emphasis on formal verification and automation. Firstly, we study exam protocols. We propose formal definitions for several authentication and privacy properties in the Applied Pi-Calculus. We also provide an abstract definitions of verifiability properties. We analyze all these properties automatically using ProVerif on multiple case studies, and identify several flaws. Moreover, we propose several monitors to check exam requirements at runtime. These monitors are validated by analyzing a real exam implementation using MarQJava based tool. Secondly, we propose a formal framework to verify the security properties of non-transferable electronic cash protocols. We define client privacy and forgery related properties. Again, we illustrate our model by analyzing three case studies using ProVerif, and confirm several known attacks. Thirdly, we propose formal definitions of authentication, privacy, and verifiability properties of electronic reputation protocols. We discuss the proposed definitions, with the help of ProVerif, on a simple reputation protocol. Finally, we obtain a reduction result to verify route validity of ad-hoc routing protocols in presence of multiple independent attackers.
Dear all,
It is my pleasure to invite you to the defense of my PhD thesis entitled
Automated Verification of Exam, Cash, Reputation, and Routing Protocols
in front of the following committee:
Sebastien Gambs Université de Rennes 1, INRIA
Steve Kremer Inria Nancy--Grand Est, LORIA
Pascal Lafourcade Université Joseph Fourier
Yassine Lakhnech Université Joseph Fourier
Olivier Pereira Université catholique de Louvain
Luca Vigano King's College London
You are also invited to the reception following the defense.
