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

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

作　　者：肖美华[1] 刘欣倩 李娅楠[1] 程道雷 梅映天 XIAO Meihua;LIU Xinqian;LI Yanan;CHENG Daolei;MEI Yingtian(School of Software, East China Jiaotong University, Nanchang 330013, China;Department of Information and Technology, PICC Property and Casualty Company Limited (Ningbo Branch),Ningbo, Zhejiang 315000, China)

机构地区：[1]华东交通大学软件学院,南昌330013 [2]中国人民财产保险股份有限公司宁波市分公司信息技术部,浙江宁波315000

出　　处：《计算机科学与探索》2016年第12期1701-1710,共10页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金Nos.61163005;61562026;江西省自然科学基金Nos.20132BAB201033;20161BAB202063;江西省对外科技合作技术项目No.20151BDH80005;江西省软科学研究计划项目No.20151BBA10042;江西省高校科技落地计划项目No.KJLD13038;南方山地果园智能化管理与装备协同创新中心资助项目;江西省普通本科高校中青年教师发展计划访问学者专项资金~~

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]