Spezifikation eines APA für das Needham-Schroeder Protokoll

Zunächst einige grundlegende Mengen:

$$\begin{eqnarray*} Agents & & \textrm{Menge der Namen von Agenten} \\ Keywords... ...lobalen Zuständen} \\ I\!N & & \textrm{die natürlichen Zahlen} \end{eqnarray*}$$

Es wird davon ausgegangen, daß die Agenten keine Typprüfungen auf den Nachrichten vornehmen können und so die im Protokoll verwendeten Zufallszahlen einfach natürliche Zahlen sind. Soll die Möglichkeit einer Unterscheidung gegeben sein, so müssen einfach nur weitere Mengen definiert werden (z.B. $Random$, $Nonce$, etc.).

Die Grafik zeigt die Struktur des APA für das Needham-Schroeder Protokoll. Die Kreise entsprechen dabei den Zustandskomponenten, die Rechtecke repräsentieren elementare Automaten. Durch die Kanten ist angegeben, auf welche Zustandskomponenten der jeweilige elementare Automat Zugriff hat.

Der APA des Needham-Schroeder Protokolls enthält drei elementare Automaten $A$, $B$ und $S$. Diese Automaten sind über die Zustandskomponente $Network$ miteinander verbunden. Zusätzlich besitzen $A$, $B$ und $S$ noch jeweils vier weitere private Zustandskomponenten (d.h. auf die jeweils nur ein einziger Automat Zugriff hat) $State_e$, $Symkeys_e$, $Asymkeys_e$ und $Goals_e$, wobei $e \in \{A,B,S\}$ ist.

Weiter muss die Menge der zugelassenen Nachrichten definiert werden. Die Vereinigung der Mengen $Agents$, $Keywords$, $Keys$ und $I\!N$ bildet die Menge der atomaren Nachrichten. Darauf aufbauend kann die Menge aller Nachrichten $M$ rekursiv definiert werden:

1. Jede atomare Nachricht ist Element von $M$.
2. Wenn $m_1, ..., m_n \in M$, dann ist auch $(m_1, ..., m_n) \in M$.
3. Wenn $k,m \in M$ dann sind auch $encrypt(k,m), decrypt(k,m) \in M$.
4. Wenn $m \in M$ dann ist auch $sub(m,1) \in M$.

Zusätzlich werden noch die Standard-Funktionen $element(k,(m_1, ...,m_n))$ und $length(m_1, ..., m_n)$ eingeführt, welche das k-te Element eines Tupels bzw. die Anzahl der Elemente des Tupels liefern. Für die Funktionen $encrypt$ und $decrypt$ werden die folgenden symbolischen Eigenschaften definiert:

$$\begin{eqnarray*} decrypt(k,encrypt(k,m)) & = & m \\ encrypt(k,decrypt(k,m)) & = & m \end{eqnarray*}$$

Diese beiden Eigenschaften modellieren symmetrische Verschlüsselung. Für die Analyse wird in diesem Fall perfekte Verschlüsselung angenommen, d.h. Schlüssel können nicht erraten werden, für die Erzeugung von $encrypt(k,m)$ und $decrypt(k,m)$ müssen $m$ und $k$ bekannt sein und aus $encrypt(k,m) = encrypt(k',m')$ folgt, daß $m = m'$ und $k = k'$ sind. Für andere Analysen können diese Annahmen jedoch durchaus gelockert werden. So lässt sich beispielsweise durch die Annahme $blockcrypt(k,(m_1,m_2)) = (blockcrypt(k,m_1),blockcrypt(k,m2))$ ein Blockchiffre modellieren.

Für die Schlüssel wird festgelegt, daß $(P,Q,sym) = (Q,P,sym)$ ist. Durch die obigen Eigenschaften wird auf natürliche Weise eine kürzeste Normalform für Nachrichten festgelegt, in denen keine sich gegenseitig aufhebenden $encrypt$- und $decrypt$-Funktionen mehr enthalten sind. Die Menge dieser kürzesten Normalformen wird mit $Messages$ bezeichnet. Die Elemente von $Messages$ bilden nun den Inhalt der Zustandskomponenten des APA. Eine Ausnahme bildet die Komponente $Network$, welche Elemente von $Agents \times Messages$ enthält. Die symmetrischen Schlüssel eines Agenten $P$ werden als Tupel $(Q,sym,key)$ in die $Symkeys_P$-Komponente eingetragen (wobei $key$ den symmetrischen Schlüssel und nicht das Element aus $Keywords$ meint).

Der Nachrichtenaustausch zwischen den Agenten läuft über die Komponente $Network$. Um eine Nachricht $M$ an einen Agenten $P$ zu schicken, wird das Tupel $(P,M)$ der $Network$-Komponente hinzugefügt. Beim Empfangen der Nachricht wird das Tupel dann im dadurch ausgelösten Zustandsübergang des empfangenden Agenten aus $Network$ gelöscht. Mit Ausnahme des Angreifers können Agenten nur an sich selbst gerichtete Nachrichten empfangen.

Jetzt muss noch für jede der Zustandskomponenten $S \in \mathcal{S}$ die zugehörige Zustandsmenge $Z_S$ definiert werden. Jede dieser Zustandsmengen ist ein Multiset. Ein Multiset über einer Menge $A$ kann durch eine Funktion $f: A \rightarrow I\!N$ repräsentiert werden, wobei $f(a)$ angibt wie oft das Element $a \in A$ im Multiset f enthalten ist. Die Menge aller Multisets über einer Menge $A$ wird im folgenden als $\overline{\mathcal{P}}(A)$ bezeichnet. Damit lassen sich die Zustandsmengen $Z_S$ des APA definieren:

$$\begin{eqnarray*} Z_{Network} & = & \overline{\mathcal{P}}(Agents \times Messag... ... Keys) \\ Z_{Goals_P} & = & \overline{\mathcal{P}}(Predicates) \end{eqnarray*}$$

Für $Symflags$ und $Asymflags$ werden dabei geeignete Mengen eingesetzt, für Needham-Schroeder ist $Symflags = \{sym\}$ und $Asymflags$ leer.

Als nächstes soll der Anfangszustand des APA spezifiziert werden. Er kann durch den Inhalt der Zustandskomponenten angegeben werden:

$$\begin{eqnarray*} State_A & = & \{(B,agent), (S,server), (start,B)\} \\ Symke... ...\} \\ Symkeys_S & = & \{(A,sym,(A,S,sym)), (B,sym,(B,S,sym))\} \end{eqnarray*}$$

Die Agenten $A$ und $B$ kennen sich also gegenseitig, kennen den Server $S$ und haben beide jeweils einen Schlüssel für die Kommunikation mit $S$. $S$ kennt $A$ und $B$ und besitzt ebenfalls die symmetrischen Schlüssel zur Kommunikation mit diesen. Das Token $(start,B)$ in $State_A$ ermöglicht Agent $A$ das Protokoll mit $B$ als gewünschtem Kommunikationspartner zu initiieren und $(respond,A)$ in $State_B$ gibt $B$ die Möglichkeit darauf zu reagieren. Alle nicht aufgeführten Zustandskomponenten sind leer.

Im letzten Schritt der Spezifikation ist die Zustandsüberführungsfunktion für die einzelnen Agenten zu modellieren. Sie kann z.B. notiert werden, indem die Voraussetzungen für den Zustandsübergang eines Agenten und die damit verbundenen Aktionen aufgeschrieben werden. Als Beispiel nun nachfolgend der zu Schritt vier des Needham-Schroeder Protokolls gehörende Zustandsübergang. $B$ erhält hierbei die Nachricht $\{K_{AB},A\}_{K_{BS}}$ und schickt daraufhin $\{R_B\}_{K_{AB}}$ an $A$.

Voraussetzung
$(B,M) \in Network$	Nachricht $M$ an $B$ liegt in $Network$
$(respond,A) \in State_B$	$B$ kann auf das von $A$ gestartete
	Protokoll reagieren
$(A,agent) \in State_B$	$B$ kennt Agent $A$
$(S,server) \in State_B$	$B$ kennt den Server $S$
$(S,sym,K_{BS}) \in Symkeys_B$	$B$ teilt einen symmetrischen Schlüssel
	mit $S$
$element(2,decrypt(K_{BS},M)) = A$	nach Entschlüsselung von $M$ mit dem
	Schlüssel $K_{BS}$ ist die zweite
	Komponente der Nachricht der Name
	von $A$
Aktionen von $B$
$K_{AB}:=element(1,decrypt(K_{BS},M))$	die erste Komponente des Klartextes
	von $M$ wird als $K_{AB}$ gesichert
$R_B \in newRandom$	$B$ generiert eine neue Zufallszahl $R_B$
$(B,M) \hookleftarrow Network$	$B$ entfernt die Nachricht aus $Network$
$(new \; session \; key,A,K_{AB},R_B) \hookrightarrow State_B$	$B$ speichert $K_{AB}$ als neuen
	Sitzungsschlüssel
$(A,encrypt(K_{AB},R_B)) \hookrightarrow Network$	$B$ schickt die nächste Nachricht an $A$

Die Spezifikation der anderen Schritte kann in [1] nachgelesen werden. Damit ist die Funktionalität des Protokolls vollständig modelliert. Durch diese Zustandsübergänge wird jedoch eigentlich beschrieben, was ein Agent in Rolle $A$ oder $B$ tun muss. Zu der formalen Beschreibung des Protokolls gehört also noch eine Festlegung, welche Kombination von Rollen verboten ist, und welche Rollen vom Angreifer übernommen werden können. Eine mögliche Festlegung für Needham-Schroeder wäre zu verbieten, daß ein Agent gleichzeitig zwei Rollen übernimmt ($A$ und $S$, $B$ und $S$ oder $A$ und $B$), und daß der Angreifer die Rolle von $S$ einnehmen kann. Für die obige Spezifikation des Anfangszustands bedeutet daher das Tupel $(B,agent)$ in $State_A$, daß $A$ alle Agenten kennt, die die Rolle $B$ übernehmen können. Im Unterschied dazu müssen bei Tupeln der Form $(S,sym,(A,S,sym))$ in den $Symkeys$-Komponenten nun die Platzhalter $A$ und $S$ durch einzelne Agenten ersetzt werden, da ein Agent nur seinen symmetrischen Schlüssel für die Kommunikation mit dem Server kennt (und nicht die aller Agenten, die die Rolle $A$ übernehmen können).

Die Sicherheit eines Protokolls kann nur relativ zu irgendwelchen Sicherheitsanforderungen bzw. Sicherheitszielen überprüft werden. Daher müssen die Sicherheitsziele mit spezifiziert werden. Sie werden in den $Goal$-Komponenten der einzelnen Agenten vermerkt. So kann ein Agent nach jeder Aktion nach der aus seiner Sicht ein bestimmtes Sicherheitsziel erfüllt sein soll, ein entsprechendes Prädikat in seiner $Goal$-Komponente vermerken. Damit ergibt sich dann eine Definition für die Sicherheit eines Protokolls.

Definition: Ein Protokoll heißt sicher, wenn jedes Prädikat welches in einer der $Goal$-Komponenten steht wahr ist, solange es dort steht.

Ein Sicherheitsziel nach dem Empfang der letzten Nachricht des Needham-Schroeder Protokolls wäre, daß der Sitzungsschlüssel $K_{AB}$ nun keinem Agenten außer $A$ und $B$ bekannt ist. In der Zustandsüberführungsfunktion drückt sich das wie folgt aus:

Aktionen von $B$
$(session \; key,A,K_{AB}) \hookrightarrow State_B$	$B$ akzeptiert $K_{AB}$ als
	Sitzungsschlüssel
$\forall_{P \in Agents \setminus \{A,B\}}: not\_knows(P,K_{AB}) \hookrightarrow Goals_B$