Soutenance de thèse
Véronique Cortier
Titre de la thèse
Vérification automatique des protocoles cryptographiques
Date et lieu
Le
jeudi 20 mars 2003 à 15h
Salle de conférences,
Pavillon des Jardins, École Normale Supérieure de Cachan.
Plan d'accès
Composition du jury (proposition)
Résumé de la thèse
Cette thèse porte sur la vérification des protocoles cryptographiques en
interprétant les primitives cryptographiques comme des boîtes noires
(hypothèse du chiffrement parfait).
Ces protocoles sont utilisés dans de très nombreuses applications comme le
paiement sécurisé sur Internet ou la téléphonie mobile. Leur vérification est
essentielle car la moindre
faille peut avoir des conséquences catastrophiques. L'automatisation
de la vérification est fondamentale car le nombre d'applications est très
important et les propriétés et spécifications techniques varient d'une
application à l'autre.
De nombreux modèles et outils ont été développés depuis quelques années mais
tous ces travaux possèdent des faiblesses sémantiques et font des hypothèses
fortes sur le nombre de sessions ou l'absence de propriétés algébriques.
Les principaux résultats sont les suivants.
-
Nous proposons un nouveau modèle clair et simple sous forme de clauses de Horn
qui a permis par exemple
d'obtenir des résultats de simplification, comme la réduction à un nombre
fixé d'agents sans perte de généralité. Il autorise également l'utilisation
des méthodes classiques de résolution développées en logique du premier ordre.
-
Même une propriété simple comme le secret peut être modélisée de manière très différente.
Elle est représentée par une propriété d'accessibilité dans la plupart des modèles
mais elle est également modélisée par une propriété d'équivalence observationnelle :
un protocole préserve le secret s si un intrus ne peut faire la différence entre
le protocole contenant s et le protocole contenant la donnée s' à la place de s.
Nous faisons un lien entre ces deux propriétés dans un contexte très général, étendant ainsi
les travaux de M. Boreale.
-
Nous avons développé
un algorithme de vérification s'appliquant dans le cas
général. Il a été implémenté et appliqué avec succès à une famille de protocoles;
il est disponible publiquement.
-
Nous proposons un résultat de décision dans le cadre d'un nombre arbitraire de sessions.
Ce résultat s'applique à des protocoles ne comportant
qu'un nombre fini de nonces et pour lesquels une seule copie est possible à chaque étape.
- L'hypothèse du chiffrement parfait n'est pas réaliste. Ainsi, certains protocoles
sont corrects sous cette hypothèse alors que des failles existent en tirant avantage des
propriétés algébriques des primitives cryptographiques utilisées. Cela motive par exemple
l'étude des protocoles cryptographiques utilisant le << ou >> exclusif.
Nous étendons notre résultat de décision à une telle classe de protocoles.