Bibliographie & annexes
Présentation
RÉSUMÉ
Le développement des technologies de communication a considérablement augmenté le besoin de sécuriser les réseaux informatiques. Utilisés notamment lors de transactions commerciales en ligne, les protocoles cryptographiques constituent des règles d’échange basées sur le cryptage des messages. Cet article présente les propriétés de sécurité assurées par ces protocoles cryptographiques, l’approche nécessaire de modélisation et leur analyse à l’aide de méthodes formelles.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
Auteur(s)
-
Véronique CORTIER : Chargée de recherche CNRS au LORIA (Laboratoire lorrain de recherche en informatique et ses applications)
INTRODUCTION
Les protocoles cryptographiques sont de courts programmes d’échange de messages basés sur le cryptage. Ils sont destinés à la sécurisation des réseaux informatiques. Ils sont notoirement difficiles à concevoir et à analyser. L’application de méthodes formelles a désormais fait ses preuves pour la détection de faille et la preuve de sécurité.
L'expertise technique et scientifique de référence
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Mathématiques
(202 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Résultats et limites4. Modélisation
Pour décrire les protocoles, nous avons jusqu’ici utilisé une représentation intuitive. Cette présentation est en fait très ambiguë car seul le déroulement normal du protocole est décrit. Pour le protocole de Needham-Schroeder, on ne sait pas si le deuxième agent teste si le nonce reçu est bien un nonce, ce qu’il fait si le message n’est pas de la forme attendue ni surtout ce qu’est exactement la « forme attendue » par l’agent.
L’étude des protocoles cryptographiques commence donc par une première étape de modélisation. Depuis quatre années environ, de nombreux modèles dédiés aux protocoles se sont développés. Le modèle choisi ici est basé sur un système de déduction.
4.1 Hypothèse du chiffrement parfait
Dans le cadre de la vérification des protocoles cryptographiques, une hypothèse très classique est celle du chiffrement parfait. Une telle hypothèse assure en particulier qu’il est impossible de décrypter un message chiffré sans avoir la clef correspondante à l’algorithme de déchiffrement.
Bien sûr, cette hypothèse ne correspond pas à la réalité : certains algorithmes de chiffrement permettent à l’intrus de connaître un message m à partir de son chiffré {m }k , dès qu’il a une connaissance partielle de m (le début du message, par exemple) ou s’il possède d’autres messages chiffrés avec la même clef k . Cependant, comme nous l’avons vu précédemment, de nombreuses attaques de protocoles ne reposent absolument pas sur la façon dont sont chiffrés les messages mais consistent tout simplement à rejouer un vieux message ou à mélanger plusieurs sessions. Il s’agit donc de vérifier les protocoles cryptographiques sans tenir compte des éventuelles failles dues au chiffrement. Il reste ensuite aux cryptologues la tâche d’assurer la quasi-inviolabilité d’un message chiffré. Cette hypothèse sera à nouveau discutée au paragraphe 5.2...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Mathématiques
(202 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Modélisation
BIBLIOGRAPHIE
-
(1) - ASOKAN (N.), SHOUP (V.), WAIDNER (M.) - Optimistic fair exchange of digital signatures. - In Advances in Cryptology – Eurocrypt ’98, vol. 1403 of LNCS, p. 591-606 (1998).
-
(2) - BELLARE (M.), DESAI (A.), POINTCHEVAL (D.), ROGAWAY (P.) - Relations among notions of security for public-key encryption schemes. - In Crypto ’98 : Proc. of the 18th Annual International Cryptology Conference on Advances in Cryptology, vol. 1462 of LNCS, p. 26-45. Springer-Verlag (1998).
-
(3) - BURROWS (M.), ABADI (M.), NEEDHAM (R.) - A logic of authentication. - In Proc. of the Royal Society, vol. 426 of Series A, p. 233-271 (1989).
-
(4) - CLARK (J.) , JACOB (J.) - A survey of authentication protocol literature. - http://www.cs.york.ac.uk/jac/papers/drareviewps.ps (1997).
-
(5) - CORTIER (V.) - Vérification automatique des protocoles cryptographiques. - PhD thesis, École normale supérieure de Cachan, France, mars 2003.
-
...
WARINSCHI (B.) - On the computational soudness of formal analysis of cryptographic protocols. - University of California San Diego (2004).
VANACKÈRE (V.) - Trust : un système de vérification automatique de protocoles cryptographiques. - Informatique. Université Aix-Marseille (2004).
LAZAR (L.) - Méthodes algorithmiques de vérification des protocoles cryptographiques. - Université Joseph Fourier Grenoble (2004).
CORTIER (V.) - Vérification automatique des protocoles cryptographiques. - École normale supérieure de Cachan (2003).
ROGER (M.) - Raffinements de la résolution et vérification de protocoles cryptographiques. - ENS Cachan (2003).
TURUANI (M.) - Sécurité des protocoles cryptographiques : décidabilité et complexité. - Université Henri Poincaré. Nancy I (2003).
CHEVALIER (Y.) - Résolution de problèmes d’accessibilité pour la compilation et la validation de protocoles cryptographiques. - Université Henri Poincaré. Nancy I (2003).
RAYNAL (F.) - Études d’outils pour la dissimulation d’information : approches fatales, protocoles d’évaluation et protocoles cryptographiques. - Université Paris Sud (2002).
HAUT DE PAGE
Plate-forme d'outils AVISPA
http://www.avispa-project.org/
Plate-forme d'outils EVA
Présentation du projet PROUVÉ
http://www.lsv.ens-cachan.fr/prouve/
Présentation...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Mathématiques
(202 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
