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.