fr/Publis/PAPERS/PDF/Boisseau-these.pdf
224 pages
Français

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

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
224 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

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

Sujets

Informations

Publié par
Nombre de lectures 151
Langue Français
Poids de l'ouvrage 1 Mo

Exrait

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 confrontØ un problŁme qui ne prØoccupait jusqu’ prØsent que les militaires et di- plomates : comment prØserver la con den tialitØ de ses donnØes ? ConsidØrons par exemple des renseignements relatifs au compte bancaire d’un client. Un contr le d’accŁs, s’il est correcte- ment mis en place, permet d’assurer la con den tialitØ de ces renseignements tant qu’ils restent statiques : stockØs sur ordinateur dans la banque et sur papier chez le client par exemple. Ce n’est plus le cas si, comme c’est aujourd’hui possible, le client dØsire consulter son compte ou rØaliser des opØrations bancaires distance au moyen d’internet car les donnØes doivent alors circuler sur le rØseau et il serait facile, pour quiconque en conna t le fonctionnement, d’y accØder, voire de les modi er. Il est donc apparu, pour le public, un besoin de sØcuriser les communications Ølectroniques. Depuis l’antiquitØ, d’aprŁs [EU00], l’usage de techniques cryptographiques tente d’apporter une rØponse ce problŁme. Cette mØthode consiste transformer les donnØes au moyen d’un algorithme tel que retrouver les donnØes de dØpart partir des donnØes chi rØes (i.e. celles obtenues aprŁs la transformation) soit algorithmiquement trŁs di cile a priori et facile si on dispose d’un autre algorithme dit de dØchi remen t. Dans les premiers temps de la cryptogra- phie, le secret reposait sur celui des algorithmes utilisØs (essentiellement des transpositions des lettres du message de dØpart ou des substitutions par d’autres lettres). En 1883, A. Kerckho s Ønonce ce que l’on appelle aujourd’hui les principes de Kerckho s [Ker83] que nous reprenons ici : [...] Il faut un systŁme remplissant certaines conditions exceptionnelles, conditions que je rØsumerai sous les six chefs suivants : 1. Le systŁme doit Œtre matØriellement, sinon mathØmatiquement, indØchi rable ; 2. Il faut qu’il n’exige pas le secret, et qu’il puisse sans inconvØnient tomber entre les mains de l’ennemi; 3. La clef doit pouvoir en Œtre communiquØe et retenue sans le secours de notes Øcrites, et Œtre changØe ou modi Øe au grØ des correspondants; 4. Il faut qu’il soit appliquable la correspondance tØlØgraphique; 5. Il faut qu’il soit portatif, et que son maniement ou son fonctionnement n’exige pas le concours de plusieurs personnes; 6. En n, il est nØcessaire, vu les circonstances qui en commandent l’application, que le systŁme soit d’un usage facile, ne demandant ni tension d’esprit, ni la connaissance d’une longue sØrie de rŁgles observer. 9 Les deuxiŁme et troisiŁme points sont sans doute les plus novateurs. Suivant ces recomman- dations, l’algorithme de chi remen t doit maintenant prendre en entrØe, non seulement les donnØes chi rer, mais aussi une clØ. Le chi remen t se fait relativement cette clØ avec pour consØquence que l’algorithme peut tout fait Œtre public, du moment que la clØ reste secrŁte. La mŒme clØ Øtait alors utilisØe pour le chi remen t et le dØchi remen t (avec, bien entendu, des algorithmes di Øren ts pour chi rer et dØchi rer) ce qui posait, entre autres, le problŁme de la communication de la clØ. On parlait alors de clØs (et de cryptographie) symØtriques. En 1976, W. Di e et M. Hellman proposent une nouvelle approche utilisant deux clØs dont l’une peut Œtre divulguØe [DH76], dont une rØalisation pratique est donnØe dans [RSA78] : c’est le fameux algorithme RSA de chi remen t. Chaque personne possŁde alors une clØ dite publique qui est potentiellement connue de tous et une clØ secrŁte (on parle alors de clØs et de cryptographie asymØtriques). Pour faire parvenir cette personne un message con den tiel, il su t de la chi rer en utilisant la clØ publique et de lui envoyer. Peu importe si le message chi rØ peut Œtre observØ ou pas : le destinataire sera le seul pouvoir le dØchi rer, puisqu’il faut pour cela utiliser la clØ secrŁte. Ce mØcanisme permet Øgalement de mettre en place une certaine forme d’authenti cation ou de signature : si quelqu’un chi re un message connu avec sa clØ secrŁte, on peut vØri er que cette opØration a bien ØtØ rØalisØ avec la bonne clØ (et par consØquent, par la bonne personne, sous certaines hypothŁses) en dØchi ran t simplement le message l’aide de la clØ publique. Le problŁme de la communication des clØs est Øgalement rØsolu puisque chaque personne peut, de maniŁre privØe, exØcuter un algorithme lui fournissant deux clØs inverses l’une de l’autre, et en publier une. NØanmoins, ces considØrations cryptographiques ne sont qu’un ØlØment de rØponse au problŁme des communications sßres et de nombreuses questions restent en suspens si on veut les mettre en pratique : comment obtient-on, par exemple, la clØ publique d’une personne ? Il n’est par ailleurs pas recommandØ d’utiliser outrance les clØs privØes et publiques. D’une part parce que les temps de chi remen t et de dØchi remen t sont plus longs qu’avec des clØs symØtriques et d’autre part, parce que les clØs privØes peuvent parfois Œtre dØcouvertes plus facilement lorsque de nombreux couples constituØs d’un message en clair et du mŒme message chi rØ sont connus. Comment, dans ces conditions, se mettre d’accord avec quelqu’un sur une clØ symØtrique, qui sera utilisØe pour une communication court terme ? Les protocoles cryptographiques permettent d’intØgrer la cryptographie dans des communications rØelles en rØpondant ces problŁmes concrets. Un protocole cryptographique se prØsente comme une succession de rØceptions et d’envois de messages, entrecoupØ de calculs Øventuels (dØchi rer des messages, les recombiner, faire des vØri cations, etc.) et qui est Øtabli dans un but prØcis (Øchanger une clØ symØtrique, s’assurer de l’identitØ de son interlocuteur, etc.). Les di Øren ts types d’interlocuteurs qui apparaissent dans la description du protocole sont appelØs des principaux, par opposition aux participants qui sont les entitØs instanciant ces principaux dans une session du protocole (i.e. une exØcution rØelle). On emploie parfois les termes plus imagØs de r les et d’acteurs. En plus de la crypto- graphie classique, les protocoles cryptographiques font gØnØralement usage d’autres notions, +par exemple [RSG 01, CJ97] : les fonctions de hachage : elles envoient les messages sur un ensemble ni, relativement petit (quelques dizaines d’octets). Elles ne peuvent par consØquent pas Œtre injectives, mais on les choisit de sorte que les collisions accidentelles soient trŁs peu probables et de sorte que, d’une part, toute modi cation (mŒme minime) du message de dØpart se traduise par un modi cation consØquente dans la valeur retournØe par la fonction de hachage et, d’autre part, que connaissant un message et son image par la de 10
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents