Der Analyse-APA

Die Analyse des Protokolls läuft auf einem speziell dafür zu schaffenden Analyse-APA. Dazu enthält er für jeden Agenten $P$, welcher sich gemäß der Protokollspezifikation verhält einen elementaren Automaten mit den benachbarten Zustandskomponenten $State_P$, $Symkeys_P$, $Asmykeys_P$, $Goals_P$ und $Network$. Zusätzlich existiert noch eine Zustandskomponente $Global$, welche von allen Agenten benutzt werden kann um z.B. Zufallszahlen zu generieren. Weiterhin gibt es einen elementaren Automaten $G$, welcher Zugriff auf $Network$, $Global$ und sämtliche $State$-Komponenten der anderen Agenten (inklusive des Angreifers) hat. Durch $G$ können Zustandsübergänge beeinflusst werden, für das Needham-Schroeder Protokoll wird $G$ allerdings nicht benötigt.

Zusätzlich wird im Analyse-APA auch ein Angreifer $E$ spezifiziert. Also werden für $E$ ein elementarer Automat und die zu $E$ benachbarten Zustandskomponenten $State_E$, $Symkeys_E$, $Asymkeys_E$, und $Sent_E$ (um mehrfaches Abschicken derselben Nachricht zu vermeiden) in den APA eingefügt. Der Angreifer hat Zugriff auf $Network$ und $Global$. Anders als die restlichen Agenten kann der Angreifer jedes Tupel aus $Network$ entfernen, auch wenn er nicht der Adressat ist. Er kann die Bestandteile der Nachricht als Wissen in seine Zustandskomponente übernehmen, und er kann dem eigentlichen Adressaten eine eigene Nachricht zukommen lassen (d.h. der Angreifer weiß auch an wen die abgefangene Nachricht gehen sollte). Das Wissen des Angreifers kann rekursiv definiert werden:

1. Der Angreifer kennt alle Daten, die im Anfangszustand in seinen Komponenten stehen.
2. Der Angreifer kennt alle Agenten, die als Adressaten abgefangener Nachrichten auftraten, d.h. als erste Komponente der Paare aus $Network$.
3. Der Angreifer kennt alle von ihm gelesenen Nachrichten, d.h. die zweiten Komponenten der Paare aus $Network$.
4. Der Angreifer kennt alle Bestandteile der von ihm gelesenen Nachrichten (verschlüsselter Text wird dabei als ein atomarer Bestandteil betrachtet).
5. Der Angreifer kennt alle Nachrichten, die er durch Konkatenation generieren kann.
6. Der Angreifer kann neue Nachrichten durch Anwenden von $encrypt$ generieren (hierbei kann jede ihm bekannte Nachricht als Schlüssel dienen).
7. Der Angreifer kann Zufallszahlen erzeugen.
8. Der Angreifer kennt jeden Klartext, den er durch Anwendung von $decrypt$ auf eine Nachricht erzeugen kann, wenn er den passenden Schlüssel kennt.
9. Der Angreifer kann die symbolische Funktion $sub$ auf Nachrichten anwenden.