Analyse des protocoles cryptographiques: des modèles symboliques aux modèles calculatoires

摘要

Security protocols are programs that secure communications by defining exchange rules on a network. They are used in many applications such as withdrawal machines, 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.