Title: Verifying security protocols by knowledge analysis

Authors: Xiaoqi Ma, Xiaochun Cheng

Addresses: School of Systems Engineering, The University of Reading, UK. ' Beijing Normal University, China; The University of Reading, UK; Middlesex University, UK

Abstract: This paper describes a new interactive method to analyse knowledge of participants involved in security protocols and further to verify the correctness of the protocols. The method can detect attacks and flaws involving interleaving sessions besides normal attacks. The implementation of the method in a generic theorem proving environment, namely Isabelle, makes the verification of protocols mechanical and efficient; it can verify a medium-sized security protocol in less than ten seconds. As an example, the paper finds the flaw in the Needham-Schroeder public key authentication protocol and proves the secure properties and guarantees of the protocol with Lowe|s fix to show the effectiveness of this method.

Keywords: security protocols; knowledge-based systems; KBS; formal verification; attacks; flaws; interleaving sessions; public key authentication; information security.

DOI: 10.1504/IJSN.2008.020092

International Journal of Security and Networks, 2008 Vol.3 No.3, pp.183 - 192

Published online: 26 Aug 2008 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article