these

Sujets

• informatique
• ordinateur

Informations

• Publié par: Phoiv
• Nombre de lectures: 24
• Langue: Français

Extrait

TH¨SE
prØsentØe à l’ cole Normale SupØrieure de Cachan
pour obtenir le grade de
DOCTEUR DE L’ COLE NORMALE SUP RIEURE DE CACHAN
par : Muriel Roger
SpØcialitØ : Informatique
Ra nemen ts de la rØsolution et vØri cation
de protocoles cryptographiques
Soutenue le 24 octobre 2003
Composition du Jury :
Guy Cousineau rapporteur
Didier Galmiche rapp
Jean Goubault-Larrecq directeur de thŁse
Francis Klay examinateur
Yassine Lakhnech prØsident du jury
Denis Lugiez
Michaºl Rusinowitch examinateur2Table des matiŁres
Introduction 7
I tat de l’art 11
1 Techniques de dØmonstration automatique 13
1.1 Quelques dØ nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.2 La rØsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.3 La rØsolution ordonnØe avec sØlection : un ra nemen t de la rØsolution . . . . . . . 16
1.4 StratØgies d’Ølimination de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4.1 limination de tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4.2 de clauses subsumØes . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4.3 limination des pures . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5 Splitting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5.1 Splitting et tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5.2 sans splitting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.6 Quelques classes dØcidables de clauses . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.6.1 Classe de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.6.2 d’Ackermann . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.6.3 Classe monadique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1.7 Clauses de Horn et automates d’arbres . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.7.1 Langages et reconnaissabilitØ . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.7.2 Automates d’arbres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.7.3 bidirectionnels alternants . . . . . . . . . . . . . . . . . . . . . . 24
2 Les protocoles cryptographiques 27
2.1 Un peu d’histoire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.2 Les notions principales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2.1 DØ nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2.2 PropriØtØs de sØcuritØ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.3 Attaques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3 ModŁles et mØthodes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.3.1 Le spi-calcul . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3.2 Les modŁles à la Dolev-Yao . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3.2.1 Principes fondamentaux . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3.2.2 Les mØthodes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.4 Extensions de modŁles à la Dolev-Yao . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.4.1 Le modŁle de B. Blanchet . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.4.2 ModŁle de trace basØ sur des clauses de Horn . . . . . . . . . . . . . . . . . 37
2.4.3 Automates d’arbres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
34 TABLE DES MATI¨RES
II Un outil modulaire de rØsolution 41
3 RØsolution abstraite 43
3.1 Termes et clauses symboliques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.1.1 Termes symboliques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.1.2 Quelques familles de termes symboliques . . . . . . . . . . . . . . . . . . . . 45
3.1.2.1 Les termes nis du premier ordre . . . . . . . . . . . . . . . . . . . 45
3.1.2.2 Les modulo une thØorie Øquationnelle quelconque . . . . . 46
3.1.2.3 Les termes rationnels du premier ordre . . . . . . . . . . . . . . . 48
3.1.2.4 Les -termes typØs et non typØs modulo ou . . . . . . . . . . 51
3.1.3 Clauses symboliques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.1.4 Uni cation et ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
3.1.4.1 Uni cation de termes symboliques . . . . . . . . . . . . . . . . . . 54
3.1.4.2 Ordre sur les atomes symb . . . . . . . . . . . . . . . . . . 55
3.2 SØmantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.2.1 SØmantique à la Tarski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.2.2tique à la Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.2.3 Clauses de Horn et plus petits modŁles . . . . . . . . . . . . . . . . . . . . . 57
3.2.4 Langages et reconnaissabilitØ . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.3 RØsolution abstraite ordonnØe avec sØlection . . . . . . . . . . . . . . . . . . . . . . 59
3.4 StratØgies d’Ølimination de clauses symboliques . . . . . . . . . . . . . . . . . . . . 66
3.4.1 limination de tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.4.2 de clauses symboliques subsumØes . . . . . . . . . . . . . . . . 66
3.4.3 limination des symb pures . . . . . . . . . . . . . . . . . . . 67
3.5 Splitting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.5.1 Splitting et tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.5.2 sans splitting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4 MoP : un prouveur modulaire 73
4.1 Architecture gØnØrale de MoP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.1.1 Les termes abstraits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.1.2 La rØsolution abstraite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.2 Algorithme de rØsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.2.1 Remarques sur la subsomption . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.2.2 Algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
5 Les di Øren ts modules 83
5.1 Termes nis du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
5.2 Termes cycliques du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
5.2.1 Une dØ nition des termes rationnels . . . . . . . . . . . . . . . . . . . . . . 85
5.2.2 Uni cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
5.3 Automates d’arbres bidirectionnels modulo AC . . . . . . . . . . . . . . . . . . . . 87
5.3.1 Termes et clauses avec opØrateur associatif et commutatif . . . . . . . . . . 87
5.3.2 Approximation sur Z=nZ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
5.3.2.1 Choix de la fonction de sØlection . . . . . . . . . . . . . . . . . . . 91
5.3.2.2 Zones hachurØes et oracles de hachures . . . . . . . . . . . . . . . 94
5.3.2.3 Un ra nemen t des zones hachurØes . . . . . . . . . . . . . . . . . 95
5.3.2.4 Un oracle modi Ø simple . . . . . . . . . . . . . . . . . . . . . . . 99
5.3.3 Modi cations du prouveur . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.3.3.1 ImplØmentation des rŁgles (ASplit) et (Exit) . . . . . . . . . . . . 101
5.3.3.2 Nouvelles rŁgles pour le prouveur . . . . . . . . . . . . . . . . . . 102TABLE DES MATI¨RES 5
6 Application 105
6.1 Group Di e-Hellman key distribution : GDH.2 . . . . . . . . . . . . . . . . . . . . 105
6.1.1 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
6.1.2 Mise sous forme clausale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
6.1.3 RØsultats de MoP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
6.2 Optimisations - AmØliorations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
6.2.1 Optimisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
6.2.2 AmØliorations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
Conclusion 117
A Ordres bien fondØs 119
B Signature sur les termes abstraits 1236 TABLE DES MATI¨RESIntroduction
Le domaine de la dØmonstration automatique est certainement l’un des plus vieux domaines
de l’informatique, qui prend ses sources avant l’apparition des premiers ordinateurs. Au dØpart,
l’intØrŒt de la dØmonstration automatique repose sur deux aspects pour les mathØmaticiens, qui
d’ailleurs donneront lieu à un certain nombre de polØmiques : le premier est l’espoir d’obtenir
ainsi une aide à la dØcouverte de thØorŁmes, et le deuxiŁme, plus rØaliste, repose sur l’aspiration
à une aide pour la vØri cation de thØorŁmes.
Les premiers programmes de dØmonstration automatique font leur apparition dans les annØes
1960. En 1