La lecture à portée de main
Découvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDécouvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDescription
Informations
Publié par | Thesee |
Nombre de lectures | 24 |
Langue | Français |
Poids de l'ouvrage | 1 Mo |
Extrait
AVERTISSEMENT
Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.
Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.
D’autre part, toute contrefaçon, plagiat, reproduction
illicite encourt une poursuite pénale.
➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr
LIENS
Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm ´D´epartement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
Contributions `a la v´erification
automatique de protocoles de groupes
`THESE
pr´esent´ee et soutenue publiquement le 11 Septembre 2009
pour l’obtention du
Doctorat de l’universit´e Henri Poincar´e – Nancy 1
(sp´ecialit´e informatique)
par
Najah CHRIDI
Composition du jury
Rapporteurs : Maryline MAKNAVICIUS-LAURENT Professeur, Telecom & Management, SudParis
Ralf TREINEN Professeur, Universit´e Paris Diderot
Examinateurs : Sjouke MAUW Professeur, Universit´e du Luxembourg
Refik MOLVA Professeur, Eurecom Sophia-Antipolis
Isabelle CHRISMENT Professeur, UHP Nancy 1
Laurent VIGNERON (directeur) Maˆıtre de conf´erences, Universit´e Nancy 2
Micha¨el RUSINOWITCH (directeur) Directeur de Recherche, INRIA
Mathieu TURUANI Charg´e de Recherche, INRIA
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Mis en page avec la classe thloria.i
`A la m´emoire de mon tr`es cher p`ere,
`A ma ch`ere m`ere,
mon immense gratitude pour tous les sacrifices que vous avez consacr´es pour moi,
`A l’homme de ma vie Nabil,
`A mes soeurs Dalila et Faten,
`A mes fr`eres Mondher et Med Ali,
`A mes neveux Abir et Oussama,
`A tous ceux qui m’aiment.iiiii
Remerciements
En tout premier lieu, je tiens `a remercier tous les membres de mon jury. Merci a` Maryline
Maknavicius-Laurent et Ralf Treinen pour avoir accept´e d’ˆetre les rapporteurs de cette th`ese
et de participer au jury. Leurs remarques et suggestions m’ont permis d’am´eliorer la qualit´e
de ce m´emoire. Merci ´egalement a` Isabelle Chrisment, Refik Molva et Sjouke Mauw qui m’ont
fait l’honneur de participer au jury de ma soutenance. Je remercie aussi Laurent Vigneron et
Micha¨el Rusinowitchpourm’avoir encadr´ee durantcette th`ese. Finalement, jeremercie Mathieu
Turuani pour sa collaboration, sa disponibilit´e et son enthousiasme.
Je tiens ´egalement a` exprimer ma gratitude `a l’ensemble des membres du LORIA et plus
particuli`erement auxmembresdel’´equipe CASSISpourlabonneambiance et laconvivialit´e qui
r`egnent dans ce laboratoire dynamique. Je remercie chaleureusement tous les enseignants avec
qui j’ai pu travailler durant la p´eriode de mes trois ann´ees de monitorat et mon ann´ee d’ATER.
Ils m’ont aid´e a` tendre vers une p´edagogie qui me ressemble et m’ont ainsi donn´e l’envie de faire
ce m´etier.
Enfin, je remercie tous les membres de ma famille et mes amis qui m’ont soutenu et accom-
pagn´e durantdenombreusesann´ees, ainsi quetoutes lespersonnesquim’ont apport´eunsoutien
moral de loin ou de pr`es. Je remercie en particulier mon mari qui n’a pas cess´e de m’´epauler et
de me soutenir dans les moments les plus difficiles. Mes remerciements ne seraient pas complets
si je ne mentionne pas mon p`ere qui n’a pas arrˆet´e de me pousser `a aller plus loin dans mes
´etudes. J’esp`ere qu’il trouve dans ce travail l’accomplissement de ses voeux.ivTable des mati`eres
Chapitre 1
Introduction 1
1.1 Protocoles cryptographiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.1 Protocoles de communication . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.2 Protocoles de groupe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.1.3 Primitives cryptographiques . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.1.4 Propri´et´es de s´ecurit´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1.5 Intrus, attaques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Formalisation des protocoles cryptographiques. . . . . . . . . . . . . . . . . . . . 9
1.2.1 Mod`ele de r´ef´erence : Alice-Bob . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2.2 Mod`ele de roˆles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.3 M´ethodes de v´erification des protocoles cryptographiques . . . . . . . . . . . . . 11
1.3.1 Falsification des protocoles cryptographiques . . . . . . . . . . . . . . . . 11
1.3.2 Validation des protocoles cryptographiques . . . . . . . . . . . . . . . . . 12
1.4 Contenu de la th`ese . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Chapitre 2
Protocoles de groupe
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Protocoles param´etr´es . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2.1 Classe de protocoles param´etr´es . . . . . . . . . . . . . . . . . . . . . . . 18
2.2.2 Protocoles de groupe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3 Gestion de clefs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.1 Approche centralis´ee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.3.2 Approche d´ecentralis´ee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3.3 Approche distribu´ee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.4 Propri´et´es de s´ecurit´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
vvi Table des mati`eres
2.4.1 Propri´et´es classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.4.2 Propri´et´es d’un groupe statique . . . . . . . . . . . . . . . . . . . . . . . . 31
2.4.3 Propri´et´es d’un groupe dynamique . . . . . . . . . . . . . . . . . . . . . . 32
2.4.4 R´esum´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.5 Impact des agents malhonnˆetes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
Chapitre 3
V´erification de protocoles de groupe
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2 Probl`emes li´es `a la v´erification des protocoles de groupe . . . . . . . . . . . . . . 40
´3.3 Etat de l’art : r´esultats exp´erimentaux . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.1 Analyse manuelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.2 Analyse automatique ou semi-automatique . . . . . . . . . . . . . . . . . 47
´3.4 Etat de l’art : r´esultats th´eoriques . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.4.1 Automates d’arbres pour les protocoles r´ecursifs (Ku¨sters) . . . . . . . . . 52
3.4.2 Clauses de Horn pour les protocoles r´ecursifs (Truderung) . . . . . . . . . 54
3.4.3 Extensions du mod`ele de Truderung (Ku¨sters-Truderung, Ku¨rtz) . . . . . 58
3.4.4 D´ecidabilit´e dans le cas d’un intrus passif (Kremer et al.) . . . . . . . . . 60
3.4.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
3.5 Notre exp´erimentation pr´eliminaire . . . . . . . . . . . . . . . . . . . . . . . . . . 62
3.5.1 M´ethode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.5.2 Analyse du protocole Asokan-Ginzboorg . . . . . . . . . . . . . . . . . . . 64
3.5.3 Analyse du protocole GDH . . . . . . . . . . . . . . . . . . . . . . . . . . 69
3.5.4 Analyse du protocole Tanaka-Sato . . . . . . . . . . . . . . . . . . . . . . 72
3.5.5 Analyse du protocole Iolus . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.5.6 Analyse d’une architecture de protocoles hi´erarchiques . . . . . . . . . . . 74
3.5.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
Chapitre 4
D´etection de types d’attaques sur les protocoles de groupe
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.2 D´efinitions pr´eliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.3 Pr´esentation du mod`ele de services . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.3.1 Exemples de protocoles de groupe : de DH a` A-GDH.2 . . . . . .