Beschränkungen des Suchraumes

Teilabfragen:

Anstatt zu fragen, wie der komplette Zustand erreicht werden kann, kann der Nutzer nur nach Teilen dieses Zustandes fragen. Kann ein Teil nicht erreicht werden, so kann auch der gesamte Zustand nicht erreicht werden. Kann man den Teilzustand jedoch von einem Anfangszustand erreichen, so muss noch einmal der komplette Zustand überprüft werden. Jedoch weiß man nun schon wie mögliche Pfade zum Startzustand aussehen.

Will man zum Beispiel fragen, wie der Angreifer die Worte d(X,W) und X erhalten kann, kann man zum Beispiel erst fragen, wie er d(X,W) erreicht, da was den Suchbaum erheblich verkleinern würde, da der Analyzer (siehe Definition oben) sowohl für beide Ziel seperat als auch zusammen versucht zu erfüllen und für eine Variable ohne weitere Bedingungen der Angreifer relativ viele mögliche Wörter finden kann.

Language Checker:

In dem Analyzer wurde ein Tool integriert, daß dazu genutzt wird um auf die oben beschrieben Weise (3.1) die Unereichbarkeit einer Sprache bewiesen. Diese Sprache kann dann in den Analyzer geladen werden, um die Zustände die ein Wort dieser Sprache als Wissen des Angreifers voraussetzen, als unerreichbar zu markieren. Der Analyzer hört dann an einem solchen Zustand mit der Suche in diesem Zweig auf. In [7] werden Methoden beschrieben, um nicht nur die Sprachen automatisch verifizieren zu lassen, sondern diese auch automatisch zu generieren. Dies wurde gegen 1996 implementiert und soll hier nicht weiter ausgeführt werden.

State Unifier:

Hier wird davon ausgegange, daß z.B. bestimmte Zustandsvariablen nur Werte in einer vorgegebenen Form annehmen, können. So z.B. eine Variable W, die einen Sessionkey aufnehmen soll, nur Werte der entsprechenden Form annimmt. Diese Daten werden dann verwendet um, wenn in einem Zustand eine Variable einen Wert annehmen soll, zu überprüfen, ob sich der zugewiesene mit der Beschreibung unifizieren lässt. Geht dies, so wird der Zustand verwendet, andernfalls als unerreichbar markiert. Solche Regel können sowohl automatisch als auch manuell hinzugefügt werden.