Analysis of cryptographic protocols: from symbolic to computational models
Analyse des protocoles cryptographiques: des modèles symboliques aux modèles calculatoires
Résumé
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.
Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.