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

• 作者: 刘欣倩 李娅楠 梅映天 程道雷 肖美华
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 形式化方法 事件逻辑 强认证理论 Neuman-Stubblebine协议
• 年，卷（期）: 2016,（12）
• 所属期刊栏目: 网络与信息安全
• 页码范围: 1701-1710
• 页数: 10页
• 分类号: TP309
• 字数: 8035字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1607032

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖美华	华东交通大学软件学院	18	92	6.0	9.0
2	梅映天	华东交通大学软件学院	7	26	3.0	5.0
3	李娅楠	华东交通大学软件学院	7	18	3.0	4.0
4	程道雷	华东交通大学软件学院	4	22	3.0	4.0
5	刘欣倩	华东交通大学软件学院	3	20	3.0	3.0