Die Sicherheit kryptographischer Protokolle hängt oft von impliziten Annahmen oder informal gegebenen Informationen ab. In dieser Ausarbeitung wurde ein Angriff auf das Needham-Schroeder Protokoll präsentiert, welcher nur möglich ist, wenn die Agenten Zufallszahlen und Schlüssel nicht unterscheiden können und einer der Agenten die ankommenden Nachrichten nicht auf die Anzahl ihrer Komponenten überprüft. Der Angriff steht und fällt also mit Implementationsdetails, die nicht unbedingt in der Protokollspezifikation behandelt werden.
Bei der Modellierung kryptographischer Protokolle mit asynchronen Produktautomaten werden keine implizite Annahmen verwendet. Alle Annahmen auf denen die Sicherheit das Protokolls basiert müssen explizit spezifiziert werden. Am Beispiel des Needham-Schroeder Protokolls wurde die Modellierung durch APA demonstriert.
Zur Analyse des APA wird vom Simple Homomorphism Verification Tool eine Suche auf dem endlichen Zustandsraum durchgeführt. Das SHVT arbeitet dabei auf speziellen Abstraktionen des Originalsystems, um mit den im allgemeinen sehr großen Zustandsräumen fertig zu werden. Die dabei erreichbare Reduktion des Zustandsraumes ermöglicht dann die Analyse größerer praxisrelevanter Systeme bzw. komplexerer Protokolle. Wurde bei der Analyse des Protokolls ein unsicherer Zustand gefunden, so kann ein dorthin führender Pfad berechnet werden, welcher das genaue Problem aufzeigt.