fr/Publis/PAPERS/PDF/Boisseau-these.pdf

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 : Alexandre Boisseau Discipline : Informatique Abstractions pour la vØri cation de propriØtØs de sØcuritØ de protocoles cryptographiques Soutenue le 19 septembre 2003 Composition du jury : Michel Bidoit Directeur de thŁse Paul Gastin PrØsident du jury Jean Goubault-Larrecq Examinateur Francis Klay Yassine Lakhnech Rapporteur Jean-Fran ois Raskin RappRemerciements Je voudrais avant tout remercier les membres du jury. Jean-Fran ois Raskin, ainsi que Steve Kremer, m’ont chaleureusement accueilli au DØ- partement d’Informatique de l’UniversitØ Libre de Bruxelles, pour travailler avec eux sur les protocoles de type signatures Ølectroniques de contrats. Je garde un excellent souvenir de ces quelques semaines de travail passØes en Belgique et je les en remercie. Je remercie d’autant plus Jean-Fran ois d’avoir acceptØ la charge de rapporteur au sujet de cette thŁse. Yassine Lakhnech m’a invitØ deux reprises pour donner un sØminaire au laboratoire VØrimag Grenoble. Ces sØminaires ont toujours ØtØ suivis de longues discussions et d’Øchanges d’idØes trŁs intØressants et mon seul regret est de n’avoir pu dØvelopper, au cours de cette thŁse, toutes les pistes qui m’avaient ØtØ suggØrØes. Je le remercie pour ces invitations et pour avoir, lui-aussi, acceptØ la charge de rapporteur. Jean Goubault-Larrecq a acceptØ de m’encadrer sur la derniŁre partie de ma thŁse et de faire partie du jury et je l’en remercie. Mais ce pourquoi j’aimerai le remercier Øgalement, c’est pour un moment dont, peut-Œtre, il ne se souvient pas. Il s’agit d’une discussion que nous avons eue un jour sur les catØgories. Discussion totalement dØsinterressØe, juste pour le plaisir de raconter (pour lui) et d’Øcouter (pour moi). Merci donc pour ce moment de science pure et pour le reste. Francis Klay a acceptØ de faire partie du jury et Paul Gastin en a ØtØ le prØsident, je les en remercie tous deux. Je tiens remercier mon directeur de thŁse, Michel Bidoit pour m’avoir encadrØ durant cette thŁse et le stage de DEA qui l’a prØcØdØ tout en me laissant librement dØcider de suivre telle ou telle direction et faire les choses ma maniŁre. Je remercie tous mes camarades Cachanais et assimilØs pour leur amitiØ indØfectible, depuis sept ans (plus ou moins quelques annØes pour certains). Je voudrais remercier en particulier ANicolas, qui m’a de nombreuses fois aidØ rØaliser avec LT X mes idØes les plus saugrenuesE et Marie, qui partage et Øgaye mon bureau depuis plus de trois ans (sans se plaindre). Bien que je leur ai rarement parlØ de mon travail, mes parents et ma s ur m’ont toujours soutenu dans mes choix et ont ØtØ extrŒmement disponible lorsque j’avais besoin d’eux (en particulier pour l’organisation du pot de thŁse). Je les en remercie vivement. Finalement, je tiens remercier mes ØlŁves, passØs, prØsents (absents aussi, parfois) et venir. Gr ce eux, nos salles de cours ont toujours ØtØ un lieu agrØable et leurs questions m’ont permis de comprendre que rien n’est jamais dØ nitif. 34Table des matiŁres Introduction 9 1 La syntaxe 17 1.1 Un exemple de protocole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.2 Messages et processus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.3 Dans la suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2 VØri cation et abstractions 23 2.1 ModØlisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.2 Des approximations correctes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 I PropriØtØs de traces 29 3 Introduction 31 3.1 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Les approches existantes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.3 Notre approche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.4 Les processus considØrØs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4 ModØlisation algØbrique de protocoles 35 4.1 Logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 4.2 galitØ et spØci cations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3 SØmantique concrŁte des protocoles . . . . . . . . . . . . . . . . . . . . . . . . . 44 5 InterprØtation abstraite algØbrique 51 5.1 Abstraction des structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.2 Guide pour les abstractions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 6 En pratique 61 6.1 Projection des noms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 6.2 Filtrage des messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 6.3 LinØarisation des messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 6.4 Que montre-t-on rØellement ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 57 OptimalitØ 77 7.1 CatØgories et institutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 7.2 Abstractions et traductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 7.3 Traductions et optimalitØ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 II PropriØtØs de jeux 87 8 Introduction 89 8.1 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 8.2 Travaux existants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 8.3 Notre approche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 8.4 Syntaxe pour les protocoles d’Øchange . . . . . . . . . . . . . . . . . . . . . . . 93 9 SystŁmes de transitions alternØs, logique temporelle alternØe 97 9.1 SystŁmes de alternØs . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 9.2 Logique temporelle alternØe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 9.3 Description d’ATS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 10 ModØlisation des protocoles 107 10.1 PrØtraitement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 10.2 ATS associØ un protocole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 10.3 Un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 10.4 PropriØtØs de sØcuritØ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 11 Abstractions 125 11.1 Abstraction des ATS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 11.2 SØmantique abstraite des ØnoncØs ATL . . . . . . . . . . . . . . . . . . . . . . . 129 11.3 Guide pour les abstractions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 12 SØmantique abstraite des protocoles 135 12.1 Les agents, leur Øtat local . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 12.2 Relations de transition locales . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 13 En pratique 147 13.1 Calcul des ATS abstraits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 13.2 VØri cation e ectiv e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 13.3 RØsultats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 13.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 III PropriØtØs d’opacitØ 155 14 Introduction 157 14.1 Deux exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 14.2 Approches existantes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 14.3 Notre approche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159 615 ModØlisation 163 15.1 L’Øquivalence par tests du spi-calcul . . . . . . . . . . . . . . . . . . . . . . . . 163 15.2 Les systŁmes observables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166 15.3 L’observateur et les propriØtØs d’opacitØ . . . . . . . . . . . . . . . . . . . . . . 167 15.4 Abstractions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 15.5 Un autre exemple : un protocole de vote . . . . . . . . . . . . . . . . . . . . . . 171 15.6 En conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172 16 Relations de bisimilaritØ 173 16.1 Environnements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 16.2 BisimilaritØ contextuelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 16.3 h-bisimilaritØ con . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178 16.4 h gardØe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180 16.5 Uni cation des di Øren tes bisimilaritØs . . . . . . . . . . . . . . . . . . . . . . . 184 16.6 Retour aux problŁmes d’opacitØ . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 17 Utilisation de contraintes 191 17.1 ReprØsentations d’un prØdicat . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 17.2 Application la simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197 18 En pratique 205 18.1 Le d ner des cryptographes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 18.2 Le protocole de vote . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208 18.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210 Conclusion 213 78Introduction Depuis le dØveloppement fulgurant de l’utilisation des rØseaux informatiques et de l’infor- matisation des communications (et l’enregistrement des donnØes), rares sont les personnes n’avoir aujourd’hui aucun contact avec un ordinateur au sens large : ordinateurs person- nels, terminaux bancaires, informatisation des dossiers mØdicaux, etc. Chacun, ou presque, est alors conf