Automatisation de preuves calculatoires de protocoles - Squirrel

Alors qu'une part croissante des activités humaines se fait via des communications électroniques (messagerie, navigation web, paiements, vote…), les protocoles visant à sécuriser ces échanges prennent une importance grandissante. Le problème générale de la vérification formelle se décline de façon un peu particulière quand on considère les protocoles de sécurité, et a été le sujet de recherches actives depuis les années 1970. Aujourd'hui plusieurs types d'outils permettent d'analyser des protocoles par ordinateur ; ils diffèrent notamment par le niveau d'abstraction adopté, le degré d'automatisation, l'aptitude à trouver des attaques et/ou fournir des preuves.

L'outil Squirrel [1, 2] est un assistant de preuve dédié aux protocoles, reposant sur une approche en cours de développement et apportant un équilibre intéressant entre automatisation et précision par rapport aux autres outils. L'approche théorique sous-jacente est fondée sur une idée proposée par Bana et Comon en 2012 [3]. Cette idée a évolué et a été validée sur plusieurs études de cas concrètes, mais ce n'est qu'avec l'apparition de Squirrel et de sa logique "à deux étages" que l'approche a permis des preuves vérifiées par ordinateur pour des exécutions non bornées de protocoles. Datant de 2021, l'outil Squirrel est encore sujet à de nombreuses évolutions.

Le sujet s'articule autour de Squirrel et sa théorie. L'objectif sera d'y apporter des améliorations, sur le plan théorique et sur celui de l'implémentation. Un premier point concernera la sémantique du langage décrivant les protocoles (une algèbre de processus). Cette sémantique n'est actuellement pas définie directement, mais à travers une traduction vers un autre formalisme (systèmes d’actions). Donner une sémantique propre au langage permettra d’expliquer plus facilement les propriétés prouvées, en particulier à des non-spécialistes. La difficulté consistera à montrer que cette nouvelle sémantique correspond à celle induite par les systèmes d'actions. On commencera par se restreindre à un sous-ensemble du langage de processus (processus sans états).

Le second axe concerne le support des propriétés d'accessibilité. Squirrel propose un cadre théorique et une logique bien adaptés à la preuve de propriétés d'équivalence (ou indistinguabilité), qui expriment des garanties fortes de secret et de vie privée (anonymat, non-traçabilité, etc.). Cependant, la logique est moins appropriée pour prouver des propriétés d'accessibilité, e.g. de secret faible, qui sont des étapes intermédiaires indispensables lors de preuves dans des modèles complexes (e.g. oracle aléatoire). Un objectif majeur sera de construire puis intégrer à Squirrel des procédures pour faciliter ces preuves. La difficulté réside dans le fait que la logique interne de Squirrel a été conçue pour les équivalences. Manipuler des conditions d'accessibilité directement y est malaisé. Notre approche sera donc d’étudier les propriétés d'accessibilité dans un autre cadre logique, plus adapté, et à prouver formellement le lien avec la logique de Squirrel. Ceci sera facilité par le travail sur la sémantique des processus. Nous étudierons plus précisément une approche par systèmes de types, dans l’esprit de [4], qui pourra permettre de proposer des procédures de vérification efficaces, dont il faudra prouver la correction.

Enfin, l'objectif à terme est d'intégrer les techniques développées dans Squirrel. Il faudra donc les implémenter pour les rendre utilisables au sein de l'outil, ce qui permettra de traiter certains protocoles pour l'instant hors de portée de Squirrel. Pour valider l'intérêt et la généralité de l'approche, on examinera des protocoles RFID, tels que OSK ou SLK [6]. Ces protocoles ont été étudiés avec Squirrel [5], mais seulement de façon incomplète et simplifiée, car ils utilisent des oracles aléatoires, qui font qu'on se heurte aux problèmes décrits plus haut. On s'attachera à analyser des modèles plus complets de ces protocoles, en utilisant les améliorations apportées à l'outil.