Die Sicherheit von Daten hängt heutzutage nicht mehr allein von den verwendeten kryptographischen Algorithmen ab. Einen ebenso großen Einfluss haben die kryptographischen Protokolle, welche bei der Übertragung dieser Daten bzw. zur Errichtung eines sicheren Übertragungskanals eingesetzt werden. Daraus leitet sich das Bedürfnis ab, die Sicherheit solcher Protokolle mit formalen Methoden zu überprüfen.
Das hier vorgestellte Verfahren modelliert das zu untersuchende Protokoll mit asynchronen Produktautomaten (kurz APA) und gehört damit in die Klasse der Modelle, welche auf Zustandsautomaten basieren. Wie auch bei anderen Methoden lassen sich hierbei lediglich Sicherheitslücken nicht jedoch die Sicherheit eines Protokolls nachweisen.
Ein erstes Problem bei der formalen Analyse von Protokollen liegt bereits in deren Spezifikation. Häufig liegen solche Protokollspezifikationen nicht vollständig formal vor, sondern enthalten bereits implizite Annahmen über die verwendeten Verschlüsselungsalgorithmen oder interne Aktionen der einzelnen Protokoll-Agenten. Die Sicherheit von Protokollen hängt jedoch auch von Informationen ab, die informal oder implizit vorliegen.
Viele Analysemodelle setzen voraus, daß die beteiligten Agenten die Typen von einzelnen Nachrichtenelementen überprüfen können, und so z.B. einfache Zufallszahlen von Schlüsseln unterscheiden können. In der Praxis gibt es jedoch Angriffe, die auf Typen-Verwirrung basieren. Mit dem hier vorgestellte Verfahren kann sehr genau modelliert werden, welche Typprüfungen vorgenommen werden und welche nicht. Zur Demonstration wird im folgenden ein Angriff auf das Needham-Schroeder Protokoll präsentiert, welcher nicht auf kompromittierten Sitzungsschlüsseln basiert.
Das Verfahren zur Modellierung kryptographischer Protokolle wurde von S. Gürgens, P. Ochsenschläger und C. Rudolph entwickelt und 2001 in einem GMD-Report (GMD - Gesellschaft für Mathematik und Datenverarbeitung) veröffentlicht. Zu Analyse der Protokolle (bzw. des entsprechenden APA) wird das Simple Homomorphism Verification Tool (kurz SHVT) eingesetzt, welches von P. Ochsenschläger, J. Repp, R. Rieke und U. Nitsche entwickelt wurde.