Otway-Rees协议改进及形式化证明

鲁来凤，段新东，马建峰

（1. 陕西师范大学 数学与信息科学学院，陕西 西安 710062；2. 南阳理工学院 软件学院，河南 南阳 473004；3. 西安电子科技大学 计算机网络与信息安全教育部重点实验室，陕西 西安 710071）

1 引言

安全协议的安全性分析一直是一个复杂而困难的问题，对安全协议的研究己成为世界上信息与网络安全方面的一个重要研究方向[1,2]。实践证明，形式化方法是安全协议安全性分析更为可靠和有效的途径[3]。

Otway-Rees认证协议[4]是由Dave Otway和Owen Rees提出的基于共享密钥的认证密钥分配协议，其目标是完成发起者和响应者之间的双向认证，并且分发服务器产生的会话密钥。该协议的特点是简单实用，没有使用复杂的同步时钟机制或双重加密，仅用少量的信息提供了良好的时效性。但该协议并不安全，存在缺陷，易受到攻击。因此有必要对它改进并进行形式化的安全性证明，而协议组合逻辑(PCL)[5～9]就是一种新的针对协议安全性证明的有力工具。

PCL是由美国斯坦福大学信息安全实验室的Datta博士等人2003年提出来的，是一种新的Floyd-Hoare类型的组合逻辑推导系统。它采用标准逻辑概念，使用Cords演算描述协议，可以用来证明安全协议的认证性和私密性等安全属性，通过逻辑公理和模块化推理方法支持复杂安全协议的组合推理（包括并行组合和顺序组合）。PCL形式化系统由协议建模工具、协议逻辑和证明系统3部分构成。其中，协议模型化是使用基于“线索（Cords）”概念的协议编程语言形式化描述协议本身及其执行的过程（区别于非形式化的箭头—信息表示法）；……