Contact
communication [at] ens-paris-saclay.fr (Communication)

Protocoles cryptographiques : vérification de propriétés d'indistinguabilité

Antoine Dallon, doctorant au Laboratoire de Spécification et Vérification, soutiendra sa thèse consacrée à la "Vérification de propriétés d'indistinguabilité pour les protocoles cryptographiques -- Petites attaques et décision efficace avec SAT-Equiv", le 26 novembre prochain.
Institut d'Alembert, Amphi Chemla
Ajouter à mon agenda11/26/2018 2:00pm 11/26/2018 3:30pm Protocoles cryptographiques : vérification de propriétés d'indistinguabilité Institut d'Alembert, Amphi Chemla Europe/Paris public

Cette thèse s'inscrit dans le domaine de la vérification de protocoles cryptographiques dans le modèle symbolique. Plus précisément, il s'agit de s'assurer, à l'aide de méthodes formelles, que de petits programmes distribués satisfont à des propriétés d'indistinguabilité, c'est-à-dire qu'un attaquant n'est pas capable de deviner quelle situation (parmi deux) il observe.

Ce formalisme permet d'exprimer des propriétés de sécurité comme le secret fort, l'intraçabilité ou l'anonymat. De plus, les protocoles sont exécutés simultanément par un grand nombre d'agents, à plusieurs reprises, si bien que nous nous heurtons très rapidement à des résultats d'indécidabilité. Dès lors, il faut ou bien tenir compte du nombre arbitraire de sessions, et rechercher des méthodes de semi-décision ou identifier des classes décidables ; ou bien établir des procédures de décision pour un nombre fini de sessions.

Au moment où nous avons commencé les travaux présentés dans cette thèse, les outils de vérification de propriétés d'indistinguabilité pour un nombre borné de sessions ne permettaient de traiter que très peu de sessions : dans certains cas il était tout juste possible de modéliser un échange complet.

Propriétés d'indistinguabilité

Cette thèse présente des procédures de décision efficaces dans ce cadre.
Dans un premier temps, nous établissons des résultats de petite attaque. Pour des protocoles déterministes, nous démontrons qu'il existe une attaque si, et seulement si, il existe une attaque bien typée, lorsque toute confusion entre les types des variables est évitée. De plus, nous prouvons que, lorqu'il existe une attaque, l'attaquant peut la trouver en utilisant au plus trois constantes.

Dans un second temps, nous traduisons le problème d'indistinguabilité en termes d'accessibilité dans un système de planification, qui est résolu par l'algorithme du graphe de planification associé à un codage SAT. Nous terminons en confimant l'efficacité de la démarche, à travers l'implémentation de l'outil SAT-Equiv et sa comparaison vis-à-vis des outils analogues.