欢迎访问中国科学院大学学报,今天是

中国科学院大学学报 ›› 2004, Vol. 21 ›› Issue (3): 380-385.DOI: 10.7523/j.issn.2095-6134.2004.3.015

• 综述 • 上一篇    下一篇

三方密码协议运行模式分析法

刘秀英1,3, 张玉清2,3, 杨波1, 邢戈2,3   

  1. 1. 西安电子科技大学信息安全教育部实验室, 西安 710071;
    2. 中国科学院研究生院信息安全国家重点实验室, 北京100039;
    3. 中国科学院研究生院国家计算机网络入侵防范中心, 北京 100039
  • 收稿日期:2003-05-16 修回日期:2003-07-01 发布日期:2004-05-10
  • 基金资助:

    国家自然科学基金项目 (60102004;60273027;60025205)资助

Running-Mode Analysis of the Three-Party Cryptographic Protocol

LIU XiuYing1,3, ZHANG YuQing2,3, YANG Bo1, XING Ge2,3   

  1. 1. National Key Laboratory of ISN, Xidian University, Xi’an 710071, China;
    2. State Key Laboratory of Information Security, Chinese Academy of Sciences, Beijing 100039, China;
    3. National Computer Network Intrusion Protection Center, Chinese Academy of Sciences, Beijing 100039, China
  • Received:2003-05-16 Revised:2003-07-01 Published:2004-05-10

摘要:

在两方密码协议运行模式分析法的基础上,利用模型检测的理论结果,提出了三方密码协议运行模式分析法。用这种方法对DavisSwick协议进行了分析,成功地验证了此协议的安全性,说明了所提出的三方密码协议运行模式分析法的有效性。

关键词: 密码协议, 形式化分析, 模型检测, 运行模式分析法

Abstract:

Based on the model checking theory, we derive the running mode analysis method of three party cryptographic protocols from the running mode analysis method of two party cryptographic protocols. To test this method, we use it to analyze the Davis Swick protocol and successfully prove the security of protocol. Therefore, we can draw a conclusion that running mode analysis of three party cryptographic protocol is available.

Key words: cryptographic protocol, formal analysis, model checking, running-mode analysis

中图分类号: