Computer Engineering and Applications ›› 2008, Vol. 44 ›› Issue (22): 97-99.DOI: 10.3778/j.issn.1002-8331.2008.22.030

• 网络、通信、安全 • Previous Articles     Next Articles

Strand space model of Yahalom-Paulson protocol and its analysis

DING Meng-wei,ZHOU Qing-lei,ZHAO Dong-ming   

  1. School of Information Engineering, Zhengzhou University, Zhengzhou 450052, China
  • Received:2007-10-10 Revised:2008-03-21 Online:2008-07-11 Published:2008-07-11
  • Contact: DING Meng-wei



  1. 郑州大学 信息工程学院,郑州450052
  • 通讯作者: 丁萌伟

Abstract: Strand spaces model is a new formal analysis tool to the analysis of cryptographic protocols.Furthermore,the proposition of the two concepts of ideal and honest simplifies the process of verification of cryptographic protocols.For the first time, based on the theory of strand space, Yahalom-Paulson protocol is analyzed from the aspects of both confidentiality and authentication.The analysis proves the correctness of the protocol.

Key words: cryptographic protocol, Yahalom-Paulson protocol, strand space, ideal

摘要: 串空间模型是一种新兴的密码协议形式化分析工具,其理论中理想和诚实概念的提出大大减少了协议的证明步骤。首次利用串空间理论从机密性和认证性两个方面对Yahalom-Paulson协议进行了分析。分析结果证明该协议是安全的。

关键词: 密码协议, Yahalom-Paulson协议, 串空间, 理想