Formal verification of unlinkability for stateful protocols — Bridging the gap between symbolic and computational models

Defense type
Thesis
Starting date
End date
Location
IRISA Rennes
Room
Métivier
Speaker
Solène MOREAU (SPICY)
Main department
Theme

The ever-increasing dependency on computer systems justifies significant concerns over privacy, and notably calls for communication protocols that ensure some security properties such as unlinkability. Formally specifying this property is difficult and context-dependent, and verifying it is complex. Therefore, providing solid mathematical foundations and computer-assisted methods is becoming crucial, but current techniques are not sufficient to analyze unlinkability for stateful protocols.
In this thesis, we address both the modelling issue and the verification issue. We first propose a precise definition of unlinkability and discuss how existing notions are inadequate for our class of stateful protocols. Then, we address the issue of computer-assisted verification. We develop two approaches, both illustrated with case studies. Our first approach is a verification method based on sufficient conditions in the symbolic model. Our second approach is a framework and an interactive prover allowing us to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model.

Composition of the jury
David BAELDE - Professeur, ENS Rennes, France - Supervisor
Gergei BANA - Associate Professor, University of Missouri, United States - Examiner
Stéphanie DELAUNE - Directrice de recherche CNRS, Rennes, France - Supervisor
Steve KREMER - Directeur de recherche Inria, Nancy, France - Reviewer
Sophie PINCHINAT - Professeure, Université de Rennes, France - Examiner
Alwen TIU - Associate Professor, Australian National University, Australia - Reviewer