Das Needham-Schroeder-Protokoll und Angriffe

Das Needham-Schroeder-Protokoll (1978) war einer der ersten formalen Versuche, ein kryptografisches Authentifizierungsprotokoll mit einer vertrauenswürdigen dritten Instanz (TTP) zu entwerfen. Das Ziel bestand darin, zwei Parteien, Alice und Bob, gegenseitig zu authentifizieren und mithilfe eines vertrauenswürdigen Authentication Server (AS), der mit jedem Principal langfristige Schlüssel teilt, einen gemeinsamen Sitzungsschlüssel einzurichten. Das Protokoll entstand vor der Public-Key-Infrastruktur, führte jedoch Konzepte wie Nonces zur Gewährleistung der Aktualität und die Schlüsselverteilung über einen vertrauenswürdigen Server ein, die auch für moderne Protokolle wie Kerberos zentral sind. Das Verständnis des NS-Protokolls und seiner Fehler hat die gesamte Protokollanalyse geprägt.

Das symmetrische NS-Schlüsselprotokoll läuft in fünf Schritten ab. (1) Alice sendet {A, B, Na} an den AS und fordert einen Sitzungsschlüssel für die Kommunikation mit Bob an. (2) Der AS antwortet Alice mit {Na, B, Kab, {Kab, A}_Kb}_Ka – einem Sitzungsschlüssel Kab und einem Ticket für Bob, wobei alles mit Alices langfristigem Schlüssel Ka verschlüsselt ist. (3) Alice leitet das Ticket {Kab, A}_Kb an Bob weiter. (4) Bob entschlüsselt das Ticket, extrahiert Kab und sendet {Nb}_Kab als Challenge an Alice. (5) Alice antwortet mit {Nb-1}_Kab und weist damit nach, dass sie Kab besitzt. Die Nonce Nb verhindert die Wiederholung von Schritt 4. Bei diesem Protokoll ist ein bekannter Replay-Angriff möglich, den Denning und Sacco (1981) ausnutzten.

Denning und Sacco (1981) entdeckten einen Fehler: Die Antwort des AS in Schritt 2 ist nicht aktuell, da sie keinen vom Server beigesteuerten Zeitstempel und keine Nonce enthält. Ein Angreifer namens Mallory, der einen alten Sitzungsschlüssel Kab zuvor abgefangen hat, indem er eine frühere Sitzung kompromittierte, kann das alte Ticket {Kab, A}_Kb zu jedem späteren Zeitpunkt an Bob erneut senden. Bob erhält ein Ticket, das scheinbar von Alice stammt, und verwendet den kompromittierten Schlüssel Kab für die Sitzung. Die Lösung von Denning und Sacco bestand darin, der Antwort des AS und dem Ticket einen Zeitstempel hinzuzufügen. Dieser Ansatz wurde in Kerberos übernommen – Zeitstempel werden in Tickets eingebettet, um deren Gültigkeitszeitraum zu begrenzen.

Das NS-Protokoll mit öffentlichen Schlüsseln (ebenfalls 1978) wurde für die gegenseitige Authentifizierung zweier Parteien mithilfe von Public-Key-Kryptografie entwickelt. (1) Alice sendet {Na, A}_PKb an Bob (die unter Bobs öffentlichem Schlüssel verschlüsselte Nonce Na). (2) Bob antwortet mit {Na, Nb}_PKa (beide Nonces, mit Alices öffentlichem Schlüssel verschlüsselt). (3) Alice antwortet mit {Nb}_PKb (sie sendet Bobs Nonce, mit seinem öffentlichen Schlüssel verschlüsselt, zurück). Nach diesem Austausch verfügen beide Parteien über beide Nonces (Na, Nb) und können einen Sitzungsschlüssel ableiten. Das Protokoll galt 17 Jahre lang als sicher – bis zu Lowes Angriff von 1995.

Gavin Lowe (1995) entdeckte mithilfe des Modelcheckers Failures in Compositional Reasoning (FDR) einen kritischen Fehler. Mallory kann sich gegenüber Alice als Bob ausgeben, während er Nachrichten an einen ehrlichen Bob weiterleitet. Schritt 1: Alice sendet {Na, A}_PKm an Mallory, da sie glaubt, mit Bob zu kommunizieren. Mallory leitet {Na, A}_PKb an Bob weiter. Schritt 2: Bob antwortet mit {Na, Nb}_PKa, das Mallory entschlüsselt und für Alice erneut verschlüsselt: {Na, Nb}_PKa. Alice entschlüsselt die Nachricht und extrahiert Nb. Schritt 3: Alice sendet {Nb}_PKm, da sie glaubt, die Nachricht gehe an Bob. Mallory entschlüsselt sie und leitet {Nb}_PKb an Bob weiter. Bob glaubt, die gegenseitige Authentifizierung mit Alice abgeschlossen zu haben – tatsächlich authentifiziert sich Alice jedoch gegenüber Mallory. Die Lösung: In Schritt 2 muss Bob seine eigene Identität aufnehmen: {Na, Nb, B}_PKa.

Lowes Lösung für das NSPK-Protokoll ist einfach, aber grundlegend: Bobs Antwort in Schritt 2 muss Bobs Identität B enthalten und wird dadurch zu {Na, Nb, B}_PKa. Wenn Alice die Antwort erhält, prüft sie nun, ob die enthaltene Identität B mit der Partei übereinstimmt, die sie kontaktieren wollte. Mallory kann seine eigene Antwort nicht einschleusen – er müsste Alices privaten Schlüssel besitzen, um ein gültiges {Na, Nb, M}_PKa zu erstellen, das Alices Prüfung besteht. Diese Erkenntnis wird als Needham-Abadi-Prinzip verallgemeinert: Authentifizierungsnachrichten müssen die Identität des Absenders ausdrücklich binden und dürfen sich bei der Identifizierung nicht allein auf den Kontext verlassen.

Lowes Entdeckung der Schwachstelle im NSPK-Protokoll wurde durch den Modellprüfer FDR (Failures-Divergences Refinement) unterstützt, der alle möglichen Protokollausführungen einschließlich Eingriffen durch Angreifer erschöpfend untersucht. Dies führte zur Entwicklung formaler Werkzeuge für die Protokollanalyse: Proverif (basierend auf dem angewandten Pi-Kalkül) kann Authentifizierungs- und Geheimhaltungseigenschaften für unendlich viele Sitzungen beweisen oder widerlegen. Tamarin Prover verwendet Multimengen-Umschreibung und unterstützt komplexe Protokolle wie TLS 1.3 und Signal. AVISPA und Scyther sind weitere Werkzeuge. Moderne Protokollentwürfe wie TLS 1.3, Signal und Noise werden vor ihrer Bereitstellung einer formalen Verifikation unterzogen – ein direktes Vermächtnis der NS/Lowe-Episode.

Die NS-Angriffe haben den Unterschied zwischen verschiedenen Authentifizierungszielen verdeutlicht. Entitätsauthentifizierung bedeutet nachzuweisen, dass eine Partei aktuell aktiv ist und am Protokoll teilnimmt (Frische ist entscheidend). Datenursprungsauthentifizierung bedeutet nachzuweisen, dass eine bestimmte Nachricht von einer bestimmten Partei erstellt wurde (beides muss nicht zugleich die Lebendigkeit der Partei belegen). Lowes Angriff kompromittiert die Entitätsauthentifizierung: Alice glaubt, sie authentifiziere sich gegenüber Bob, tatsächlich authentifiziert sie sich jedoch gegenüber Mallory, der Nachrichten an Bob weiterleitet. Moderne Protokollspezifikationen formulieren ihre Ziele präzise: „Alice ist gegenüber Bob als Initiatorin dieser Sitzung authentifiziert.“ Vage Ziele führen zu mehrdeutigen Spezifikationen, die eine informelle Prüfung bestehen, aber bei der formalen Analyse scheitern.

Eine weitere Klasse von Angriffen im Zusammenhang mit NS sind Reflexionsangriffe: Mallory sendet Nachrichten von Alice an Alice zurück. Wenn das Protokoll symmetrisch aufgebaut ist (beide Parteien verwenden denselben Schlüssel und dasselbe Nachrichtenformat), kann Alice ihre eigene Challenge als gültige Antwort von Bob akzeptieren. Als Schutz können unterschiedliche Schlüsselrichtungen verwendet werden (getrennte Verschlüsselungs- und Entschlüsselungsschlüssel für jede Richtung), oder die Nachrichten enthalten Rollenkennungen (der Verschlüsselnde fügt der Nachricht „I am initiator“ hinzu). Moderne Protokolle wie TLS verwenden rollenspezifische Bezeichner in von HKDF abgeleiteten Schlüsseln (mit „c e traffic“ für den Client und „s hs traffic“ für den Server), um Reflexionen zu verhindern.

Interleaving-Angriffe kombinieren Nachrichten aus mehreren gleichzeitig laufenden Protokollsitzungen, um eine Authentifizierung zu fälschen. Wenn Alice zwei Sitzungen gleichzeitig ausführt, kann Mallory Nachrichten aus beiden Sitzungen vermischen und so eine konsistente, aber ungültige kombinierte Sitzung erzeugen, in der Mallory authentifiziert wird. Eine Gegenmaßnahme ist die Sitzungsbindung: Jede Nachricht muss kryptografisch an den Kontext ihrer Sitzung gebunden sein (beispielsweise durch eine Sitzungs-ID oder einen eindeutigen Schlüssel pro Sitzung). TLS verhindert Interleaving durch die Finished-Nachricht, die ein MAC über den vollständigen Protokollverlauf der aktuellen Sitzung ist. Jede eingeschobene Nachricht verändert den Protokollverlauf und macht den Finished-Wert ungültig.

Die Needham-Schroeder-Protokolle haben das Design von Kerberos (Zeitstempel zur Verhinderung von Replay-Angriffen, übernommen aus der Lösung von Denning und Sacco), TLS (der Finished-MAC über den Protokollverlauf verhindert Interleaving und Reflexionen), dem Signal Protocol (Sitzungsbindung durch den Ratchet-Zustand) und dem Noise Protocol Framework (Identitätsbindung in Handshake-Mustern) direkt beeinflusst. Die NS-Angriffe haben gezeigt, dass informelle Sicherheitsargumente nicht ausreichen: Jedes Protokoll muss gegen einen aktiven Angreifer analysiert werden, der das Netzwerk kontrolliert und Nachrichten wiedergeben, umordnen und verändern kann. Dieses Angreifermodell (Dolev-Yao) ist heute Standard bei der formalen Protokollverifikation.

Welche einfache Änderung schlug Lowe vor, um die Schwachstelle des NS-Public-Key-Protokolls zu beheben?

Das symmetrische Needham-Schroeder-Protokoll (1978) führte die Verteilung von Sitzungsschlüsseln über eine vertrauenswürdige dritte Partei (TTP) ein. Der Denning-Sacco-Angriff (1981) deckte eine Replay-Schwachstelle auf, die durch Zeitstempel in Kerberos behoben wurde. Das NSPK-Public-Key-Protokoll war einem von Lowe (1995) mithilfe von Modellprüfung entdeckten Man-in-the-Middle-Angriff ausgesetzt, der durch die Aufnahme der Absenderidentität in die Nachrichten behoben wurde. Diese Angriffe etablierten die formale Verifikation (Proverif, Tamarin) als unverzichtbar für das Protokolldesign. Die wichtigsten Lehren: Nachrichten müssen die Identität des Absenders binden, Sitzungen müssen voneinander isoliert sein, Reflexionsangriffe werden durch gerichtete Schlüsselableitung verhindert und Interleaving-Angriffe durch MACs über den Protokollverlauf.