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

来源：计算机科学与探索杂志2016年第12期北京时间：

作者：肖美华，刘欣倩，李娅楠，程道雷，梅映天

单位：1. 华东交通大学 软件学院，南昌 3300132. 中国人民财产保险股份有限公司宁波市分公司 信息技术部，浙江 宁波 315000

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

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