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

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.