Ma soutenance de thèse

Informations pratiques

Date et heure

Lundi 26 novembre 2018, 14h00.

Lieu

Amphi Chemla
École Normale Supérieure Paris-Saclay
61 avenue du Président Wilson
94230 Cachan

Comment venir

Allez voir cette page pour l'itinéraire jusqu'au campus et ensuite cette carte pour trouver votre chemin sur le campus. L'amphi Chemla se trouve dans l'Institut D'Alembert, indiqué par IDA sur la carte. À ne pas confondre avec le bâtiment D'Alembert.

Thèse

Titre

Vérification de propriétés d'indistinguabilité pour les protocoles cryptographiques -- Petites attaques et décision efficace avec SAT-Equiv.

Mots-clés

Protocoles cryptographiques, Méthodes formelles, Modèle symbolique

Résumé

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. 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.

Manuscrit

Ma thèse est disponible ici.

Jury

CHEVALIER Yannick Rapporteur
VIGANÒ Luca Rapporteur
DELAUNE Stéphanie Directrice de thèse
CORTIER Véronique Directrice de thèse
PALAMIDESSI Catuscia Examinatrice
COMPAGNA Luca Examinateur
LUBICZ David Examinateur

À propos du LSV