%0 Journal Article %A 肖美华 %A 刘欣倩 %A 李娅楠 %A 程道雷 %A 梅映天 %T 基于强认证理论的三方网络协议安全性证明 %D 2016 %R 10.3778/j.issn.1673-9418.1607032 %J 计算机科学与探索 %P 1701-1710 %V 10 %N 12 %X 形式化方法是分析网络安全协议的一种重要方法,网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于证明网络安全协议的安全性。以事件逻辑为基础,定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究,分析得出发送者是安全的而接收者是不安全的,从而证明了该协议是不安全的,说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。 %U http://fcst.ceaj.org/CN/10.3778/j.issn.1673-9418.1607032