Verifying Authentication Protocol Implementations
Steve A. Schneider · 2002
Formal methods for verifying authentication protocols tend to assume an idealised, perfect form of encryption. This approach has been spectacularly successful in finding flaws, but when we aim for proofs of correctness then we need to consider this assumption more carefully, and perhaps to weaken it to reflect properties of real cryptographic mechanisms. This paper reviews the existing CSP approach to verifying protocols, and considers how algebraic properties of real cryptographic mechanisms can be incorporated within a rank function verification. The approach is illustrated with an authentication protocol which makes use of exclusive-or. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.