计算机科学与探索 ›› 2016, Vol. 10 ›› Issue (12): 1701-1710.DOI: 10.3778/j.issn.1673-9418.1607032

• 网络与信息安全 • 上一篇    下一篇

基于强认证理论的三方网络协议安全性证明

肖美华1,刘欣倩1,2+,李娅楠1,程道雷1,梅映天1   

  1. 1. 华东交通大学 软件学院,南昌 330013
    2. 中国人民财产保险股份有限公司宁波市分公司 信息技术部,浙江 宁波 315000
  • 出版日期:2016-12-01 发布日期:2016-12-07

Security Certification of Three-Party Network Protocols Based on Strong Authentication Theory

XIAO Meihua1, LIU Xinqian1,2+, LI Yanan1, CHENG Daolei1, MEI Yingtian1   

  1. 1. School of Software, East China Jiaotong University, Nanchang 330013, China
    2. Department of Information and Technology, PICC Property and Casualty Company Limited (Ningbo Branch), Ningbo, Zhejiang 315000, China
  • Online:2016-12-01 Published:2016-12-07

摘要: 形式化方法是分析网络安全协议的一种重要方法,网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于证明网络安全协议的安全性。以事件逻辑为基础,定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究,分析得出发送者是安全的而接收者是不安全的,从而证明了该协议是不安全的,说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。

关键词: 形式化方法, 事件逻辑, 强认证理论, Neuman-Stubblebine协议

Abstract: Formal method is an important approach for analyzing network security protocols. Network protocol secu-rity is a research hotspot in information security field. Event logic is a formalism for describing transition between states in a distributed system. It’s common to use event logic to certify the security of network security protocols. Based on event logic, this paper defines strong match and match sessions, and proposes the strong authentication theory by combining event logic axioms and inference rules. Using the strong authentication theory, this paper proves that three-principal Neuman-Stubblebine protocol is not secure because the sender is secure and the receiver isn’t secure. The research results show that the strong authentication theory is applicable to the security certification of similar multi-party security protocols.

Key words: formal method, event logic, strong authentication theory, Neuman-Stubblebine protocol