Übergangsregeln

Die Regeln sind ähnlich, wie oben beschrieben aufgebaut, jedoch durch die events erweitert worden.

Vorbedingungen (if)

Gibt an welche Worte der Angreifer wissen muss, die Werte der Zustandsvariablen (lfacts) die gesetzt sein müssen und weitere Bedingungen die erfüllt sein müssen, damit die Regel wirksam wird.

Folgerung (then)

Die Bedingungen die erfüllt sind, nachdem die Regel wirksam geworden ist. Gibt die Wörter an die der Angreifer gelernt hat, und gibt Zustandsvariablen neue Werte. Außerdem wird, wenn die Regel ausgeführt wird, ein Zähler des Teilnehmers erhöht, um die Protokollschritte mitverfolgen zu können.

Event-Anweisung

Dies ist hier der wesentlichste Unterschied zu der obigen Beschreibung. Die Events werden benutzt um das Auslösen der Regel zu speichern. Sie beschreiben, was die Regel macht. Diese Event-Beschreibung muss natürlich mit den Rest der Regel übereinstimmen. Die Eventanweisung ist ein Funktion mit vier Parameter, der eine Liste relevanter Wörter übergeben wird. Der erste Paramter gibt den Teilnehmer an, der das Event ausführt. Der Zweite, gibt den Zähler des Teilnehmers vor dem Auslösen der Regel und der Vierte den Zähler danach. Der Dritte Parameter dient dazu das Event zu identifizieren (z.B. als Sende eines Schlüssels).

Ähnlich wie die events sind die lfacts aufgebaut. Sprich mit einem Bezeichner zur Identifizierung, dem zugehörigen Nutzer, und den beiden Zählerständen. Die Regeln und ihre Substitution werden dadurch erheblich unübersichtlicher, weswegen ich auf weiterführende Beispiele (ganzer Protokollspezifikationen und dem Finden eines Fehlers) verzichten werde. Zur Veranschaulichung nur kurz ein Beispiel für solch eine Regel. Nutzer können entweder honest oder dishonest sein. Ist der dishonest wird davon ausgegangen, daß er mit dem Angreifer kooperiert und dem Angreifer somit seine Möglichkeiten zur Verfügung stehen.


rule(1)
If:
count(user(A,honest)) = [N],
then:
count(user(A,honest)) = [s(N)],
intruderlearns([pke(pubkey(server),rand(user(A,honest),N)),
user(A,honest), user(B,W)])
lfact(user(A,honest),N,step1,s(N))=[user(B,W),rand(user(A,honest),N)]
EVENT:
event(user(A,honest),N,initrequest,s(N))=[user(B,W),rand(user(A,honest),N)]

user(A,honest) versucht Verbindung mit einem anderen Nutzer aufzunehmen, dazu verschickt er an einen Keyserver mit dessen öffentlichen Schlüssel verschlüsselt eine Zufallszahl und ausßerdem noch die Namen beider Nutzer. Er merkt sich in seinen Zustandvariablen, daß er user(B,W) Verbindung aufnehmen wollte und die entsprechende Zufallszahl, welche später als Key verwendet werden soll.