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）”概念的协议编程语言形式化描述协议本身及其执行的过程（区别于非形式化的箭头—信息表示法）；协议逻辑用来描述协议的安全属性（主要包括认证性和保密性），包括逻辑语法（Syntax，描述安全属性本身）和逻辑语义（Semantics，描述安全属性的含义）；证明系统包含了用于形式化证明的若干公理和推理规则以及不同形式的协议安全性证明方法。

2 Otway-Rees协议及改进

Otway-Rees[4]认证协议采用的是基于可信第三方的通信机制，参加协议的主体有3个：包括通信双方A、B，还有认证服务器S。该协议交互过程如图1所示。

图1 Otway-Rees认证协议

其中，A、B表示协议的参与方；T表示协议攻击者；S表示认证服务器；Na、Nb分别是A、B随机取定的值，用来保证A、B收到的消息是S最近发出的，而不是一个重放的消息；M是A随机取定的值，帮助A识别它和S间的通信是由B转发的；Kas、Kbs是S分别与A、B共享的密钥；Kab由S生成，作为A和B之间通信的会话密钥。

由协议描述可得，（M，A，B）在通信过程中都是公开的。攻击者T首先截获从B发给服务器S的消息，去掉明文消息（A，B）后，冒充S重发消息，由于消息位数的特殊性，使A，B误认（M，A，B）是会话密钥，这样攻击者成功地进行了攻击，今后可以用会话密钥（M，A，B）窃听A和B之间的会话。

类似地，攻击者T还可以冒充B，重放消息（1）中的加密分量，将它作为消息（4）中的加密分量发送给A。这里针对Otway-Rees协议的攻击就是一个典型的类型缺陷攻击，攻击之所以能成功是因为协议的描述对于协议中出现的变量没有提供足够的明确的类型信息，消息相关的名字不是很明确，协议实现时的消息格式过于对称。

另外，该协议还有一个缺陷，就是在消息（4）中，A收到了B发来的消息，通过解密获得了S分发的会话密钥Kab，但它并不能确定B是否也已经获得了同样的会话密钥。

鉴于以上的协议攻击形式及缺陷分析，对协议改进如下（amended Otway-Rees，记为AOR协议）：

第一是在3）、4）消息中增加身份信息，使得消息身份信息明确，同时能够避免因消息结构固定、对称而引起的攻击；第二是在3）、4）消息第一个加密项中添加Nb同时在消息4）中增加消息分量{Nb}Kab，使得A能够确定它所收到的会话密钥是否与B收到的一致。

3 改进型的Otway-Rees协议建模

为了更好地形式化描述改进型的Otway-Rees协议，需要对传统的PCL进行一定的扩展。在此基础上，可以进行协议建模工作。协议的建模工作又分为协议本身的形式化和协议安全属性的形式化描述。

3.1 PCL扩展

1) 扩展1

基本的PCL语法系统是针对公钥密码体制。本文为了更好地描述基于对称密码体制的Otway-Rees协议，扩展了对称加解密语法如下。

定义对称加解密的动作sec_sk和dec_sk。具体含义为：(sec_sk u，K)表示对称密码系统中用密钥K加密表示对称系统中用对u进行解密，由于对称密码体制中K=，有时加解密密钥均使用K。

2) 扩展2

扩展定义协议项的减法动作“-”：t-t1代表从组合项t中剔除子项t1，若项t中不包含子项t1，则该操作无意义，直接返回t。例如令t=(t1，t2)即t是由不相同的项t1与t2拼接起来的项，则此时t-t1的结果为t2。

3.2 协议本身建模

采用PCL描述上述改进型协议AOR实体执行协议模型，有协议交互方A，B和服务器S 3个角色，它们的执行过程分别如下。

3.3 安全属性建模

Otway-Rees协议主要功能是完成发起者和响应者之间的双向认证，并且分发服务器产生的会话密钥。会话密钥的保密性是基本的要求，本文主要讨论该安全属性。

定义1 改进型Otway-Rees协议（简写成AOR协议）的密钥保密性。

当公式φAOR-Sec成立时，Otway-Rees协议能够保证密钥保密性。其中，

4 改进型的Otway-Rees协议证明

首先，将协议进行划分。改进型Otway-Rees协议记为Q，它包含3个主体，分别为通信主体A、B和服务器S，将协议Q划分为3个子协议模块Q1、Q2和Q3，其中，Q1包含消息1），Q2包含消息2）和3），Q3包含消息4）。

下面将对各个子协议模块及组合协议进行证明。

4.1 子模块Q1证明

引理1 Φ[Q1]Aψ1成立，其中，

证明 引理1描述的是以角色A的形式执行协议Q1的情形，详细的证明过程如图2所示。

图2 引理1的证明过程

从图2中式（8）能够得出引理3成立。

若以角色B的形式执行协议Q1，类似的结论显然成立。所以有定理1成立。

定理1 Φ[Q1]ψ1成立，其中，

4.2 子模块Q2证明

引理2 ψ1[Q2]Sψ2成立，其中，

证明 若按照角色S来执行协议Q2，引理2成立，详细证明过程如图3所示。

图3 引理2的证明过程

若按角色B的方式执行协议Q2有类似的结论成立。所以有定理2成立。

定理2 ψ1[Q2]ψ2成立，其中，

4.3 子模块Q3证明

引理3 ψ2[Q3]Bψ成立，其中，

证明 若按照角色B来执行协议Q3，引理3成立，详细证明过程如图4所示。

图4 引理3的证明过程

若按角色A的方式执行协议Q3，有类似的结论成立。所以有定理3成立。

定理3 ψ2[Q3]ψ成立，其中，

4.4 协议组合证明

由定理1、定理2和定理3可知，Φ[Q1]ψ1,ψ1[Q2]ψ2,ψ2[Q3]ψ成立，其中，Φ=Has(A,Kas)∧

根据模态顺序组合规则S1[9]，由定理1、定理2，有公式Φ[Q1Q2]ψ2成立。由该公式和定理3，再次应用模态顺序组合规则S1，可得如下公式：Φ[Q1Q3Q3]ψ，其中，

即改进型的Otway-Rees协议满足密钥的保密属性。

5 结束语

安全协议是现代网络系统安全性的基石，安全协议安全性分析是一项紧迫且意义重大的工作。自BAN逻辑[10]被提出以来，用形式化的方法分析安全协议的安全性已成为信息安全研究的热点之一[3]。

本文选取认证密钥分配协议Otway-Rees协议作为研究对象，利用协议组合逻辑作为协议证明工具展开研究。给出了Otway-Rees协议常见的攻击形式，分析了存在的缺陷，提出了改进方案（AOR协议）；为了更好地形式化描述AOR协议，对传统的PCL进行了扩展；紧接着，用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述，将改进后的协议进行模块化划分，并利用PCL进行组合证明。最后，得出是改进后的AOR协议具有密钥保密属性。

[1] 范红,冯登国.安全协议理论与方法[M].北京:科学出版社, 2003.FAN H, FENG D G. Theories and Methods for Security Protocols[M].Beijing: Science Press, 2003.

[2] 卿斯汉.安全协议20年研究进展[J].软件学报.2003,14(10):1740- 1752.QING S H. Twenty years development of security protocols research[J]. Journal of Software. 2003, 14(10): 1740-1752.

[3] 李建华,张爱新,薛质等.网络安全协议的形式化分析与验证[M].北京:机械工业出版社.2010.LI J H, ZHANG A X, XUE Z, etal. Formal Analysis and Verification of Network Security Protocols[M]. Beijing: China Machine Press.2010.

[4] OTWAY D, REES O. Efficient and timely mutual authentication[J].Operating Systems Review, 1987, 21(1):8-10.

[5] DATTA A. Security Analysis of Network Protocol: Compositional Reasoning and Complexity Theoretic Foundations[D]. Computer Science Department, Stanford University, September 2005.8-72.

[6] DATTA A, DEREK A, MITCHELL J, etal. Secure protocol composition[A]. Proceedings of the 2003 ACM workshop on Formal methods in security engineering[C]. 2003. 11-23.

[7] DURGIN N, MITCHELL J, PAVLOVIC D. A compositional logic for proving security properties of protocols[J]. Journal of Computer Security, 2003, 11(4): 677-721.

[8] ROY A, DATTA A, DEREK A, etal. Secrecy analysis in protocol composition logic[A]. Advances in Computer Science-ASIAN. 2006.Secure Software and Related Issues[C].2006. 197-213.

[9] DATTA A, ROY A, MITCHELL J C, etal. Protocol composition logic(PCL)[J]. Electronic Notes in Theoretical Computer Science,2007,172(1): 311-358.

[10] BURROWS M, ABADI M, NEEDHAM R. A logic of authentication[J]. ACM Transactions on Computer Systems, 1990, 8(1): 18-36.