Das Analyse-Szenario

Für ein konkretes zu analysierendes Szenario müssen jetzt noch die teilnehmenden Agenten (inklusive der Rollen die sie übernehmen können), sowie der Startzustand (d.h. der Inhalt sämtlicher Zustandskomponenten am Anfang) spezifiziert werden. In diesem Fall gibt es zwei Agenten $Alice$ (übernimmt Rolle $A$) und $Bob$ (Rolle $B$) und einen Server (Rolle $S$). Des weiteren gibt es einen Angreifer $E$, der nicht an dem Protokoll teilnimmt, d.h. keine der Rollen übernehmen kann und auch keinen gemeinsamen Schlüssel mit dem Server besitzt. Er kennt jedoch die Namen der Agenten $Alice$, $Bob$ und des Servers (d.h. er kann Nachrichten an diese schicken). Insgesamt sieht der Startzustand wie folgt aus:

$$\begin{eqnarray*} State_{Alice} & = & \{(Bob,agent), (Server,server), (start,Bo... ...\\ State_E & = & \{(Alice,agent),(Bob,agent),(Server,server)\} \end{eqnarray*}$$

Alle nicht aufgeführten Zustandskomponenten sind zu Anfang leer. Es soll nun überprüft werden, ob alle in den $Goal$-Komponenten enthaltenen Prädikate wahr sind, solange sie dort enthalten sind. Insbesondere also das von $B$ nach dem letzten Schritt eingefügte Prädikat ( $\forall_{P \in Agents \setminus \{Alice,Bob\}}: not\_knows(P,K_{Alice,Bob})$). Die Analyse ist eine Zustandsraumsuche auf den erreichbaren Zuständen, durchgeführt vom SH Verification Tool. Wird ein Zustand gefunden in dem ein aktuelles Ziel-Prädikat verletzt ist, kann mit demselben Tool der Weg der dahin führt ausgegeben werden. Eine Analyse auf dem soeben definierten Analyse-APA liefert einen Zustand, welcher das angegebene Prädikat verletzt. Nachfolgend nun der Weg zu diesem Zustand.

Zunächst gibt sich der Angreifer als $Bob$ aus und startet einen Protokoll-Lauf mit $Alice$. Dazu generiert er eine Zufallszahl $random_E$ und schickt die entsprechende Nachricht an den $Server$.

$$\begin{eqnarray*} E & \rightarrow & Server: \; (Bob,Alice,random_E) \end{eqnarray*}$$

Der Server generiert daraufhin einen neuen Sitzungsschlüssel $K$ und eine Nachricht, welche er an $Bob$ 'zurück'schickt.

$$\begin{eqnarray*} Server & \rightarrow & Bob: \; (encrypt((Bob,Server,sym),(ran... ... & & wobei: \;\; M_{Alice} = encrypt((Alice,Server,sym),(K,Bob)) \end{eqnarray*}$$

$Bob$ empfängt dann diese Nachricht, entschlüsselt sie und stellt fest, daß die zweite Komponente dem Namen $Alice$ entspricht. Außerdem kann $Bob$ auf einen von $Alice$ gestarteten Protokoll-Lauf reagieren. D.h. $Bob$ interpretiert diese Nachricht als dritte Nachricht eines von $Alice$ gestarteten Protokoll-Laufs obwohl sie als zweite Nachricht des Protokolls gedacht ist. Entsprechend des oben aufgeführten Zustandsübergangs betrachtet $Bob$ nun $random_E$ (die erste Komponente dieser Nachricht) als neuen Sitzungsschlüssel, generiert eine Zufallszahl $random_B$ und schickt diese verschlüsselt mit $random_E$ an $Alice$.

$$\begin{eqnarray*} Bob & \rightarrow & Alice: \; (encrypt(random_E,random_B)) \end{eqnarray*}$$

Der Angreifer fängt die Nachricht ab, kann sie entschlüsseln (da er $random_E$ kennt), und schickt die Antwort die $Bob$ erwartet.

$$\begin{eqnarray*} E & \rightarrow & Bob: \; (encrypt(random_E,sub(random_B,1))) \end{eqnarray*}$$

Schließlich erhält $Bob$ diese Nachricht, entschlüsselt sie und stellt fest, daß sie den Klartext $sub(random_B,1)$ enthält. Also betrachtet $Bob$ von nun an $random_E$ als gültigen Sitzungsschlüssel für die Kommunikation mit $Alice$. Dadurch wird das Prädikat, welches $Bob$ im letzten Schritt in seine $Goals$-Komponente einfügt falsch, da es einen Agenten gibt (nämlich $E$), welcher ebenfalls diesen Schlüssel kennt. Der Angreifer könnte sich jetzt gegenüber $Bob$ als $Alice$ ausgeben.

Dieser Angriff wird als arity-attack bezeichnet (arity heißt Stelligkeit). Er kann verhindert werden, indem $Bob$ beim Erhalt der dritten Nachricht des Protokolls prüft, wieviele Komponenten die Nachricht enthält. Der Angriff ist ebenfalls unmöglich, wenn die Agenten in der Lage sind zwischen Zufallszahlen und Schlüsseln zu unterscheiden. In diesem Fall würde es genügen, wenn bei $Bob$ im dritten Schritt die Voraussetzung $K_{AB} \in Keys$ hinzugefügt wird.