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.

Abstract:

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.

Jury:

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