Les Newsletters Interstices
© Inria / Photo G. Scagnelli.
    Niveau intermédiaire
    Niveau 2 : Intermédiaire

    Vérifier la sécurité de nos communications

    Sécurité & Vie privée
    Quand nous échangeons des messages numériques, nous sommes persuadés de communiquer avec l'interlocuteur que nous avons choisi. Pour s'en assurer réellement, il faut mettre en place des protocoles de communication sécurisés. Mais même en utilisant des canaux sûrs, cela peut ne pas suffire comme l'illustre l'attaque de G. Lowe dite « de l'homme du milieu ».

    De plus en plus de communications sont dématérialisées du fait de l’essor des moyens de communications numériques : email, messagerie instantanée, commerce en ligne, etc. Afin d’assurer la sécurité de ces échanges, de nombreux protocoles utilisant la cryptographie ont vu le jour. Il existe deux familles d’algorithmes de chiffrement : les algorithmes symétriques comme le chiffrement historique de Vigenère [4] ou AES [7] et les algorithmes asymétriques aussi appelés algorithmes à clé publique comme RSA [10].

    Le chiffrement symétrique

    Dans un chiffrement symétrique, deux personnes souhaitent communiquer de manière chiffrée. Ici Alice et Bob, que nous identifions respectivement par A et B, possèdent la même clé symétrique KAB. Ainsi, comme expliqué sur le dessin ci-dessous, Alice chiffre avec la clé KAB son message puis l’envoie à Bob. Une fois le message chiffré reçu, Bob peut le déchiffrer en utilisant la même clé KAB puis le lire. Ces chiffrements sont dits symétriques car la même clé est utilisée pour chiffrer et déchiffrer.

    Le chiffrement asymétrique

    Le chiffrement asymétrique fonctionne différemment. Chaque participant possède une clé publique et une clé secrète. Pour Alice, nous noterons pub(A) sa clé publique et sk(A) la clé secrète associée. Tous les participants connaissent les clés publiques de tous les autres car elles sont publiées dans des annuaires sur Internet. Chaque participant a intérêt à publier sa clé publique car elle sert à générer des messages chiffrés pour lui. Par exemple, si Alice veut envoyer un message chiffré à Bob, il lui suffit de trouver la clé publique de Bob, pub(B), sur Internet, puis de chiffrer le message avec celle-ci et de l’envoyer à Bob. Une fois le message reçu, Bob utilise la clé secrète sk(B) pour déchiffrer le message. Seul Bob peut lire le message car lui seul possède la clé secrète pour le déchiffrer.

    Le problème de l’échange de clé

    La cryptographie à clé publique permet à une personne d’envoyer une information chiffrée sans aucun échange au préalable, en utilisant par exemple le chiffrement RSA. Malheureusement, toutes les communications ne peuvent pas s’effectuer avec un tel chiffrement. En effet, il faut environ 30 secondes avec un ordinateur de bureau pour chiffrer un message de 10 Mo avec RSA, alors qu’il ne faut que 0,1 secondes pour chiffrer avec AES.

    Afin d’avoir le meilleur des deux mondes, nous allons utiliser la cryptographie à clé publique pour échanger une clé symétrique entre Alice et Bob. Ainsi ils pourront communiquer en toute sécurité en utilisant cette nouvelle clé. Les protocoles cryptographiques permettant cela sont appelés protocoles d’échange de clé.

    Le protocole de Needham-Schroeder

    En 1978, un an après la publication de RSA, le premier chiffrement à clé publique, R. Needham et M. Schroeder [9] proposèrent un protocole d’échange de clé symétrique entre deux participants, Alice et Bob. Ces deux participants veulent échanger en toute sécurité une nouvelle clé symétrique K. Le protocole utilise un algorithme de chiffrement asymétrique et il fonctionne comme suit :

    a) Alice envoie à Bob un message chiffré par la clé publique de Bob, pub(B). Il contient son identité A et un nombre aléatoire NA« fraîchement » choisi par Alice, aussi appelé nonce.
    b) Une fois ce message reçu, Bob choisit une nouvelle clé symétrique, notée pour communiquer avec Alice. Il répond à Alice en envoyant cette nouvelle clé K, ainsi que le nonce NA précédemment reçu, dans un message chiffré par la clé publique d’Alice, pub(A).
    c) Alice confirme à Bob qu’elle a bien reçu le message, en lui renvoyant le K chiffré par pub(B), la clé publique de Bob.

    Une fois le protocole terminé, Alice est convaincue d’avoir effectué une session du protocole avec Bob, car il lui a renvoyé son nonce NA. De même, Bob pense avoir communiqué avec Alice. Ils partagent alors une information commune K qui sera la clé publique utilisée dans leurs communications futures. Ils pensent également qu’ils sont les seuls à connaître la clé symétrique K.

    L’attaque « de l’homme du milieu » de Gavin Lowe

    Ce protocole est célèbre car, dix-sept ans après sa publication, une attaque fut découverte. Elle fit prendre conscience qu’un protocole, dont toutes les informations transmises sont cryptées par un chiffrement asymétrique sûr mais qui utilise un canal de communication accessible à tous, n’est pas nécessairement un échange de messages sûr. De par la conception même du protocole, des informations confidentielles peuvent être découvertes par un intrus.

    Gavin Lowe trouva cette attaque en utilisant un outil automatique de vérification de protocoles cryptographiques [8]. Cette attaque permet à un intrus, appelé Charlie et identifié par C, d’obtenir la clé secrète K échangée par Alice et Bob.

    Cette attaque est un exemple d’intrusion connu sous le nom de « man in the middle », car Charlie est placé entre Alice et Bob. Il joue en parallèle deux sessions du protocole, une avec Alice et une avec Bob. Il peut par exemple se placer entre les deux interlocuteurs qui communiquent en utilisant une communication sans fil, ou bien simplement se placer sur le réseau. Voyons plus précisément comment l’attaque fonctionne.

    Alice commence une session du protocole avec Charlie en suivant la première étape du protocole. Elle utilise la clé publique de Charlie et lui envoie un premier message. Charlie peut alors déchiffrer le message avec sa clé secrète. Il récupère ainsi l’identité d’Alice A et son nonce NA. L’intrus peut ensuite commencer une deuxième session avec Bob, en se faisant passer pour Alice. Il envoie à Bob un message chiffré avec la clé publique de Bob contenant l’identité d’Alice A et le nonce NA, comme l’indique la première étape du protocole.

    D’après le message qu’il a reçu, Bob pense parler en toute sécurité à Alice, alors qu’il communique en fait avec Charlie. Il répond donc, comme l’indique la seconde étape du protocole, en envoyant un message qui contient le nonce NA et la clé symétrique K qu’il vient de générer, et en chiffrant ce message avec la clé publique d’Alice. Charlie ne peut pas le déchiffrer, n’ayant pas la clé secrète d’Alice. Il le transfère donc à Alice.

    Après avoir déchiffré le message reçu, Alice renvoie la clé K comme cela est spécifié dans le protocole. Ainsi Charlie reçoit le message, et le déchiffre, car Alice a utilisé la clé publique de l’intrus. Celui-ci conclut alors le protocole initié avec Bob, en envoyant K chiffré avec la clé publique de Bob.


    Rappelons que le protocole sert à échanger la clé symétrique K entre Alice et Bob. L’intrus connaît maintenant cette clé, il peut alors continuer sans aucun problème à écouter les messages envoyés par Bob à Alice, les déchiffrer et même, se faire passer pour Alice. En effet, il peut répondre à Bob en chiffrant ses réponses grâce à la clé symétrique K.

    Correction de la faille de sécurité

    Afin de corriger cette attaque, il suffit que Bob ajoute son identifiant dans sa première réponse à Alice. Il envoie donc son identifiant B, le nonce NA, et la clé symétrique K. Quand Alice reçoit le message, elle s’aperçoit qu’elle discute avec deux personnes à la fois, car la clé associée à l’identifiant B ne correspond pas à la clé publique de Charlie pub(C). Alice arrête le protocole et empêche l’intrus d’apprendre le secret. L’attaque ne fonctionne plus.

    Vérification formelle pour les protocoles cryptographiques

    Utiliser un algorithme de chiffrement incassable est un prérequis indispensable pour assurer la sécurité mais n’est pas suffisant, comme illustré ci-dessus avec le protocole de Needham-Schroeder. En effet, en combinant plusieurs échanges de messages, un intrus peut obtenir de l’information si le protocole est mal conçu. Par exemple, l’attaque de Gavin Lowe permet de récupérer la clé secrète du chiffrement symétrique. Ce genre d’attaque est appelée attaque logique.

    Pour attaquer un protocole cryptographique, il existe une autre approche, qui consiste à essayer d’obtenir de l’information sur les messages chiffrés échangés, par exemple en les déchiffrant ou en cherchant à obtenir la clé utilisée. Ces attaques sont appelées cryptanalyses et portent sur la sécurité de l’algorithme cryptographique employé [6].

    La sécurité des protocoles de communication utilise des fonctions mathématiques pour chiffrer les messages. Bien que nécessaires, ces techniques n’assurent pas forcément le secret des communications, comme le montre l’attaque sur le protocole de Needham-Schroeder. Construire de tels protocoles de manière sécuritaire n’est pas une tâche facile et dépasse largement les capacités humaines.

    Pour le protocole de communication de Needham-Schroeder qui n’a que trois messages, il a fallu dix-sept ans pour découvrir une attaque, qui une fois présentée semble relativement simple. Sa découverte fut le point de départ de la vérification formelle pour les protocoles cryptographiques. Depuis, les chercheurs ont développé avec succès des techniques de vérification automatique. Ces outils permettent de garantir l’absence de faille de sécurité face à un intrus, ou bien de découvrir des failles et de les corriger.

    Pour vérifier qu’un protocole cryptographique est sûr, il faut modéliser plusieurs éléments : le protocole, la propriété de sécurité et l’attaquant contre lequel le protocole doit être sûr. Chacune de ces étapes nécessite de trouver le bon niveau d’abstraction, c’est-à-dire le bon compromis entre abstraction et efficacité de la vérification. Il existe de nombreux outils de vérification [1, 3, 2, 5], qui permettent aujourd’hui de vérifier automatiquement le secret et l’authentification. Ces outils ont par exemple permis de vérifier un protocole d’échange de mails [11].

    Il reste encore de nombreuses techniques à développer pour vérifier automatiquement les propriétés de sécurité des protocoles à venir de par les nouvelles fonctionnalités désirées, mais aussi la complexité des protocoles et primitives cryptographiques utilisés…

    [1] Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Heám, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michael Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The avispa tool for the automated validation of internet security protocols and applications. In Proceedings of CAV’2005, LNCS 3576, pages 281-285. Springer-Verlag, 2005.

    [2] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proc. CSFW’01, pages 82-96. IEEE Comp. Soc. Press, 2001.

    [3] Bruno Blanchet. Automatic verification of correspondences for security protocols. Journal of Computer Security, 2009.

    [4] François Cayre. Cryptographie, du chiffre et des lettres. Sur Interstices, 21/04/2009.

    [5] C.J.F. Cremers. The Scyther Tool : Verification, falsification, and analysis of security protocols. In Computer Aided Verification, 20th International Conference, CAV, volume 5123/2008 of LNCS, pages 414-418. Springer, 2008.

    [6] Mathieu Cunche. À l’attaque des codes secrets. Sur Interstices, 24/03/2011.

    [7] Joan Daemen and Vincent Rijmen. The Design of Rijndael. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2002.

    [8] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of LNCS, pages 147-166, Berlin, Germany, 1996. Springer-Verlag.

    [9] R. Needham and M. Schroeder. Using encryption for authentification in large networks of computers. Communications of the ACM, 21(12) :993-999, 1978.

    [10] Jonathan Touboul. Nombres premiers et cryptologie : l’algorithme RSA. Sur Interstices, 21/12/2007.

    [11] Martin Abadi, Bruno Blanchet. Computer-assisted verification of a protocol for certified email. In Science of Computer Programming, Volume 58, Issues 1–2, Pages 3-27, 2005.

    Newsletter

    Le responsable de ce traitement est Inria. En saisissant votre adresse mail, vous consentez à recevoir chaque mois une sélection d'articles et à ce que vos données soient collectées et stockées comme décrit dans notre politique de confidentialité

    Niveau de lecture

    Aidez-nous à évaluer le niveau de lecture de ce document.

    Si vous souhaitez expliquer votre choix, vous pouvez ajouter un commentaire (Il ne sera pas publié).

    Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !

    Pascal Lafourcade

    Maître de conférences à l'Université de Clermont Auvergne, membre de l'équipe Réseaux et Protocoles du LIMOS, laboratoire d'informatique de Clermont-Ferrand.

    Voir le profil

    Découvrez le(s) dossier(s) associé(s) à cet article :

    DossierCulture & Société
    Environnement & PlanèteSécurité & Vie privée

    TIPE 2020-2021 : enjeux sociétaux

    DossierCulture & Société
    DonnéesSécurité & Vie privée

    Données – Vie privée

    Ces articles peuvent vous intéresser

    ArticleSécurité & Vie privée
    Culture & Société

    Les méthodes formelles : l’autre arme de la cybersécurité

    Jean Goubault-Larrecq

    Niveau intermédiaire
    Niveau 2 : Intermédiaire