Formal verification: an imperative step in the design of security protocols

Traditionally, security protocols have been designed and verified using informal techniques. However, the absence of formal verification can lead to security errors remaining undetected. Formal verification techniques, on the other hand, provide a systematic way of discovering protocol flaws. This paper discusses the process of formal verification using modal logics. The verification process is demonstrated by way of case studies on three security protocols, which are designed for use in mobile communications. Our formal analysis discovers all known flaws in the three chosen protocols. Further, a hitherto unknown flaw is identified in these protocols. This flaw causes a protocol failure, which can be exploited in an attack where an adversary impersonates a legitimate protocol participant. A new protocol, resistant to this attack, is proposed and formally verified, giving confidence in the correctness of the protocol. The result of these case studies, where formal verification successfully discovers all these flaws, demonstrates that using formal verification techniques is an imperative step in the design of security protocols. (C) 2003 Elsevier B.V. All rights reserved.