Habilitation

David Baelde

Maître de Conférences, ENS Paris-Saclay

Defense

Jury (rapporteurs shown in bold)

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

Manuscript

The manuscript is available here.

Summary

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.

Résumé

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.

About LSV