Defense of the Habilitation to conduct research
November 18th, 2009, 9:30, in room C005 at LORIA, Nancy



Title: Analysis of cryptographic protocols: from symbolic to computational models



The habilitation manuscript (under review) can be found here (in French).

Abstract: (French version here)
Security protocols are programs that secure communications by defining exchange rules on a network. They are used in many applications such as ATM, pay-per-view, mobile phone and e-commerce. Their objective is e.g. to guarantee the confidentiality of sensitive data, to authenticate some of the participants, or to guarantee anonymity or non-repudiation. These programs are executed on easily accessible public networks like the Internet. Thus in order to check their security, it is necessary to consider all possible attacks that could be mounted.

The goal of my research habilitation thesis is to show that formal methods are well adapted for a precise analysis of cryptographic protocols, through various kind of tools. In this thesis, we present procedures to detect automatically  whether a protocol is secure or not. We have proposed several algorithms, depending on which security properties are considered and which cryptographic primitives are used (encryption, signature, hash, exclusive or, etc.). Moreover, we characterize conditions that allow to combine the preceding results and to design protocol in a modular way.

These results are based on symbolic models, very different from those used in cryptography where the notion of security is based on the complexity theory. This notion of security allows a better identification of all the attacks that can be mounted in reality but in return, the (heavy) security proofs are done by hand and seem difficult to automate. We have identified cryptographic hypotheses that allow to take the benefit of the symbolic and cryptographic approaches. It is then possible to obtain security proof at a cryptographic level, directly from proofs established (automatically) in symbolic models.



The committee will be composed of:

Reviewers Serge Abiteboul, INRIA Saclay, France
Yassine Lakhnech, Grenoble University, France
Roberto Segala, Verona University, Italy
Examiners Jean Goubault-Larrecq, LSV, ENS de Cachan, France
Joshua Guttman, Mitre Corporation / Worcester Polytechnic Institute, USA
Jean-Yves Marion, LORIA, INRIA, France
Michael Rusinowitch, LORIA, INRIA, France
Jacques Stern, École Normale Supérieure, France
Invitee Hubert Comon-Lundh, LSV, ENS de Cachan, France