TY - JOUR
T1 - Formal verification
T2 - An imperative step in the design of security protocols
AU - Coffey, Tom
AU - Dojen, Reiner
AU - Flanagan, Tomas
PY - 2003/12/5
Y1 - 2003/12/5
N2 - 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.
AB - 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.
KW - BCY protocol attack
KW - Cryptography
KW - Formal verification
KW - Modal logics
KW - Security protocols
UR - http://www.scopus.com/inward/record.url?scp=0142125896&partnerID=8YFLogxK
U2 - 10.1016/S1389-1286(03)00292-5
DO - 10.1016/S1389-1286(03)00292-5
M3 - Article
AN - SCOPUS:0142125896
SN - 1389-1286
VL - 43
SP - 601
EP - 618
JO - Computer Networks
JF - Computer Networks
IS - 5
ER -