Maître de Conférences, ENS Paris-Saclay
| Martín Abadi | Principal Scientist, Google & Professor emeritus, UC Santa Cruz |
| Gilles Barthe | Scientific Director, Max Planck Institute for Security and Privacy |
| Véronique Cortier | Directrice de Recherche, CNRS |
| Paul Gastin | Professeur, ENS Paris-Saclay |
| Catuscia Palamidessi | Directrice de Recherche, Inria |
| Frank Pfenning | Professor, Carnegie Mellon University |
The manuscript is available here.
Formal methods use techniques from theoretical computer science for the design and verification of trustworthy systems. Since the 80', the verification of cryptographic protocols has been the topic of active research in this domain, which has made it possible to automatically discover attacks and to formally prove security properties for ever-increasing classes of protocols, attackers and properties: Particular classes of attackers may be described symbolically, or arbitray Turing machines may be considered. Security properties 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 first consider the formal modelling of unlinkability and a technique for proving unlinkability with unbounded sessions, via the verification of sufficient conditions using existing tools. We then develop several partial order reduction techniques that have brought performance improvements in state-of-the-art equivalence verification tools for bounded sessions. We finally present ongoing work on a new approach for proving protocols in the computational model, based on the development of a meta-logic over the CCSA logic.
Les méthodes formelles mettent les outils de l'informatique théorique au service de la conception et de la vérification de systèmes fiables. Depuis les années 80, la vérification des protocoles cryptographiques a été un sujet de recherche actif dans ce domaine, ce qui a rendu possible la découverte automatique d'attaques et la preuve formelle de propriétés de sécurité pour des classes de protocoles, d'attaquants et de propriétés s'élargissant avec le temps: On peut notamment se restreindre à certaines classes d'attaquants spécifiées symboliquement, ou considérer des machines de Turing arbitraires. Par ailleurs, les propriétés de sécurité peuvent être vues comme des problèmes d'accessibilité, ce qui convient par exemple pour la confidentialité, ou plus généralement comme des problèmes d'équivalence comportementale, ce qui permet aussi de rendre compte de diverses propriétés liées au respect de la vie privée.
Nous présentons dans ce mémoire d'habilitation plusieurs contributions à ce domaine. Nous nous intéressons d'abord à la modélisation de la propriété de non-traçabilité et à sa preuve en nombre non-borné de sessions, via la vérification de conditions suffisantes au moyen d'outils existants. Nous développons ensuite plusieurs techniques de réduction d'ordres partiels qui ont permis l'amélioration des outils actuels de vérification d'équivalences en nombre de session borné. Nous présentons enfin des travaux en cours sur une nouvelle approche pour la preuve de protocoles dans le modèle calculatoire, fondée sur le développement d'une meta-logique au dessus de la logique CCSA.