Contributions à la Vérification des Protocoles Cryptographiques
David Baelde · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
Formal methods use techniques from theoretical computer science for the designand verification of trustworthy systems. Since the 80’, the verification of cryptographicprotocols has been the topic of active research in this domain, which has made it possibleto automatically discover attacks and to formally prove security properties for ever-increasing classes of protocols, attackers and properties: Particular classes of attackersmay be described symbolically, or arbitrary Turing machines may be considered. Securityproperties may be viewed as reachability problems, which is appropriate e.g. for secrecy,or more generally as behavioural equivalences, which allows to capture various privacy-type properties.This habilitation manuscript presents several contributions to this domain. We firstconsider the formal modelling of unlinkability and a technique for proving unlinkabilitywith unbounded sessions, via the verification of sufficient conditions using existingtools. We then develop several partial order reduction techniques that have broughtperformance improvements in state-of-the-art equivalence verification tools for boundedsessions. We finally present ongoing work on a new approach for proving protocols in thecomputational model, based on the development of a meta-logic over the CCSA logic.