Vérification formelle de protocoles cryptographiques : ProVerif, 25 ans déjà !

Les protocoles cryptographiques sont au cœur de la sécurité des communications numériques modernes. Pourtant, leur conception est notoirement sujette à erreurs, et leurs vulnérabilités demeurent difficiles à détecter par des méthodes de test traditionnelles. La vérification formelle propose une méthode rigoureuse pour analyser ces protocoles et établir, de manière mathématiquement fondée, des garanties de sécurité telles que la confidentialité ou l’authentification.

Après une mise en contexte et un bref panorama des approches et outils existants dans ce domaine, cet exposé présentera l’approche dite symbolique, et plus particulièrement les principes sous-jacents à l’outil ProVerif. Nous reviendrons sur les évolutions de l’outil depuis sa première version en 2001. Enfin, je vous présenterai un travail récent que j'ai mené en collaboration avec Vincent Cheval (Université d’Oxford). Ce travail étend ProVerif et permet l'analyse de protocoles reposant sur l'utilisation du ou exclusif (XOR), primitive dont les propriétés algébriques posent des défis spécifiques pour la vérification automatique.