À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.
| Identifer | oai:union.ndltd.org:theses.fr/2016SACLN008 |
| Date | 11 January 2016 |
| Creators | Chretien, Rémy |
| Contributors | Université Paris-Saclay (ComUE), Delaune, Stéphanie |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0019 seconds