[PDF] Rapport de Projet de Fin d'Etude Construction d'attaques pour les protocoles cryptographiques

Introduction
I Pr¶ esentation g¶ en¶ erale
1 Les protocoles cryptographiques
1.1 Primitives cryptographiques . . . . . . . . . . . . . . . . . . . . . .
1.1.1 Chi®rement . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.1.2 Concat¶ enation . . . . . . . . . . . . . . . . . . . . . . . . .
1.1.3 Nonces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Les agents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3 Propri¶ et¶ es de s¶ ecurit¶ e . . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Di±cult¶ es de la veri¯cation . . . . . . . . . . . . . . . . . . . . . .
1.5 Approches pour la v¶ eri¯cation . . . . . . . . . . . . . . . . . . . . .
2 L'outil de v¶ eri¯cation Hermes
2.1 Architecture et caract¶ eristiques de l'outil . . . . . . . . . . . . . . .
2.2 Principe de l'outil . . . . . . . . . . . . . . . . . . . . . . . . . . .
II M¶ ethode de V¶ eri¯cation
3 Pr¶ eliminaires
3.1 T ermes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4 Les protocoles cryptographiques : mod¶ elisation et abstraction
4.1 Mod¶ elisation des protocoles cryptographiques . . . . . . . . . . . .
4.1.1 Messages . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.2 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.3 Mod¶ elisation de l'intrus . . . . . . . . . . . . . . . . . . . .
4.1.4 S¶ emantique op¶ erationnelle . . . . . . . . . . . . . . . . . . .
Download