Contributions à la vérification automatique de protocoles de groupes, Contribtutions to the Automatic verification of group protocols

Najah Chridi

Description

Sous la direction de Michaël Rusinowitch, Laurent Vigneron
Thèse soutenue le 11 septembre 2009: Nancy 1
Les protocoles cryptographiques sont cruciaux pour sécuriser les transactions électroniques. La confiance en ces protocoles peut être augmentée par l'analyse formelle de leurs propriétés de sécurité. Bien que beaucoup de travaux aient été dédiés pour les protocoles classiques comme le protocole de Needham-Schroeder, très peu de travaux s'adressent à la classe des protocoles de groupe dont les caractéristiques principales sont : les propriétés de sécurité spécifiques qu'ils doivent satisfaire, et le nombre arbitraire des participants qu'ils impliquent. Cette thèse comprend deux contributions principales. La première traite la première caractéristique des protocoles de groupe. Pour cela, nous avons défini un modèle appelé modèle de services que nous avons utilisé pour proposer une stratégie de recherche d'attaques se basant sur la résolution de contraintes. L'approche proposée a permis de retrouver d'anciennes attaques et d'en découvrir de nouvelles sur quelques protocoles de groupe. Certaines attaques ont aussi pu être généralisées pour couvrir le cas de n participants. La deuxième contribution principale de cette thèse consiste à définir un modèle synchrone qui généralise les modèles standards de protocoles en permettant les listes non bornées à l'intérieur des messages. Ceci est assuré par l'introduction d'un nouvel opérateur appelé mpair qui représente une liste construite sur un même patron. Dans ce modèle étendu, nous avons proposé une procédure de décision pour une classe particulière des protocoles de groupe appelée classe de protocoles bien-tagués avec clefs autonomes, en présence d'un intrus actif et avec des clefs composées.
-Protocole de groupe
-Listes paramétrées
-Protocoles cryptographiques
Cryptographic protocols are crucial for securing electronic transactions. The con?dence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder, very few address the class of group protocols whose main characteristics are : the speci?c security properties that they must satisfy, and the arbitrary number of participants they imply. This thesis provides two main contributions. The ?rst one deals with the ?rst characteristic of group protocols. For that, we de?ned a model called the services model which we used to propose a strategy for ?aws detection based on constraints solving. The suggested approach allows us to ?nd known attacks and new ones on some group protocols. Some attacks have been also generalized to cover the case of n participants. The second main contribution of this thesis consists in de?ning a synchronous model, that generalizes standard protocol models by permitting unbounded lists inside messages. This is ensured by the introduction of a new operator called mpair which represents a list built on the same pattern. In this extended model, we have proposed a decision procedure for a particular class of group protocols called the class of well-tagged protocols with autonomous keys, in presence of an active intruder and with composed keys.
Source: http://www.theses.fr/2009NAN10069/document

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 : [e-mail]




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 . . . . . .