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

摘要：

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

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

所属期刊栏目：10

分类号：TP309(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant Nos.61163005,61562026;the Natural Science Foundation of Jiangxi Province under Grant Nos.20132BAB201033,20161BAB202063;the Science and Technology International Cooperation Project of Jiangxi Province under Grant No.20151BDH80005;the Soft Science Research Project of Jiangxi Province under Grant No.20151BBA10042;the Science and Technology Ground Project of College in Jiangxi Province under Grant No.KJLD13038;the Program of Co-Innovation Center of the Intelligent Management and Equipment for Orchard on the Hilly Land in South China;the Special Funds for Visiting Scholars Development Plan of the Young Teachers in the Ordinary Universities of Jiangxi Province

在线出版日期：2017-02-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1701-1710