Vérification formelle des protocoles cryptographiques :

lien avec la cryptanalyse

  Auteur : Véronique Cortier (LORIA, CNRS & projet INRIA Cassis)

cortier@loria.fr

Travaux réalisés en collaboration avec Bogdan Warinschi (Université de Bristol)

Les protocoles cryptographiques sont des petits programmes d'échanges de messages sur un réseau. Ils servent à assurer par exemple la confidentialité et l'authenticité des communications.

Deux approches très différentes ont été développées pour étudier ces protocoles. D'une part, l'approche dite "logique" ou "formelle" considère une version simplifiée des protocoles où le chiffrement est vu comme une boîte noire. Cette approche permet d'analyser très précisément, et souvent de manière automatique, la partie "protocole". D'autre part, les algorithmes de chiffrement sont étudiés par les cryptanalystes, en tenant parfaitement compte des fonctions mathématiques utilisées dans les algorithmes. Nous présenterons les deux approches et nous verrons comment il est possible de relier les deux. Cela permet de combiner les avantages des deux modèles : des preuves automatiques pour des notions de sécurité cryptographiques.

Ces résultats ne s'appliquent pour l'instant pas directement aux protocoles de vote mais cet exposé pourra être l'occasion de discuter de développements possibles dans cette direction.