Dolev-Yao-Angreifermodell und symbolische Kryptografie

Das 1983 von Danny Dolev und Andrew Yao vorgeschlagene Dolev-Yao-Modell ist das Standard-Angreifermodell für die symbolische Protokollanalyse. Der Angreifer kontrolliert das gesamte Netzwerk.

Der Dolev-Yao-Angreifer kann jede Nachricht abfangen, Nachrichten speichern, alte Nachrichten wiedergeben und aus bekannten Komponenten neue Nachrichten fälschen, kann aber die zugrunde liegenden kryptografischen Primitive nicht brechen.

In symbolischen Modellen ist Verschlüsselung eine perfekte Blackbox: Der Angreifer kann ohne den Schlüssel nicht entschlüsseln, große Zahlen nicht faktorisieren und keine Signaturen fälschen. Das vereinfacht die Analyse, kann jedoch Angriffe auf Implementierungsebene übersehen.

Nachrichten werden als Terme modelliert: enc(k, m), sig(sk, m), hash(m), pair(a, b). Der Angreifer kennt bestimmte Terme und leitet mithilfe definierter Regeln (Ableitungsregeln) neue daraus ab.

Das Wissen des Angreifers ist unter Ableitung abgeschlossen: Wenn er enc(k,m) und k kennt, kann er m ableiten. Kennt er pair(a,b), kann er a und b ableiten. Die Hülle des Ausgangswissens umfasst alles, was der Angreifer lernen kann.

Die Protokollsicherheit wird folgendermaßen formuliert: „Das Wissen des Angreifers enthält in keinem erreichbaren Zustand jemals das Geheimnis s.“ Geheimhaltung = Erreichbarkeit. Authentifizierung = das Fehlen bestimmter schädlicher Trace-Muster.

Zwei-Parteien-Protokoll: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. In der Termalgebra sendet Alice enc(pubkey_B, pair(Na, A)). Wir überprüfen, dass nach der Ausführung nur B Na kennt.

Der Applied Pi-Kalkül (Abadi & Fournet 2001) ist eine Prozessalgebra zur Modellierung von Protokollen. Prozesse kommunizieren über Kanäle; der Angreifer kontrolliert öffentliche Kanäle. ProVerif und Tamarin verwenden diesen Formalismus.

Ein Protokoll, das im Dolev-Yao-Modell sicher ist, kann dennoch rechnerisch unsicher sein, wenn die kryptografische Instanziierung schwach ist. Der Satz zur Computational Soundness (Cortier et al.) überbrückt für bestimmte Klassen von Primitiven die Lücke.

Dolev-Yao kann Folgendes nicht modellieren: algebraische Eigenschaften (z. B. die Kommutativität von XOR), Seitenkanalangriffe, Implementierungsfehler oder probabilistische Fehler. Erweiterungen wie Modelle auf Basis von Gleichungstheorien können einige algebraische Eigenschaften berücksichtigen.

Welche Fähigkeit hat der Dolev-Yao-Angreifer NICHT?

Dolev-Yao gibt dem Angreifer vollständige Kontrolle über das Netzwerk, setzt aber perfekte Kryptografie voraus. Nachrichten sind Terme in einer Algebra; Sicherheit ist eine Erreichbarkeitseigenschaft. Der Applied Pi-Kalkül stellt die formale Sprache bereit. Einschränkungen: Algebraische Beziehungen, Seitenkanäle und Implementierungsfehler können nicht modelliert werden.