ACCES: Algorithmes Cryptographiques CErtifiéS
Collaboration Locale de Recherche
Contexte et Objectifs
La vérification des protocoles cryptographiques, qui a connu ces
dernières années une véritable explosion, repose sur l'hypothèse de la
cryptographie parfaite, selon laquelle il est impossible d'accéder au
contenu d'un message crypté sans connaître la clé. Cette hypothèse est
cruciale pour les travaux de vérification mais elle est très forte et
il serait souhaitable de l'affaiblir. Toutefois, il s'est avéré
difficile de fournir un cadre dans lequel exprimer la correction d'un
algorithme cryptographique: en fait, la robustesse d'un algorithme
cryptographique est traditionnellement exprimée par réduction à un
problème calculatoire complexe, comme la factorisation en nombres
premiers.
Le modèle GM+ROM offre un cadre mathématique pour donner une
définition précise de la sûreté d'un algorithme cryptographique, et de
démontrer qu'un algorithme donné est sûr. Pour ce faire, GM+ROM
combine le modèle de l'oracle aléatoire (Random Oracle Model ROM),
développé par Fiat et Shamir puis amélioré par Bellegarde et Rogaway,
et le modèle générique (Generic Model GM), développé par Nechaev, puis
amélioré par Shoup, Schnorr et Jakobsson. L'intérêt de ce modèle est
triple: premièrement, il permet de prouver la sûreté d'un algorithme
cryptographique. Deuxièmement, il permet de raisonner sur des attaques
interactives, ce qui était exclu par les approches précédentes.
Troisièmement, il se prête bien à la modélisation dans un assistant à
la preuve. C'est ce dernier aspect qui nous intéresse.
L'objectif du projet est de fournir une description formelle du modèle
de sécurité GM+ROM sous Coq, et d'utiliser ce modèle pour démontrer la
correction d'algorithmes cryptographiques. Ce travail nécéssitera la
formalisation préliminaire de résultats d'algèbre et de probabilité,
qui se concrétisera par le développement d'une bibliothèque Coq sur
la théorie des nombres.
Participants
Les participants sont issus de l'I3S (Bruno Martin), du projet
Lemme à l'INRIA Sophia-Antipolis
(Gilles Barthe;
Jan Cederquist;
Loïc Pottier;
Sabrina Tarento),
et de l'équipe de
Géométrie Algébrique du Laboratoire Jean Dieudonné
(André Hirschowitz; Marie Virat).
Le projet Lemme utilise les méthodes formelles pour la certification
de logiciels, notamment pour le calcul scientifique et pour la validation
du code mobile et embarqué. Le projet dispose de deux compétences
complémentaires, d'une part dans les assistants à la preuve et leurs
applications et d'autre part dans le développement d'outils de
vérification dédiés à un domaine donné.
Les recherches de l'équipe de Géométrie Algébrique du Laboratoire
Jean Dieudonné portent sur la géometrie algébrique et applications à
la cryptographie, la théorie des catégories, le lambda-calcul et la
formalisation des mathématiques.
Les recherches de Bruno Martin portent sur la cryptographie.
Résultats
Certifying Cryptographic Algorithms in Coq, par Sabrina Tarento.