Détails sur le séminaire

Résumé : Les preuves de sécurité pour les systèmes cryptographiques peuvent être effectuées dans
différents modèles qui correspondent chacun à des hypothèses de sécurité différentes. Dans
le modèle symbolique, on considère qu’un attaquant ne peut deviner aucun secret et qu’il
a seulement la possibilité d’appliquer un ensemble prédéfini d’actions. À l’inverse, dans le
modèle calculatoire, l’adversaire peut espérer deviner des secrets et appliquer n’importe
quelle opération qui se déroule en temps polynomial. Les propriétés de sécurité sont plus
dures à établir et à vérifier dans ce dernier modèle.
Au cours des travaux exposés dans cette thèse, nous avons étendu un cadre de travail
pour la certification de preuves d’indiscernabilité calculatoire. Ces preuves sont modélisées
à l’aide de l’assistant de preuve Coq, et basées sur cil (Computationnal Indistinguishability
Logic), une logique spécialisée pour le modèle calculatoire qui peut être appliquée et pour
les primitives et pour les protocoles. Nous montrons comment cil et sa modélisation en Coq
permettent des preuves qui vont au-delà du modèle calculatoire classique dit boîte noire,
où un adversaire n’effectue que des échanges de type requête/réponse avec le système sans
avoir d’information sur l’état du système.
Nous avons étendu cil pour parvenir à raisonner dans ces modèles. En particulier pour
prendre en compte la fuite d’information de systèmes honnêtes, autorisant l’adversaire à
connaître partiellement des données secrètes. Pour ce faire, nous nous sommes basés sur
le modèle à taille de mémoire bornée, qui limite la quantité d’information pouvant être
retrouvée par l’adversaire. Nous avons utilisé cette extension pour la preuve de sécurité
d’un protocole d’échange de clefs résistant aux intrusions. En modélisant l’intrusion hors
de la logique en elle-même, nous avons fait en sorte que cil garde une utilisation large et
non spécifique au modèle.
De cette façon, nous montrons qu’il est possible de modéliser des fuites d’informations
des participants honnêtes de protocoles sans modification majeure de cil. L’intrusion est
prise en compte au niveau de la modélisation du protocole, en ayant soin de ne pas rendre
cette preuve trop complexe pour l’utilisateur. Cette stratégie a été choisie pour sa capacité
d’adaptation à d’autres modèles de sécurité et constitue la motivation majeure de ces
travaux.
Pour mener à bien la preuve de ce protocole, nous avons développé diverses biblio-
thèques générales (comme la gestion des distributions) ainsi que des procédures permettant
d’automatiser les parties les plus triviales des preuves. De plus, nous avons développé une
architecture complexe pour modéliser la preuve de ce protocole qui s’articule sur plusieurs
primitives différentes, ce qui implique une preuve complexe devant s’articuler autour des
propriétés de sécurité de ces primitives.
Il résulte de ces travaux une preuve complexe d’un protocole dans un modèle de sécurité
sortant des modèles conventionnels. Cette preuve s’appuie sur les hypothèses de sécurité
des primitives utilisées par le protocole, ainsi que sur les règles de cil pour parvenir à
certifier la sécurité du protocole en présence d’agent d’observation.
Mots clefs : cryptographie, sécurité, preuve, méthodes formelles, certification, résistance
aux intrusions, modèle calculatoire, modèle à taille de mémoire borné, Coq



Composition du jury:
Christine Paulin : Université Paris Sud, INRIA - Saclay, Rapporteur
Véronique Cortier : CNRS, Nancy, Rapporteur
Bruno Blanchet : INRIA Paris - Rocquencourt, Examinateur
Steve Kremer : INRIA Nancy - Grand Est, Examinateur
Jean-François Monin : Université Grenoble-Alpes, Examinateur
Jean-Guillaume Dumas : Université Grenoble-Alpes, Examinateur
Yassine Lakhnech : Université Grenoble-Alpes, Directeur de thèse
Pierre Corbineau : Université Grenoble-Alpes, Co-Directeur de thèse