Dolev-Yao-Modell

Das Dolev-Yao-Modell ist ein von Danny Dolev und Andrew Yao vorgeschlagenes formales Modell, in dem interaktive Protokolle beschrieben werden können. Ein solches Modell wird benötigt, um formale Aussagen über solche Protokolle zu treffen. Um solche Aussagen leichter zu treffen, werden vereinfachende Annahmen über die kryptologischen Bestandteile des Protokolls, den Angreifer, das Netzwerk sowie dessen Teilnehmer getroffen. Angewendet wird das Dolev-Yao-Modell in der Kryptologie, um die Sicherheit von Protokollen zu beweisen.

Das ursprüngliche Dolev-Yao-Modell kann in zwei Teile gespalten werden, die auch unabhängig voneinander benutzt werden. Das Dolev-Yao-Angreifermodell ist ein klassisches Angreifermodell, mit der Annahme, dass der Angreifer ein aktiver Teilnehmer des Netzes ist und alle darin verkehrende Nachrichten entweder von ihm versendet oder manipuliert werden. Es formalisiert den Angreifer im Netz, indem es ihm bestimmte Fähigkeiten zuweist. Das algebraische Dolev-Yao-Modell formalisiert die Beschreibung eines Protokolls und ersetzt dabei kryptographische Verfahren durch Elemente von Termalgebren.

Die Umgebung

Das Netzwerk wird durch eine Menge abstrakter Teilnehmer repräsentiert. Diese Teilnehmer brauchen keine Autorisierung und sind durch Kanäle miteinander verbunden, über welche Nachrichten in beide Richtungen versendet werden können. Jederzeit können weitere Teilnehmer diesem Netz beitreten und dort Nachrichten versenden und empfangen. Da weder über die dem Netz zugrunde liegende Technologie wie z. B. WLAN noch über die Art der Teilnehmer etwas ausgesagt wird, ist dieses Modell sehr allgemein und lässt sich auf beliebige Netze anwenden.

Das Angreifermodell

In dem zugrunde liegenden Umgebungsmodell muss man davon ausgehen, dass es auch feindselige Teilnehmer gibt, die nicht nur die versendeten Nachrichten passiv abhören, sondern sich auch aktiv in das Netz einmischen. Dabei muss die Möglichkeit miteinbezogen werden, dass der Angreifer auf dem Weg zwischen zwei Benutzern liegt, also zum Beispiel ein Internetknoten ist, der die Pakete weiterleitet. Das ermöglicht es ihm, Nachrichten zu verändern, neu zu adressieren, zu duplizieren, löschen oder neu hinzuzufügen. Er verfügt auch über Möglichkeiten wie IP-Spoofing. Solche feindseligen Teilnehmer werden in der Kryptologieliteratur als aktive Angreifer bezeichnet. Es kann einen einzigen oder eine Gruppe von Angreifern geben, zu der auch normale Teilnehmer gehören können. Normalerweise werden alle Instanzen, die sich nicht protokollgerecht verhalten, zu einem Angreifer zusammengefasst. Das impliziert, dass sich diese Parteien einen Kanal außerhalb des Netzes teilen, über den sie Informationen austauschen können.

Im Dolev-Yao-Modell wird der Angreifer mit folgenden Eigenschaften charakterisiert:

• Der Angreifer kann jede Nachricht abfangen, die netzintern gesendet wird.
• Der Angreifer ist ein berechtigter Teilnehmer des Netzes und kann somit jedem Teilnehmer Nachrichten senden.
• Der Angreifer hat die Möglichkeit von jedem anderen Teilnehmer Nachrichten zu empfangen.
• Der Angreifer kann seine Nachrichten an andere Instanzen unter einer falschen Identität senden.

Man kann das Modell auch so auffassen, dass jeder Teilnehmer seine Nachricht an den Angreifer schickt, der dann die Möglichkeit hat, sie zu verändern, zu löschen, zu duplizieren oder an einen anderen als den beabsichtigten Empfänger zu schicken.

Das algebraische Modell

Dolev und Yao modellieren eine asymmetrische Verschlüsselungsfunktion für einen Benutzer $X$ als einen abstrakten Operator $E_{X}$ und die dazugehörige Entschlüsselungsfunktion als $D_{X}$. Die einzigen geforderten Eigenschaften sind, dass die Hintereinanderausführung dieser Funktionen die Identische Abbildung ist ($D_{X}E_{X}=E_{X}D_{X}=1$), und dass aus $E_{X}(M)$ keine Informationen über $M$ gefolgert werden können. Diese Darstellung idealisiert konkrete Verschlüsselungen. Während ein Angreifer in der realen Welt immer Bitfolgen hat, die er manipulieren kann, hat ein Angreifer im Modell nur ein Symbol, mit dem er nichts anfangen kann, außer es zu entschlüsseln, wenn er den richtigen Schlüssel kennt. Er hat auch nicht die Möglichkeit, den Schlüssel zu raten. Auch alle anderen verwendeten kryptographischen Funktionen werden auf diese Weise dargestellt. Das erlaubt es, ein Protokoll „an sich“ als sicher zu beweisen, ohne auf eventuelle Schwächen der kryptographischen Primitive einzugehen, erzwingt aber auch gesonderte Untersuchungen, inwieweit ein Sicherheitsbeweis im algebraischen Modell auf ein reales Protokoll übertragbar ist (Soundness). Angriffe gegen die idealisierten kryptographischen Primitive werden im Modell nicht erfasst und können daher auch nicht ohne weitere Betrachtungen ausgeschlossen werden.

Beispiel

Der unauthentifizierte Diffie-Hellman-Schlüsselaustausch ist im Dolev-Yao-Modell unsicher, weil in diesem Modell ein Man-in-the-middle-Angriff möglich ist. Der Angreifer kann die von den Teilnehmern gesendeten Nachrichten durch eigene ersetzen.

Literatur

• Danny Dolev, Andrew Yao: On the security of public key protocols. In: IEEE trans. on Information Theory. IT-29, 1983, S. 198–208 (cs.huji.ac.il [PDF; 1,8 MB]). 
• Sergey Kovalev: Angreifermodelle für Sensornetze. 2009 (skovalev.de [PDF; 217 kB] Seminararbeit). 
• Michael Backes, Birgit Pfitzmann, Michael Waidner: Soundness Limits of Dolev-Yao Models. In: Workshop on Formal and Computational Cryptography (FCC'06), affiliated with ICALP'06. 2006 (uni-saarland.de). 
• Wenbo Mao: A structured operational modelling of the dolev-yao threat model. 2009 (citeseerx.ist.psu.edu [PDF]).