Itsaka Rakotonirina, PhD student in the Pesto Team, will defend his thesis on Monday, February 1st at 2pm.
Title: Symbolic verification of cryptographic protocols, theory and practice
The defence will be english. You can also find his dissertation here.
This thesis studies the analysis of cryptographic protocols. They are sequences of instructions permitting to interact with a recipient remotely while protecting the sensitive content of the communication from a potential malicious third party. Classical cases where the confidentiality and the integrity of the communication are critical are, among others, online payments and medical-service booking, or electronic voting.
We study notions of security defined technically by observational equivalences (which includes among others confidentiality, anonymity or non-traceability). We designed a program, DeepSec, which, from the description of a protocol for a fixed number of participants, verifies in a fully-automated way whether the protocol offers a security guarantee of this type. We demonstrate the ability of this tool to analyse complex attack scenarios through several examples, optimisations, and a detailed study of the complexity of the underlying problem.
David Basin (ETH Zurich) – reviewer, president
Tamara Rezk (Inria Sophia Antipolis) – reviewer
Myrto Arapinis (University of Edinburgh)
Vincent Cheval (Inria Nancy) – co-advisor
Thomas Jensen (Inria Rennes)
Steve Kremer (Inria Nancy) – advisor
Catuscia Palamidessi (Inria Saclay)