Beschreibung des Modells

Aus der Tatsache, daß der Analyzer in Prolog implementiert ist, ergibt sich daß Variablen mit einem großen Buchstaben und Konstanten und Funktionssymbole mit einem Kleinen beginnen, sowie daß alle Variablen universell quantifiziert sind (z.B. für do(X) bedeutet: für alle X do(X)). Die selben Konventionen gelten daher auch für die Protokollspezifizierung und für Beispiele in den folgenden Abschnitten.

Desweiteren wird die Verschlüsselung einer Nachricht Y mit einem Schlüssel X, wird mit e(X,Y) angegeben und die Entschlüsselung einer Nachricht Y mit einem Schlüssel X als d(X,Y).

In dem Modell werden Protokollregeln in der Form

$$\mbox{ If } I\subseteq {\bf W} \mbox{ and } A \mbox{ and Cond}(I,A) \mbox{ then } {\bf W} := {\bf W} \cup O \mbox{ and } A'$$

ausgedrückt, wobei

• W die Menge der Wörter ist, die der Angreifer kennt.
• $I$ (in) die Wörter einer Nachricht angibt, die zu einem Teilnehmer geschickt wurden.
• $O$ (out) die Wörter einer Nachricht angibt, die von einem Teilnehmer geschickt wurden.
• $A$ und $A'$ sind Anweisungen, die aus Gleichungen der Form $T=D$ bestehen, wo T der Name einer Zustandsvariablen ist.
• Cond$(I,A)$ ist eine Menge weiterer Bedingungen an $I$ und $A$ der Form: $C \neq E$, wobei $C$ ein Subterm aus $I$ oder $A$ ist und $E$ ein Term.

Solche Regeln können verschiedene Ereignisse beschreiben, wie

• einen Teilnehmer, der auf eine Nachricht des Angreifers antwortet;
• die Veränderung einer internen Zustandsvariable eines Teilnehmers;
• ein Teilnehmer, der versucht den Prokollablauf zu initiieren.
• den Angreifer, welcher mit dem ihn zur Verfügung stehenden Mitteln Nachrichten generiert.

Beispiel 1
Eine Regel für einen Angreifer, der in der Lage ist, Daten zu verschlüsseln, kann so dargestellt werden:

$\mbox{ If } \{X,Y\}\subseteq {\bf W} \mbox{ then } {\bf W} := {\bf W} \cup \{e(X,Y)\}$

Wie wir in Abschnitt 4 sehen werden, ist eine solche Angabe in der echten Spezifikation nicht nötig, da diese sich etwas von den theoretischen Grundlagen unterscheidet und solche Regeln von Analyzer selbstständig generiert werden.

Beispiel 2
Nehmen wir an ein Teilnehmer sendet alle Nachrichten die er bekommt mit dem Sessionkey verschlüsselt weiter, so kann man das mit folgender Regel ausdrücken.

$\mbox{ If } \{Y\}\subseteq {\bf W} \mbox{ and KEYSTATE(}a)=X \mbox{ then } {\bf W} := {\bf W} \cup \{e(X,Y)\}$

Neben den Regeln besteht ein Protokoll in diesem Modell aus einer Menge von Reduktionsregeln, welche die Umformung komplexerer Wörter in Einfachere beschreiben. Beispiele dafür sind

1. $d(X,e(X,Y)) \rightarrow Y$, da sich Ver- und Entschlüsselung mit dem selben Key aufheben
2. $p(s(X)) \rightarrow X$, wobei s und p die Nachfolger- und Vorgängeroperationen (successor und predecessor) sind.

Definition 1: Spezifikation S eines Protokolls ist ein Tupel
$[T(\Phi,F),{\cal E}, {\bf S, R}, W_0, A_0]$ wobei

• $\Phi$ eine abzählbare Menge von Variablen ist;
• $F$ eine endliche Menge an Funktionssymbolen ist;
• $T(\Phi,F)$ die Menge von Termen ist, die durch $\Phi$ und $F$ gebildet werden kann;
• $\cal E$ ist eine Menge an Umschreiberegeln (rewrite rules)
• S eine Menge von Zustandsvariablen ist;
• $W_0$ die Menge der Wörter aus $[T(\Phi,F)$ ist, die der Angreifer zu Beginn kennt;
• $A_0$ eine Menge von anfänglichen Zuweisungen von Werten auf Zustandsvariablen;

und R eine Menge von Protokollregel der Form

$\mbox{ If } I\subseteq {\bf W} \mbox{ and } A \mbox{ and Cond}(I,A) \mbox{ then } {\bf W} := {\bf W} \cup O \mbox{ and } A'$

wie oben, jedoch mit den Einschränkungen, daß

• $I$ und $O$ nur aus Termen von $T(\Phi,F)$ besteht;
• $A$ und $A'$ Anweisungen aus Gleichungen der Form $T=D$ bestehen, wo $T$ der Name einer Zustandsvariablen ist und $D \in T(\Phi,F)$.

Definition 2: Term, Konstanten
Sei $\Phi$ eine abzählbare Menge an Variablen und $F$ eine endliche Menge an Funktionssymbolen disjunkt von $\Phi$ mit zugehöriger arity (Anzahl der Funktionsparameter). Dann ist ein Term entweder eine Variable aus $\Phi$ oder ein Funktionsymbol gefolgt von $n$ Termen, wobei n die arity des Funktionssymbols angibt. Ein Funktionssymbol mit einer arity von null ist eine Konstante.

Definition 3: Substitution, Unifikator
Sei $T(\Phi,F)$ die Menge von Termen ist, die durch $\Phi$ und $F$ gebildet werden kann. Dann ist eine Substitution eine Funktion von $\Phi$ in $T(\Phi,F)$. Der Term den man durch Anwendung einer Substitution $\sigma$ auf die Variablen eines Terms $T$ erhält, wird durch $\sigma T$ angegeben.

Ein Unifikator von zwei Termen $T$ und $U$ ist eine Substitution $\sigma$, so daß $\sigma T = \sigma U$. Es werden also 2 Terme durch entsprechende Substitution in den gleichen Term umgewandelt. Der allgemeingültigste Unifikator von $T$ und $U$ ist ein Unifikator $\sigma$, so daß, wenn es einen weiteren Unifikator $\tau$ gibt, es noch ein weiter Unifikator $\mu$ existiert, so daß gilt $\tau = \mu \sigma$.

Definition 4: term-rewriting system, Normalform
Ein term-rewriting system über $T(\Phi,F)$ ist eine Menge gerichteter Gleichungen $\cal E$, so daß für $T_1 \rightarrow T_2$ in $\cal E$, $V(T_2) \subseteq V(T_2)$ gilt, wobei V(T) die Menge der Variablen in T angibt.

Wenn ein Term A in einen eindeutigen nicht reduzierbaren Term durch die Anwendung von Reduktionsregeln gebracht werden kann, so nennt man den erzeugten Term Normalform von A (nf(A)).

Für den Analyzer sind term-rewriting systems interessant, die Noetherian und locally confluent sind. Diese haben die Eigenschaft, daß jeder Term A zu einer eindeutigen nicht mehr weiter reduzierbaren Normalform nf(A) reduzierbar ist.

Definition 5: Noetherian, locally confluent
Sei $\cal E$ ein term-rewriting sytem über $T(\Phi,F)$. $\cal E$ ist Noetherian, wenn ein Term A, der von einem Term B mittels der Anwendung von Reduktionsregeln erreichbar ist, innerhalb einer endlichen Anzahl von Schritten erreicht wird.

$\cal E$ ist locally confluent, falls wennimmer ein Term A zu den Termen B und C mittels zwei verschiedener Reduktionsregeln reduzierbar ist, dann sind B und C beide zu einem gemeinsamen Term D reduzierbar.

Beispiel 3
Solch ein term-rewriting system kann zum Beispiel wie folgt aussehen. Es handelt sich wieder um die triviale Aufhebung von Ver- und Entschlüsselung mit dem selben Key.


$d(A,e(A,B) \rightarrow B$
$e(A,d(A,B) \rightarrow B$

Es folgen Grundlagen für das Zustandsmodell, es wird beschrieben, was ein Systemzustand und was eine Zustandsbeschreibung ist und wie man eine Zustandsbeschreibung von einer Anderen erreicht.

Definition 6: Systemzustand und Zustandbeschreibung
Ein Systemzustand ist ein Paar ( $\Lambda, \Delta$), wobei $\Lambda$ die Menge der Wörter ist, die der Angreifer kennt und $\Delta = { \gamma_1 = \beta_1, \ldots, \gamma_k = \beta_k}$ den Zustandsvariablen ($\gamma_l$) die Werte ($\beta_l$) zuordnet.

Eine Zustandsbeschreibung ($L,D$) ist ein Paar, so daß $L$ eine Menge an Termen aus $T(\Phi,F)$ ist und $D = { G_1 = D_1, \ldots, G_t = D_t }$ ist die Zuordnung einer Menge von Termen aus $T(\Phi,F)$ ($D_i$) zu den Zustandsvariablen ($G_i$).

Ein Systemzustand ( $\Lambda, \Delta$) genügt einer Zustandsbeschreibung ($L,D$), wenn alle Terme in ( $\Lambda, \Delta$) nicht reduzierbar sind und es eine Substitution $\sigma$ gibt, so daß $\sigma L \subseteq \Lambda$ und $\sigma D \subseteq \Delta$.

Beispiel 4
Nehmen wir die Zustandsbeschreibung (e(k,X),). Dann können wir annehmen, daß der Angreifer ein word e(k,$\sigma$X) kennt, wobei die Substitution X einen Term zuweist, so daß e(k,$\sigma$X) nicht weiter reduziert werden kann. Daher könnte er e(k,m) oder e(k,e(l,m)) kennen, nicht aber e(k,d(k,m)).

Die Annahme, daß Term (im Beispiel e(k,$\sigma$X)) nicht weiter reduzierbar ist, ist daher wichtig, weil wenn der Angreifer e(k,$\sigma$X) kennt und X=d(k,Y) sein könnte, sich das ganze zu Y reduzieren würde und man daraus erfahren würde, daß der Angreifer irgendein Y kennt. Und zu der Zustandsbeschreibungdiese nutzlose Information hinzukommen würde.

Eine Protokollregel kann nun interpretiert werden, um von einer Zustandsbeschreibung zu einer Weiteren zu gelangen. Die Bedingungen der Regel müssen von einer Zustandsbeschreibung erfüllt sein, damit die Regel angewandt wird. Mit der Folgerung aus der Regel wird die neue Beschreibung konstruiert.

Definition 7: Übergange zwischen Zustandsbeschreibungen
Seien ($L,D$) und ($L',D'$) Zustandsbeschreibungen. Dann sei R eine Regel der bekannten Form

$\mbox{ If } I\subseteq {\bf W} \mbox{ and } A \mbox{ and Cond}(I,A) \mbox{ then } {\bf W} := {\bf W} \cup O \mbox{ and } A'$

,so daß eine Substitution $\sigma$ existiert, die den Variablen von R einen Term zuordnet und die Terme in ($L,D$), ($L',D'$), $I$, $A$ so umformt, daß diese nicht weiter reduzierbar sind und gilt

1. $\sigma I \subseteq \sigma L$
2. $\sigma A \subseteq \sigma D$
3. Cond( $\sigma A, \sigma I$) enthält keine Ungleichungen der Form $X\neq X$ (not contradicted)
4. $\sigma L' \subseteq \sigma L \cup nf(\sigma O)$ (,,die übertragenen Wörter werden den, dem Angreifer bekannten Wörtern, hinzugefügt``)
5. $\sigma D' \subseteq (\sigma D - \sigma D'') \cup nf(\sigma A')$, wobei $\sigma D''$ die Menge der Zuweisung aus $\sigma D$, die durch neue Zuweisung in $nf(\sigma A')$ ersetzt wird. (,,die neuen Werte für lokalen Zustandsvariablen werden, die aus der Regel folge, werden in der Zustandsvariablenliste des Zielzustandes gesetzt``)
6. Entweder $\sigma L' \cap nf(\sigma O)$ oder $\sigma D' \cap nf(\sigma A')$ ist nicht leer. (Um triviale Übergänge zu verhindern; Es würden keine Terme oder Zustandsvariablen durch eine solche Regel hinzugefügt/geändert.)

Die Zustandsbeschreibung ($L',D'$) ist nun von der Zustandsbeschreibung ($L,D$) mittels der Regel R zu erreichen. $P'$ ist von $P$ mittels der Regeln $R_1, \ldots, R_k$ erreichbar, wenn es eine Reihe von Zustandsbeschreibungen $P_0, \ldots, P_k$ gibt, so daß $P'$ von $P_k$ mittels $R_k$ erreichbar ist und so weiter.

Beispiel 5
Gehen wir davon aus, daß der Angreifer das Wort ``message`` kennt und KEYSTATE(a):=key1, dann kann die Regel

$\mbox{ If } Y \subseteq {\bf W} \mbox{ and } \mbox{KEYSTATE(}Z)=X \mbox{ then } {\bf W} := {\bf W} \cup e(X,Y)$

mit der Substitution Y=message, Z=a und X=key1 angewendet werden. Man gelangt dann von der Zustandsbeschreibung ({message}, {KEYSTATE(a)=key1}) zu ({message, e(key1,message)}, {KEYSTATE(a)=key1}).

Man kann nun verfolgen wie durch Anwendung der Prokollregeln man von einem Zustand zum nächsten gelangt. Um zu Bestimmen, ob ein Protokoll sicher ist soll gezeigt werden, daß man von bestimmten Zuständen nicht den Initialzustand erreichen kann. Was nun folgt ist genau der umgekehrte Schritt. Es muss anhand der Zustandsbeschreibung bestimmt werden, welche andere Zustandsbeschreibungen die Zustände beschreibt, die direkt davor gewesen sein könnten. Dazu wird im Prinzip die Folgerung jeder Regel mit der Zustandsbeschreibung unifiziert.

Sei die Zustandsbeschreibung ($L,D$) gegeben. Man sucht nun eine Substitution $\sigma$, die $I$, $A$ und ($L,D$) so umformt, daß diese nicht weiter reduzierbar sind und im weiteren gilt

1. sich entweder irgendeine Teilmenge von $\sigma O$ zu einer Teilmenge von $\sigma L$ oder irgendeine Teilmenge von $\sigma A'$ sich zu einer Teilmenge von $\sigma D$ reduziert.
2. Cond( $\sigma A, \sigma I$) enthält keine Ungleichungen der Form $X\neq X$ (not contradicted)
3. $\sigma A'$ reduziert sich zu einem Ausdruck, der $D$ nicht wiederspricht.
4. Wenn $\sigma D$ eine Anweisung $\sigma (G_i=D_i)$ enthält und $\sigma A$ dieser Anweisung wiederspricht, dann muss $nf(\sigma A')$ diese Anweisung enthalten.

Daraus ergibt sich ein vorheriger Zustand ($L',D'$), in dem der Angreifer $\sigma I \cup (\sigma L - nf(\sigma O))$ kennt und die Menge der Zustandsvariablen $\sigma A \cup (\sigma D - \sigma D'')$ entspricht, wobei $\sigma D''$ alle Zuweisung aus $nf(\sigma A')$ enthält.

Der Analyzer muss nun alle möglichen Substitutionen $\sigma$ finden, die die Zustandsbeschreibung mit der Folgerung einer Regel unifiziert. Davon gibt es oft eine unendliche Menge, jedoch eine endlich, ausreichende Menge (complete set), mit deren Hilfe man alle anderen Unifikatoren bilden kann. Zu der Bestimmung solcher Mengen gibt es einige Algorithmen. Da von dem term-rewriting Sytem verlangt wird, daß es Noetherian und locally confluent ist, kann man mit Hilfe eines Algorithmus aus der Klasse der ,,narrowing algorithms`` diese Menge bestimmen. Im Fall des Analyzers wurde eine modifizierte Version des NARROWER Algorithmus [5] eingesetzt, um anhand einer Protokollbeschreibung und der Beschreibung eines Systemzustandes, die Menge der Beschreibungen zu finden, die diesem direkt vorangehen können.

Beispiel 6
Nehmen wir als Beispiel eine Spezifikation mit der einen Regel

$\mbox{ If } Y \subseteq {\bf W} \mbox{ and } \mbox{KEYSTATE(}Z)=X \mbox{ then } {\bf W} := {\bf W} \cup e(X,Y)$

und fragen den Analyzer danach, wie der Angreifer ein Wort Q finden kann. Dann sucht das Programm nach einer ausreichenden Menge der Unifikatoren mit e(X,Y) und dem term-rewriting system


$d(A,e(A,B) \rightarrow B$
$e(A,d(A,B) \rightarrow B$.

Es werden dann 2 Elemente der Menge gefunden und zwar Q:=e(X,Y) und Y:=d(X,Q). Wendet man die 1. Unifikation an erhält man die Bedingungen $Y \subseteq {\bf W}$ and KEYSTATE($Z)=X$ und der Angreifer lernt das Wort Q:=e(X,Y), der Vorgängerzustand war demnach (Y, KEYSTATE($Z)=X$). Bei der 2. erhält man $d(X,Q) \subseteq {\bf W}$ and KEYSTATE(Z)=X und der Angreifer lernt das Wort Q (e(X,Y)=e(X,d(X,Y))), der Vorgängerzustand ist demnach (d(X,Q), KEYSTATE($Z)=X$)

Beispiel 7
Als zweites Beispiel dieselbe Spezifikation mit der einen Regel

$\mbox{ If } Y \subseteq {\bf W} \mbox{ and } \mbox{KEYSTATE(}Z)=X \mbox{ then } {\bf W} := {\bf W} \cup e(X,Y)$

und fragen den Analyzer danach, wie der Angreifer das Wort e(A,B) lernen kann, also den Zustand (e(A,B),) erreicht. Dann werden die Substitutionen 1. X=A,Y=B und 2. Y=d(X,e(A,B) gefunden. Für den ersten ergibt sich der Zustand (B,KEYSTATE(Z)=A) und für den zweiten (d(X,e(A,B)),KEYSTATE(Z)=A).

Ziel des Programmes ist es nun zu zeigen, daß ein Startzustand nicht von einem definierten unsicheren Zustand zu erreichen ist. Würde man das ganze ohne Einschränken durchführen, würde schnell ein unüberschaubare Menge an Zuständen entstehen, meist in Endlosschleifen endend. Man braucht also zum einen Techniken um die Suche einzuschränken und zum anderen zu Zeigen, daß ein Zustand der irgendwo in einer Endlosschleife entsteht kein Startzustand sein kann. Um ein Protkoll zu analysieren, wird nun eine Protokollspezifikation erstell, die unsicherne Zustände bestimmt und gezeigt, daß ein Menge von Zuständen unerreichbar ist. Dann wird über die restlichen Zustände ein komplette Suche laufen gelassen. Hier wird nun noch beschrieben, wie Zustände mit Hilfe formaler Sprachen als unerreichbar bestimmt werden.