Le protocole Needham-Schroeder et ses attaques

Le protocole de Needham-Schroeder (1978) fut l’une des premières tentatives formelles de conception d’un protocole d’authentification cryptographique faisant appel à un tiers de confiance (TTP). L’objectif était de permettre à deux parties, Alice et Bob, de s’authentifier mutuellement et d’établir une clé de session partagée à l’aide d’un serveur d’authentification (AS) de confiance, qui partage des clés à long terme avec chaque entité. Le protocole est antérieur à l’infrastructure à clés publiques, mais il a introduit des concepts — des valeurs de fraîcheur et la distribution de clés par l’intermédiaire d’un serveur de confiance — qui restent essentiels dans des protocoles modernes comme Kerberos. La compréhension de NS et de ses failles a façonné tout le domaine de l’analyse des protocoles.

Le protocole NS à clé symétrique se déroule en cinq étapes. (1) Alice envoie {A, B, Na} à l’AS pour demander une clé de session destinée à communiquer avec Bob. (2) L’AS répond à Alice avec {Na, B, Kab, {Kab, A}_Kb}_Ka : une clé de session Kab et un jeton destiné à Bob, le tout chiffré avec la clé à long terme Ka d’Alice. (3) Alice transmet à Bob le jeton {Kab, A}_Kb. (4) Bob déchiffre le jeton, en extrait Kab et envoie {Nb}_Kab à Alice (un défi). (5) Alice répond {Nb-1}_Kab, prouvant qu’elle détient Kab. La valeur de fraîcheur Nb empêche la relecture de l’étape 4. Ce protocole est vulnérable à une attaque par rejeu connue, exploitée par Denning et Sacco (1981).

Denning et Sacco (1981) ont découvert une faille : la réponse de l’AS à l’étape 2 n’est pas fraîche, car elle ne contient ni horodatage ni valeur de fraîcheur généré par le serveur. Un attaquant, Mallory, qui avait précédemment intercepté une ancienne clé de session Kab (en compromettant une session passée), peut rejouer l’ancien jeton {Kab, A}_Kb auprès de Bob à tout moment ultérieur. Bob, recevant ce qui semble être un jeton légitime d’Alice, utilise la clé compromise Kab pour la session. La correction proposée par Denning et Sacco consiste à ajouter un horodatage à la réponse de l’AS et au jeton. Cette correction a été adoptée dans Kerberos : des horodatages sont intégrés aux jetons afin de limiter leur durée de validité.

Le protocole NS à clé publique (également conçu en 1978) a été conçu pour l’authentification mutuelle de deux parties au moyen de la cryptographie à clé publique. (1) Alice envoie {Na, A}_PKb à Bob (la valeur Na chiffrée avec la clé publique de Bob). (2) Bob répond {Na, Nb}_PKa (les deux valeurs de fraîcheur, chiffrées avec la clé publique d’Alice). (3) Alice répond {Nb}_PKb (elle renvoie la valeur de Bob chiffrée avec sa clé publique). Après cet échange, les deux parties détiennent les deux valeurs (Na, Nb) et peuvent dériver une clé de session. Le protocole a semblé sûr pendant 17 ans, jusqu’à l’attaque de Lowe en 1995.

Gavin Lowe (1995) a découvert une faille critique à l’aide du vérificateur de modèles FDR (« échecs du raisonnement compositionnel »). Mallory peut se faire passer pour Bob auprès d’Alice tout en relayant les messages à un Bob honnête. Étape 1 : Alice envoie {Na, A}_PKm à Mallory, pensant communiquer avec Bob. Mallory transmet {Na, A}_PKb à Bob. Étape 2 : Bob répond {Na, Nb}_PKa, que Mallory déchiffre puis rechiffre pour Alice : {Na, Nb}_PKa. Alice déchiffre le message et en extrait Nb. Étape 3 : Alice envoie {Nb}_PKm, pensant que le message est destiné à Bob. Mallory le déchiffre et transmet {Nb}_PKb à Bob. Bob croit avoir terminé une authentification mutuelle avec Alice, mais Alice s’authentifie en réalité auprès de Mallory. La correction consiste à ce que Bob inclue sa propre identité à l’étape 2 : {Na, Nb, B}_PKa.

La correction de Lowe apportée au protocole NSPK est simple, mais profonde : la réponse de Bob à l'étape 2 doit inclure l'identité B de Bob, ce qui donne {Na, Nb, B}_PKa. Ainsi, lorsqu'Alice reçoit la réponse, elle vérifie que l'identité incluse B correspond à la partie qu'elle avait l'intention de contacter. Mallory ne peut pas substituer sa propre réponse : il lui faudrait la clé privée d'Alice pour construire un {Na, Nb, M}_PKa valide qui passe la vérification d'Alice. Cette leçon est généralisée sous le nom de principe de Needham-Abadi : les messages d'authentification doivent lier explicitement l'identité de l'expéditeur, sans s'appuyer uniquement sur le contexte pour l'identifier.

La découverte par Lowe de la faille de NSPK a été facilitée par le vérificateur de modèles FDR (Failures-Divergences Refinement), qui explore exhaustivement toutes les exécutions possibles du protocole, y compris les interventions d'un adversaire. Elle a conduit au développement d'outils d'analyse formelle des protocoles : Proverif (fondé sur le calcul pi appliqué) peut démontrer ou réfuter les propriétés d'authentification et de confidentialité dans un nombre infini de sessions. Tamarin Prover utilise la réécriture de multiensembles et prend en charge des protocoles complexes comme TLS 1.3 et Signal. AVISPA et Scyther sont d'autres outils. Les conceptions modernes de protocoles (TLS 1.3, Signal, Noise) font l'objet d'une vérification formelle avant leur déploiement — un héritage direct de l'épisode NS/Lowe.

Les attaques contre NS ont clarifié la distinction entre les objectifs d'authentification. Authentification de l'entité : prouver qu'une partie est actuellement active et participe au protocole (la fraîcheur est importante). Authentification de l'origine des données : prouver qu'un message précis a été créé par une partie précise (cela n'implique pas nécessairement la vivacité). L'attaque de Lowe compromet l'authentification de l'entité : Alice croit s'authentifier auprès de Bob, mais elle s'authentifie en réalité auprès de Mallory, qui relaie les échanges vers Bob. Les spécifications modernes des protocoles énoncent précisément les objectifs : "Alice est authentifiée auprès de Bob en tant qu'initiatrice de cette session." Des objectifs vagues conduisent à des spécifications ambiguës qui passent une revue informelle, mais échouent à l'analyse formelle.

Une autre catégorie d'attaques liées à NS est l'attaque par réflexion : Mallory renvoie à Alice des messages d'Alice. Si le protocole est symétrique (les deux parties utilisent la même clé et le même format de message), Alice peut accepter son propre défi comme une réponse valide de Bob. Défense : utiliser des sens de clés différents (des clés distinctes de chiffrement et de déchiffrement pour chaque sens) ou inclure des indicateurs de rôle dans les messages (le chiffreur inclut "I am initiator" dans le message). Les protocoles modernes comme TLS incluent des chaînes d'étiquettes spécifiques au rôle dans les clés dérivées par HKDF (avec "c e traffic" pour le client et "s hs traffic" pour le serveur) afin d'empêcher la réflexion.

Les attaques par entrelacement combinent des messages provenant de plusieurs sessions concurrentes du protocole afin de forger une authentification. Si Alice exécute deux sessions simultanées, Mallory peut mélanger des messages des deux sessions pour créer une session combinée cohérente, mais invalide, dans laquelle Mallory est authentifié. Défense : liaison à la session — chaque message doit être lié cryptographiquement au contexte de sa session (par exemple, inclure un identifiant de session ou utiliser une clé unique par session). TLS empêche l'entrelacement au moyen du message Finished, qui est un MAC calculé sur la transcription complète de la session actuelle. Tout message entrelacé modifie la transcription et invalide la valeur de Finished.

Les protocoles de Needham-Schroeder ont directement influencé la conception de Kerberos (horodatages pour empêcher le rejeu, repris de la correction de Denning-Sacco), de TLS (le MAC du message Finished sur la transcription empêche l'entrelacement et la réflexion), du protocole Signal (liaison à la session via l'état du mécanisme à cliquet) et du cadre de protocoles Noise (liaison de l'identité dans les schémas d'établissement). Les attaques contre NS ont établi que les arguments de sécurité informels sont insuffisants — chaque protocole doit être analysé face à un adversaire actif qui contrôle le réseau et peut rejouer, réordonner et modifier les messages. Ce modèle d'adversaire (Dolev-Yao) est désormais standard dans la vérification formelle des protocoles.

Quel changement simple Lowe a-t-il proposé pour corriger la vulnérabilité du protocole NS à clé publique ?

Le protocole symétrique de Needham-Schroeder (1978) a introduit la distribution de clés de session fondée sur un TTP. L'attaque de Denning-Sacco (1981) a révélé une vulnérabilité au rejeu — corrigée par les horodatages dans Kerberos. Le protocole NSPK à clé publique a subi une attaque MITM découverte par Lowe (1995) grâce à la vérification de modèles — corrigée par l'inclusion de l'identité de l'expéditeur dans les messages. Ces attaques ont établi la vérification formelle (Proverif, Tamarin) comme essentielle à la conception des protocoles. Leçons clés : les messages doivent lier l'identité de l'expéditeur, les sessions doivent être isolées les unes des autres, les attaques par réflexion sont empêchées par la dérivation directionnelle des clés et les attaques par entrelacement par des MAC de transcription.