PROUVÉ :
Protocoles cryptographiques: Outils de rification automatique

PROUVÉ était un projet exploratoire du Réseau National des Technologies Logicielles (RNTL) soutenu par le Ministère de l'éducation nationale, de l'enseignement supérieur et de la recherche. Le projet a commencé le 24 novembre 2003, et s'est terminé le 23 mai 2007 (36 mois plus 6 mois de prolongation).

Contexte : Vérification de protocoles cryptographiques

PROUVÉ porte sur la vérification automatique des protocoles cryptographiques. Ces protocoles sont utilisés massivement dans les applications logicielles sécurisées, par exemple dans les services bancaires, les services audiovisuels, les enchères et le vote électronique, la distribution d'informations etc.

Même en supposant que les algorithmes utilisés, typiquement le chiffrement, les fonctions à sens unique ou les générateurs aléatoires sont parfaits, la plupart des protocoles publiés comportent des failles. Ceci justifie l'intérêt grandissant de la communauté scientifique pour la vérification de tels protocoles.

Par ailleurs, chaque application possède ses contraintes spécifiques et utilise en général de petites variantes d'un même protocole. Mais de petites variations d'un protocole sûr peuvent comporter des failles de sécurité. La multiplicité des variantes requiert ainsi, à fins de vérification, des outils automatiques.

PROUVÉ s'attaquera à des problèmes sémantiques, à la diversification des propriétés sécuritaires considérées; il étudiera et implantera pour la première fois, des vérificateurs automatiques qui ne supposent pas le chiffrement parfait et produira un logiciel comportant plusieurs démonstrateurs dont l'entrée et les sorties seront spécifiées dans un unique formalisme.

Critique des outils existants

Il existe aujourd'hui de nombreux prototypes de vérification automatique de protocoles cryptographiques, notamment en France et aux États-Unis. Ceux-ci comportent tous de nombreuses faiblesses. D'abord ils s'appuient presque exclusivement sur un seul outil de démonstration, ce qui présente deux défauts majeurs  Tous les outils existants font également deux hypothèses importantes: celle du chiffrement parfait et celle du générateur aléatoire parfait. La première énonce qu'aucune information ne peut être obtenue sur un texte à partir du chiffrement de ce texte et la deuxième énonce le caractère unique et imprévisible des nombres engendrés aléatoirement (nonces). Or aucune de ces deux hypothèses n'est vraiment réaliste: certains protocoles utilisent au contraire explicitement les propriétés algébriques des techniques de chiffrement et d'autre part certains protocoles remplacent, pour des raisons d'efficacité, les nonces par des empreintes de date (timestamp) ou même des compteurs.

Nos objectifs dans le projet PROUVÉ

Nous avons pour ambition de fournir au moins trois outils de vérification issus de trois laboratoires distincts avec les spécificités suivantes : Enfin, le projet s'attaquera à deux études de cas significatives : un porte-monnaie électronique et un protocole d'enchères, qui lui permettront à la fois de guider les recherches, d'expérimenter les outils et de valider les résultats. Il maintiendra par ailleurs une base de données de protocoles cryptographiques qui serviront également de test.

Organisation du projet

Le projet est divisé en cinq tâches :
  1. Sémantique des protocoles et des propriétés
  2. Présentation des résultats
  3. Étude de cas
  4. Réalisation et mise au point des outils
  5. Affaiblissement du chiffrement parfait

Partenaires

Délivrables

Tache 1

Tache 2

Tache 3

Tache 5

Rapport final

Software


Page maintenue par Ralf Treinen