Wie im Modell von Dolev und Yao wird davon ausgegangen, daß der Angreifer den gesamten Netzwerkverkehr mitlesen, Nachrichten zurückverfolgen, verändern und löschen und auch selbst eigene Nachrichten erzeugen kann. Weiterhin kann er Funktionen die normalen Nutzern zur Verfügung stehen, wie Ver- und Entschlüsselung, ausführen und evtl. mit einigen Nutzern kooperieren. Es wird jedoch angenommen, daß er einige Mengen von Wörtern nicht kennt und es sein Ziel ist, diese herauszufinden. Dies sind z.B. keys von ehrlichen (honest) Nutzern oder verschlüsselte Nachrichten.
Aus der Tatsache, daß er volle Kontrolle über den Netzverkehr hat, folgt daß jede Nachricht, die ein Teilnehmer erhält, vom Angreifer stammen kann. Daher kann man sich das Protokoll als ein algebraisches System vorstellen, daß der Angreifer manipuliert. Also als eine Menge von Regel zum Erzeugen von Wörtern in einer formalen Sprache. Die Wörter und damit die Regeln, die die Wörter erzeugen, unterliegen einigen Reduktionsregeln, z.B. daß sich Ver- und Entschlüsselung gegenseitig aufheben. Der Angreifer versucht nun herauszufinden, ob ein Wort zu der Sprache gehört oder nicht. Wenn der Angreifer nun kein geheimes Wort aus einer vorbestimmten Menge (z.B. den key eines Nutzers) erhalten kann, ist das Protokoll sicher (analog zum Modell von Dolev und Yao).
Als Erweiterung zum Modell von Dolev und Yao ist es nicht nur Ziel des Angreifers ein solches geheimes Wort zu finden, sondern auch, daß interne Zustandsvariablen bestimmte Werte anzunehmen, also einen einen Teilnehmer davon zu überzeugen, daß ein Wort bestimmte Eigenschaften hat, die es nicht besitzt. Ein Protokoll ist daher unsicher, wenn Angreifer nicht in der Lage ist ein geheimes Wort zu lernen und wenn er ein Wort lernen oder generieren kann und einem ehrlichen Nutzer zu überzeugen, daß das Wort Eigenschaften eines geheimen Wortes besitzt, so z.B. ein von ihm generiertes Wort ein Sessionkey ist.
Ein weiterer Unterschied zum Dolev und Yao Modell ist, daß keine Protokollklassen definiert und effiziente Algorithmen zu deren Verifizierung bestimmt werden, sondern eine allgemeinere Prozedur für verschiedene Arten von Protokollen (key managment- und Authentifizierungsprotokolle) entwickelt wurde.
Es folgt nun eine formale Beschreibung des Modells nach [1], wobei dieses Paper von 1992 stammt und nicht alles abdeckt, was später im Analyzer implementiert wurde, zudem wird der Analyzer dort noch nicht als ,,NRL Protocol Analyzer`` bezeichnet. Deswegen beschreibe ich im darauffolgenden Kapitel den Analyzer nach [3]. Dies soll nur noch einmal die Verwendung des Analyzers veranschaulichen, weswegen ich dort nicht zu sehr ins Detail gehen werde.