Kryptographische Protokolle benutzen kryptographische Elemente, wie Verschlüsselung, um z.B. sicher Schlüssel zu verteilen (key distribution) oder Teilnehmer und Dienste zu authentifizieren. Dies soll über Netzwerke passieren, die möglicherweise von Angreifern belauscht werden, welche genau dies verhindern wollen. So z.B. kann ein Angreifer versuchen bei der key distribution den session key zu erhalten oder einen selbst erstellten key als session key zu verteilen. Den Angreifern wird dies meist durch Fehler in den Protokollen und weniger durch Fehler in den Verschlüsselungsalgorithmen oder durch deren Schwäche ermöglicht. In der Vergangenheit wurden immer wieder Fehler in solchen Protokollen gefunden, nachdem sie veröffentlicht oder gar schon lange in der Verwendung waren und als sicher galten. Um dies zu verhindern und somit ein Missbrauch vorzubeugen versucht man die kryptographischen Protokolle auf deren Sicherheit zu überprüfen. Da informale Analysen oft auch schon bei einfachen Protokollen nicht ausreichen, werden schon seit einiger Zeit formale Techiken zur Verifizierung solcher Protokolle entwickelt. Dazu gibt es verschieden Ansätze, welche mehr oder weniger die ,,reale Welt`` und die Möglichkeiten des Angreifers abbilden können und überprüfen, ob das Protokoll seine Ziele erfüllt. Diese lassen sich grundlegend in folgende Klassen unterteilen:
Der ,,NRL Protocol Analyzer`` verbindet, ähnlich wie der Interrogator oder das Modell von Dolev und Yao[4], auf dem es zudem basiert, den algebraischen Ansatz mit den der Zustandsmaschinen. Er kann verwendet werden um sicherheitsrelevante Eigentschaften eines Protokolles zu überprüfen, als auch Fehler in diesen zu finden.