Vérification automatique des protocoles cryptographiques : propriétés d'équivalence

Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.Plusieurs outils ont été développé pour vérifier automatiquement les propriétés de sécurité sur des protocoles cryptographiques. Jusqu'à maintenant, la plupart de ces outils permettent de vérifier des propriétés de trace (ou propriétés d'accessibilité) tel que le secret simple ou l'authentification. Néanmoins, plusieurs propriétés de sécurité ne peuvent pas être exprimés en tant que propriété de trace, mais peuvent l'être en tant que propriété d'équivalence. L'anonymat, la non-tracabilité ou le secret fort sont des exemples classique de propriété d'équivalence. Typiquement, deux protocoles P et Q sont équivalent si les actions d'un adversaire (intrus) ne lui permettent pas de distinguer P de Q. Dans la littérature, plusieurs notions d'équivalence ont été étudiés, par exemple l'équivalence de trace ou l'équivalence observationnelle. Néanmoins, ces équivalences se relèvent être très difficiles à démontrer , d'où l'importance de développer des outils de vérification automatique efficaces de ces équivalences. Au sein de cette thèse, nous avons dans un premier temps travaillé sur une approche reposant sur des techniques de résolution de contraintes et nous avons créé un nouvel algorithme pour décider l'équivalence de trace entre deux protocoles pouvant contenir des conditionnelles avec branches "else", et pouvant également être non-déterministe. Cet algorithme a été appliqué sur des exemples concrets comme le "Private authentification protocol" ainsi que le "E-passport protocol". Cette thèse propose également des résultats de composition pour l'équivalence de trace. En particulier, nous nous sommes intéressé à la composition parallèle de protocoles partageant certains secrets. Ainsi dans cette thèse, nous avons démontré que, sous certaines conditions, la composition parallèle de protocoles préserve les propriétés d'équivalence. Ce résultat fut appliqué au "E-passport protocol". Enfin, cette thèse présente une extension à l'outil de vérification automatique ProVerif afin de démontrer automatiquement plus de propriétés d'équivalence. Cette extension a été implémenté au sein de ProVerif ce qui a permis de démontrer la propriété d'anonymat pour le "Private authentification protocol"