Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés – ASAP

Nos techniques sont issues de différents domaines : le raisonnement automatique, la théorie de la concurrence et plus généralement la vérification automatique. Le travail sur l'outil ProVerif a en effet bénéficié d'avancées dans le domaine de la déduction automatique, à savoir le «feature vector indexing« permettant une subsomption efficace d'ensemble à clause proposée par Schulz il y a quelques années. Notre travail sur les équivalences dans un calcul probabiliste de pi appliqué s'appuie sur un grand nombre de résultats existants car nous exprimons notre sémantique en termes de systèmes de transition probabilistes et non déterministes généraux. Enfin, la théorie de SAPIC+ s'appuie sur la sémantique classique des calculs de processus, telle qu'elle est étudiée en théorie de la concurrence.

Nous avons étudié les équivalences de processus probabilistes pour les protocoles de sécurité et nous proposons un nouveau cadre où le flux de contrôle des protocoles et des attaquants peut être probabiliste. Nous montrons que pour la classe des protocoles non-probabilistes, mais permettent à l'attaquant de faire des choix probabilistes, l'équivalence de may-testingqui en résulte est strictement plus forte en permettant un attaquant probabiliste. Pour un nombre limité de sessions, le may-testing avec un attaquant probabiliste coïncide avec la similarité purement possibiliste. Nous considérons également une classe de processus simples, avec un non-déterminisme très limité. Pour cette classe, nous montrons que l'équivalence des traces coïncide avec le may-testing lorsque les attaquants sont des processus séquentiels.

Nous avons effectué une révision majeure de l'outil populaire ProVerif en améliorant son expressivité et son automatisation. Son efficacité a été considérablement améliorée en utilisant des techniques de déduction automatique pour accélérer les vérifications de subsomption. En moyenne, ProVerif est maintenant 10 à 50 fois plus rapide que sa version précédente. Nous avons également intégré à TAMARIN une plateforme de vérification de protocoles appelée SAPIC+ qui permet aux utilisateurs de compiler un langage d'entrée commun à 3 outils de vérification de pointe. Nos preuves de correction garantissent que les résultats d'un outil peuvent être utilisés dans n'importe quel autre outil. Pour démontrer son utilité, nous avons porté (entre autres) le modèle TAMARIN existant de l'étude de cas complexe des protocoles d'authentification 5G vers SAPIC+ : les oracles dédiés utilisés pour automatiser les preuves dans TAMARIN ont été transférés directement, et le temps de vérification a été préservé, ce qui montre l'efficacité du modèle généré.

Nous avons réalisé plusieurs études de cas. Nous avons effectué une analyse approfondie du protocole de vote électronique Belenios avec un modèle beaucoup plus détaillé que celui habituellement considéré. L'analyse dévoile des failles inconnues dans certains scénarios de corruption. Nous proposons des solutions et prouvons qu'elles sont sûres. Le système de vote électronique SwissPost est actuellement soumis à un examen public, avant d'être déployé en 2022 pour les élections politiques dans plusieurs cantons suisses. Nous expliquons comment des contraintes du monde réel ont conduit à des failles qui ont permis de monter une attaque contre la confidentialité. Cette faille a été reconnue par la Poste suisse, rendue publique, et le système sera corrigé pour éviter le problème. Nous avons travaillé sur une analyse formelle détaillée de ZCash, une spécification et une implémentation d'un système de paiement anonyme décentralisé. Bien que ProVerif soit couramment utilisé pour l'analyse de grands protocoles cryptographiques réels, cette étude de cas a poussé l'outil à ses limites. En conséquence, nous avons ajouté des optimisations qui accélèrent la vérification et améliorent la consommation de mémoire. Enfin, nous avons utilisé SAPIC+ pour une vérification formelle approfondie du protocole LAKE-EDHOC, un protocole d'authentification pour l'IoT, actuellement en cours de normalisation.

Nous poursuivons le développement de nos outils en les appliquant à des études de cas ambitieuses. Les analyses du standard LAKE-EDHOC et de la spécification ZCash sont toujours en cours. Elles permettent d'identifier les limites des outils actuels et les améliorations à apporter. En particulier, SAPIC+ devra gagner en maturité pour devenir une plateforme utilisable. Motivés par notre travail sur les équivalences dans un calcul probabiliste de pi appliqué, nous prévoyons d'intégrer dans DEEPSEC la vérification de l'équivalence de similarité et une extension pour les processus probabilistes. Pendant la vérification de LAKE-EDHOC, nous avons identifié le besoin de vérifier les propriétés de vivacité (pour vérifier la propriété de non-répudiation). Un problème similaire se pose dans le vote électronique lorsque la responsabilité («acountability«) est requise. Ceci est actuellement hors de portée de ProVerif, et nous allons travailler sur une extension de ProVerif pour fournir au moins un support limité pour de telles propriétés. Nous travaillerons également à l'amélioration de l'automatisation dans Tamarin : en particulier, nous améliorerons les heuristiques intégrées et un meilleur support pour les «oracles« qui permettent à un utilisateur de spécifier des heuristiques dédiées.

1. ProVerif with Lemmas, Induction, Fast Subsumption, and
Much More. Bruno Blanchet, Vincent Cheval, and Véronique
Cortier. In Proceedings of the 42nd IEEE Symposium on Security
and Privacy (S&P'22), IEEE Computer Society Press, 2022.
hal.inria.fr/hal-03366962v1

2. A privacy attack on the Swiss Post e-voting system.
Véronique Cortier, Alexandre Debant, and Pierrick Gaudry. In
Real World Crypto Symposium (RWC'22), Amsterdam,
Netherlands, 2022. hal.inria.fr/hal-03446801/

Les protocoles cryptographiques sont un élément essentiel pour sécuriser les communications en ligne. En s'appuyant sur des primitives cryptographiques, telles que le chiffrement et la signatures numérique, ces protocoles garantissent des propriétés de sécurité telles que la confidentialité et l'authenticité. Ces propriétés sont les objectifs élémentaires de TLS, le protocole cryptographique le plus largement déployé, qui sous-tend toutes les connexions 'https' sur Internet. De nombreuses applications modernes peuvent également avoir besoin de garantir des propriétés liées à la vie privée des utilisateurs, p. ex. l'anonymat et la non-traçabilité des utilisateurs.

L'histoire a cependant montré que les protocoles cryptographiques sont sujets aux erreurs et des attaquants ont su exploiter de nombreuses failles de conception. La difficulté de concevoir correctement ces protocoles vient d'une asymétrie inhérente : alors que le concepteur doit penser à toutes les attaques possibles, un attaquant n'a besoin de trouver qu'une seule faiblesse. Il est difficile pour un humain d'explorer tous les cas possibles dans une preuve de sécurité : on considère un attaquant ayant le contrôle du réseau, capable d'intercepter, de modifier et d'insérer des messages, en plus des aspets liés à la concurrence. Cette tâche est d'autant plus compliquée pour des propriétés de sécurité fortes qui sont garanties (parfois de façon dégradée) même lorsque des parties du système ont été compromises. Il est donc essentiel de concevoir des algorithmes capables d'automatiser ces preuves ou, le cas échéant, de détecter les attaques. L'approche qui consiste à représenter les messages comme des termes du premier ordre a été initiée dans les travaux fondateurs de Dolev et Yao et a connu un grand succès, p. ex. lors de l'analyse de nouveaux standard tels que TLS 1.3 ou la 5G.

Le but du projet est la conception d'algorithmes et d'outils efficaces, basés sur des techniques de raisonnement automatique, pour la vérification de protocoles cryptographiques. Le raisonnement automatique est le sous-domaine de l'IA visant la conception d'algorithmes permettant aux ordinateurs de raisonner; ces techniques sous-tendent presque tous les outils modernes de vérification. Les outils d'analyse actuels ont cependant du mal à passer à l'échelle, ou nécessitent de (trop) simplifier les modèles, lorsqu'ils sont appliqués à des protocoles cryptographiques réellement déployés. Notre objectif est de surmonter ces limitations : nous concevrons de nouveaux algorithmes dédiés, intégrerons ces algorithmes dans les outils de vérification et utiliserons les outils résultants pour l'analyse de sécurité de ces protocoles. Les outils auront une efficacité accrue, une meilleure automatisation et une portée plus large. Ces développements seront guidés par et validés sur trois classes de protocoles : les protocoles de vote électronique, les protocoles pour les appareils mobiles du standard 5G et les protocoles pour les applications de messagerie, tels que ceux définis dans le cadre NOISE.

Notre recherche est guidée par le développement d'outils de vérification et leur application à des protocoles réels. Le développement d'outils efficaces et utilisables nécessite, d'une part, le développement de bases théoriques solides et, d'autre part, leur évaluation sur des études de cas réels. Notre projet s'articulera autour du développement de plusieurs outils complémentaires développés au sein de l'équipe de recherche PESTO, dirigée par Steve Kremer. D'un point de vue plus technique, les méthodes développées dans le projet incluent des techniques de raisonnement symbolique sur des traces partiellement ordonnées, de nouveaux algorithmes de subsomption efficace pour la résolution des clauses de Horn, des techniques de raisonnement équationnel pour supporter des opérateurs associatifs, commutatifs, ainsi que des heuristiques pour guider l'exploration de l'espace d'états afin de favoriser la terminaison.