Automatisation de preuves calculatoires de protocoles - Squirrel

Publié le lun 24/01/2022 - 14:28
Equipe
Date de début de thèse (si connue)
Septembre 2022
Lieu
IRISA, campus de Beaulieu, Rennes
Unité de recherche
IRISA - UMR 6074
Description du sujet de la thèse

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.

Bibliographie

[1] https://squirrel-prover.github.io

[2] David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos et Solène Moreau.
An Interactive Prover for Protocol Verification in the Computational Model.
In IEEE S&P 2021 - 42nd IEEE Symposium on Security and Privacy, San Francisco / Virtual, United States, mai 2021.
url : https: //hal.archives-ouvertes.fr/hal-03172119.

[3] Gergei Bana, Hubert Comon-Lundh.
A Computationally Complete Symbolic Attacker for Equivalence Properties.
ACM Conference on Computer and Communications Security  CCS'14. http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf

[4] Riccardo Focardi et Matteo Maffei.
Types for Security Protocols.
In Véronique Cortier et Steve Kremer, éditeurs, Formal Models and Techniques for Analyzing Security Protocols. Tome 5, Cryptology and Information Security Series, pages 143-181. IOS Press, 2011.
url : https://doi.org/10.3233/978- 1-60750-714-7-143.

[5] David Baelde, Stéphanie Delaune, Adrien Koutsos, Solène Moreau.
Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant.
[Research Report] IRISA. 2021.
https://hal.archives-ouvertes.fr/hal-03500056/

[6] Ton van Deursen, Sasa Radomirovic.
Attacks on RFID protocols.
IACR e-print, 2008. https://eprint.iacr.org/2008/310.pdf

Liste des encadrants et encadrantes de thèse

Nom, Prénom
Delaune, Stéphanie
Type d'encadrement
Directeur.trice de thèse
Unité de recherche
IRISA, UMR 6074
Equipe

Nom, Prénom
Lallemand, Joseph
Type d'encadrement
Co-encadrant.e
Unité de recherche
IRISA, UMR 6074
Equipe
Contact·s
Nom
Delaune, Stéphanie
Email
stephanie.delaune@irisa.fr
Téléphone
02 99 84 73 38
Nom
Lallemand, Joseph
Email
joseph.lallemand@irisa.fr
Téléphone
02 99 84 75 41
Mots-clés
Sécurité, protocoles cryptographiques, méthodes formelles