Dieser Abschitt beschreibt kurz den Analyzer, wie er 1994 implementiert war. Das ursprüngliche Modell, wie oben beschrieben, wurde erweitert. Außerdem wird beschrieben, wie die Spezifikation für das Programm aussieht.
Im Gegensatz zu anderen Tool ist der Analyzer weniger automatisiert, wie schon weiter oben gesehen muss der Nutzer die Bearbeitung beeinflussen, dennoch gibt es einen automatischen Modus und immer mehr Teile der Analyse wurden automatisiert.
Die wichtigste Erweiterung in der Protokollspezifikation ist es, daß bei den Übergangsregeln die Ereignisse, die Regel ausführt, mitprotokolliert werden, welche die Übergänge repräsentieren. Diese Events sind dann auch Teil der Zustandsbeschreibung und, damit eine Regel benutzt werden kann um einen Vorgängerzustand zu finden, werden auch die Events der Beschreibung mit dem Event der Regel unifiziert. So kann man nicht nur nachfragen, wie der Angreifer ein Wort findet, sondern wie ein bestimmtes Event stattfinden konnte, etc..