Begrenzung des Suchraumes durch formale Sprache

Die Endlosschleifen in denen das Programm landet, durchlaufen fast nie immer wieder die selbe Menge an Zuständen, statt dessen passiert meist folgendes. Sucht man nach einem Wort t und der Analyzer gibt aus, daß dies nur gefunden werden kann, wenn der Angreifer zuvor e(X,t) kennt. Fragt man nun nach diesem Wort und der Analyzer findet, daß das nur mit dem zuvorigen Wissen von e(X2,e(X,t)) geht. Dies geht dann so weiter. Es ist ersichtlich, daß er die Wörter nicht finden kann und statt dessen in eine Endlosschleife gerät. Für das Beispiel kann man nun die formale Sprache E mit folgenden Erzeugenden entwickeln.

1. E $\rightarrow t$,
2. E $\rightarrow e$(X,E)

wobei X die Sprache aller nicht reduzierbaren Wörter über $T(\Phi,F)$ ist. Zu zeigen ist nun, daß jedes nicht reduzierbare Wort aus E nur dem Angreifer bekannt sein kann, wenn er vorher schon ein anderes Wort der Sprache E kennt. Damit ist kein Wort der Sprache E erreichbar, und somit auch kein Zustand in dem der Angreifer solch ein Wort kennen müsste. Der Analyzer wird nun auf jeden Erzeugenden der Sprache E angewandt, um zu zeigen, daß nicht reduzierbare Wörter der Sprache erzeugt werden. Im Beispiel ist dies trivial und schon gezeigt. Nun kann man bei der Analyse alle solche Zustände ignorieren, die ein solches Wort enthalten oder zu denen man nur gelangt, wenn man in einem vorrigen Zustand solch ein Wort wissen müsste. Sind alle Zustände die zu einem sicheren Zustand führen, unereichbar, so ist das Protokoll für diesen Angriff sicher.