Verifying security protocols by knowledge analysis

被引：4
作者：
School of Systems Engineering, The University of Reading, Reading, United Kingdom [1 ]
不详 [2 ]
不详 [3 ]
机构：
[1] School of Systems Engineering, The University of Reading, Reading
[2] Beijing Normal University, Beijing
[3] Middlesex University, Middlesex
来源：
Int. J. Secur. Netw. | 2008年 / 3卷 / 183-192期
关键词：
Formal verification; Knowledge-based system; Security protocol;
D O I：
10.1504/IJSN.2008.020092
中图分类号：
学科分类号：
摘要：
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. © 2008, Inderscience Publishers.
引用
收藏
页码：183 / 192
页数：9
相关论文
共 20 条
  • [1] Bella G., Massacci F., Paulson L., An overview of the verification of SET, International Journal of In formation Security, 4, 1-2, pp. 17-28, (2005)
  • [2] Bolignano D., An approach to the formal verification of cryptographic protocols, Proceedings of the 3rd ACM Conference on Computer and Communications Security, pp. 106-118, (1996)
  • [3] Burrows M., Abadi M., Needham R., A logic of authentication, ACM Transactions on Computer Systems, 8, 1, pp. 18-36, (1990)
  • [4] Chen Q., The Verification Logic for Secure Transaction Protocols, (2004)
  • [5] Chen Q., Zhang C., Zhang S., A logical framework ENDL for verifying secure transaction protocols, Knowledge and Information Systems, 7, 1, pp. 84-109, (2005)
  • [6] Cheng X., Ma X., Cheng M., Huang S.C.-H., Proving secure properties of cryptographic protocols, Proceedings of the 24th IEEE International Performance Computing and Communications Conference (IPCCC 2005), pp. 3-9, (2005)
  • [7] Kim I., Choi J., Formal verification of PAP and EAP-MD5 protocols in wireless networks: FDR model checking, Proceedings of the 18th International Conference on Advanced Information Networking and Applications, pp. 264-269, (2004)
  • [8] Liebl A., Authentication in distributed systems: A bibliography, ACM SIGOPS Operating Systems Review, 27, 4, pp. 122-136, (1993)
  • [9] Lowe G., An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, 56, 3, pp. 131-133, (1995)
  • [10] Lowe G., Breaking and fixing the Needham-Schroeder public-key protocol using FDR, Lecture Notes in Computer Science, 1055, pp. 147-166, (1996)
12