PROUVÉ :
Protocoles cryptographiques: Outils de Vé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
- Comme la vérification de protocoles est indécidable,
tout outil ou bien peut ne pas s'arrêter, ou bien effectue des
approximations. Dans les deux cas, la présence de plusieurs outils
permettra de réduire les cas d'échec en choisissant l'outil adapté au
problème posé
- Chaque outil utilise implicitement un modèle pour les protocoles et les
propriétés à vérifier. Certains exemples célèbres de protocoles prouvés sur
lesquels ont été ultérieurement trouvées des attaques montrent qu'il faut être
extrêmement précis sur les hypothèses effectuées et les modèles utilisés. Le
projet EVA, qui réunissait deux
outils de démonstration a montré d'ailleurs qu'il existe de nombreuses
variantes dans la définition des modèles et que, faire tourner plusieurs
outils issus d'équipes différentes à partir d'une même spécification soulève
des problèmes sémantiques insoupçonnés.
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 :
-
Nos outils de vérifications utiliseront un
unique langage d'entrée avec une syntaxe et une sémantique commune.
-
Nos outils ne seront pas restreints à une seule propriété de sécurité
spécifique.
-
Nous allons définir un langage de propriétés
indépendant des protocoles et dans lequel peuvent s'exprimer de
nombreuses variantes des propriétés classiques.
-
Nous proposons d'étudier la vérification de protocoles
cryptographiques en affaiblissant l'hypothèse du chiffrement parfait,
notamment en considérant certaines propriétés algébriques des primitives
cryptographiques et la substitution des nonces par des timestamps.
-
Nous proposons de réaliser un outil de visualisation des
résultats et de simulation des attaques potentielles.
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 :
- Sémantique des protocoles et des propriétés
- Présentation des résultats
- Étude de cas
- Réalisation et mise au point des outils
- Affaiblissement du chiffrement parfait
Partenaires
Délivrables
Tache 1
Tache 2
- Report 8: Formalisme de Sortie des Outils de Vérification de
Protocoles Cryptographiques PROUVÉ
[Postscript]
[PDF]
Tache 3
Tache 5
Rapport final
Software
Page maintenue par
Ralf Treinen