Einschränkungen des Analyzers

Es gibt einige Eigenschaften in kryptographischen Systemen, die nicht als rewrite-rules wiedergegeben werden können, so zum Beispiel kommutative Operationen (z.B. bei RSA). Solche können nicht im Analyzer modelliert werden und somit Fehler die damit zusammenhängen nicht gefunden werden. Hier will man aber nach anderen allgemeineren Gleichungstheorien suchen, welche Unifikationen.

Der Analyzer kann nur nach definierten unsicheren Zuständen suchen. So kann man zwar bestimmen, ob bestimmte Fehler existieren, man kann jedoch nicht generell sagen, daß das Protokoll sicher ist. Hier versucht man eine universelle Sprache zu entwickeln, um kryptographische Anfordung anzugeben, die unabhängig vom Protokoll ist.

Zudem kann der Analyzer auch keine Fehler in den verwendeten kryptographischen System finden, da er diese, wie die anderen Tools auch, nicht abbildet.