Otway-Rees協(xié)議改進及形式化證明

魯來鳳，段新東，馬建峰

（1. 陜西師范大學(xué) 數(shù)學(xué)與信息科學(xué)學(xué)院，陜西 西安 710062；2. 南陽理工學(xué)院 軟件學(xué)院，河南 南陽 473004；3. 西安電子科技大學(xué) 計算機網(wǎng)絡(luò)與信息安全教育部重點實驗室，陜西 西安 710071）

1 引言

安全協(xié)議的安全性分析一直是一個復(fù)雜而困難的問題，對安全協(xié)議的研究己成為世界上信息與網(wǎng)絡(luò)安全方面的一個重要研究方向[1,2]。實踐證明，形式化方法是安全協(xié)議安全性分析更為可靠和有效的途徑[3]。

Otway-Rees認證協(xié)議[4]是由Dave Otway和Owen Rees提出的基于共享密鑰的認證密鑰分配協(xié)議，其目標是完成發(fā)起者和響應(yīng)者之間的雙向認證，并且分發(fā)服務(wù)器產(chǎn)生的會話密鑰。該協(xié)議的特點是簡單實用，沒有使用復(fù)雜的同步時鐘機制或雙重加密，僅用少量的信息提供了良好的時效性。但該協(xié)議并不安全，存在缺陷，易受到攻擊。因此有必要對它改進并進行形式化的安全性證明，而協(xié)議組合邏輯(PCL)[5～9]就是一種新的針對協(xié)議安全性證明的有力工具。

PCL是由美國斯坦福大學(xué)信息安全實驗室的Datta博士等人2003年提出來的，是一種新的Floyd-Hoare類型的組合邏輯推導(dǎo)系統(tǒng)。它采用標準邏輯概念，使用Cords演算描述協(xié)議，可以用來證明安全協(xié)議的認證性和私密性等安全屬性，通過邏輯公理和模塊化推理方法支持復(fù)雜安全協(xié)議的組合推理（包括并行組合和順序組合）。PCL形式化系統(tǒng)由協(xié)議建模工具、協(xié)議邏輯和證明系統(tǒng)3部分構(gòu)成。其中，協(xié)議模型化是使用基于“線索（Cords）”概念的協(xié)議編程語言形式化描述協(xié)議本身及其執(zhí)行的過程（區(qū)別于非形式化的箭頭—信息表示法）；協(xié)議邏輯用來描述協(xié)議的安全屬性（主要包括認證性和保密性），包括邏輯語法（Syntax，描述安全屬性本身）和邏輯語義（Semantics，描述安全屬性的含義）；證明系統(tǒng)包含了用于形式化證明的若干公理和推理規(guī)則以及不同形式的協(xié)議安全性證明方法。

2 Otway-Rees協(xié)議及改進

Otway-Rees[4]認證協(xié)議采用的是基于可信第三方的通信機制，參加協(xié)議的主體有3個：包括通信雙方A、B，還有認證服務(wù)器S。該協(xié)議交互過程如圖1所示。

圖1 Otway-Rees認證協(xié)議

其中，A、B表示協(xié)議的參與方；T表示協(xié)議攻擊者；S表示認證服務(wù)器；Na、Nb分別是A、B隨機取定的值，用來保證A、B收到的消息是S最近發(fā)出的，而不是一個重放的消息；M是A隨機取定的值，幫助A識別它和S間的通信是由B轉(zhuǎn)發(fā)的；Kas、Kbs是S分別與A、B共享的密鑰；Kab由S生成，作為A和B之間通信的會話密鑰。

由協(xié)議描述可得，（M，A，B）在通信過程中都是公開的。攻擊者T首先截獲從B發(fā)給服務(wù)器S的消息，去掉明文消息（A，B）后，冒充S重發(fā)消息，由于消息位數(shù)的特殊性，使A，B誤認（M，A，B）是會話密鑰，這樣攻擊者成功地進行了攻擊，今后可以用會話密鑰（M，A，B）竊聽A和B之間的會話。

類似地，攻擊者T還可以冒充B，重放消息（1）中的加密分量，將它作為消息（4）中的加密分量發(fā)送給A。這里針對Otway-Rees協(xié)議的攻擊就是一個典型的類型缺陷攻擊，攻擊之所以能成功是因為協(xié)議的描述對于協(xié)議中出現(xiàn)的變量沒有提供足夠的明確的類型信息，消息相關(guān)的名字不是很明確，協(xié)議實現(xiàn)時的消息格式過于對稱。

另外，該協(xié)議還有一個缺陷，就是在消息（4）中，A收到了B發(fā)來的消息，通過解密獲得了S分發(fā)的會話密鑰Kab，但它并不能確定B是否也已經(jīng)獲得了同樣的會話密鑰。

鑒于以上的協(xié)議攻擊形式及缺陷分析，對協(xié)議改進如下（amended Otway-Rees，記為AOR協(xié)議）：

第一是在3）、4）消息中增加身份信息，使得消息身份信息明確，同時能夠避免因消息結(jié)構(gòu)固定、對稱而引起的攻擊；第二是在3）、4）消息第一個加密項中添加Nb同時在消息4）中增加消息分量{Nb}Kab，使得A能夠確定它所收到的會話密鑰是否與B收到的一致。

3 改進型的Otway-Rees協(xié)議建模

為了更好地形式化描述改進型的Otway-Rees協(xié)議，需要對傳統(tǒng)的PCL進行一定的擴展。在此基礎(chǔ)上，可以進行協(xié)議建模工作。協(xié)議的建模工作又分為協(xié)議本身的形式化和協(xié)議安全屬性的形式化描述。

3.1 PCL擴展

1) 擴展1

基本的PCL語法系統(tǒng)是針對公鑰密碼體制。本文為了更好地描述基于對稱密碼體制的Otway-Rees協(xié)議，擴展了對稱加解密語法如下。

定義對稱加解密的動作sec_sk和dec_sk。具體含義為：(sec_sk u，K)表示對稱密碼系統(tǒng)中用密鑰K加密表示對稱系統(tǒng)中用對u進行解密，由于對稱密碼體制中K=，有時加解密密鑰均使用K。

2) 擴展2

擴展定義協(xié)議項的減法動作“-”：t-t1代表從組合項t中剔除子項t1，若項t中不包含子項t1，則該操作無意義，直接返回t。例如令t=(t1，t2)即t是由不相同的項t1與t2拼接起來的項，則此時t-t1的結(jié)果為t2。

3.2 協(xié)議本身建模

采用PCL描述上述改進型協(xié)議AOR實體執(zhí)行協(xié)議模型，有協(xié)議交互方A，B和服務(wù)器S 3個角色，它們的執(zhí)行過程分別如下。

3.3 安全屬性建模

Otway-Rees協(xié)議主要功能是完成發(fā)起者和響應(yīng)者之間的雙向認證，并且分發(fā)服務(wù)器產(chǎn)生的會話密鑰。會話密鑰的保密性是基本的要求，本文主要討論該安全屬性。

定義1 改進型Otway-Rees協(xié)議（簡寫成AOR協(xié)議）的密鑰保密性。

當公式φAOR-Sec成立時，Otway-Rees協(xié)議能夠保證密鑰保密性。其中，

4 改進型的Otway-Rees協(xié)議證明

首先，將協(xié)議進行劃分。改進型Otway-Rees協(xié)議記為Q，它包含3個主體，分別為通信主體A、B和服務(wù)器S，將協(xié)議Q劃分為3個子協(xié)議模塊Q1、Q2和Q3，其中，Q1包含消息1），Q2包含消息2）和3），Q3包含消息4）。

下面將對各個子協(xié)議模塊及組合協(xié)議進行證明。

4.1 子模塊Q1證明

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

證明 引理1描述的是以角色A的形式執(zhí)行協(xié)議Q1的情形，詳細的證明過程如圖2所示。

圖2 引理1的證明過程

從圖2中式（8）能夠得出引理3成立。

若以角色B的形式執(zhí)行協(xié)議Q1，類似的結(jié)論顯然成立。所以有定理1成立。

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

4.2 子模塊Q2證明

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

證明 若按照角色S來執(zhí)行協(xié)議Q2，引理2成立，詳細證明過程如圖3所示。

圖3 引理2的證明過程

若按角色B的方式執(zhí)行協(xié)議Q2有類似的結(jié)論成立。所以有定理2成立。

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

4.3 子模塊Q3證明

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

證明 若按照角色B來執(zhí)行協(xié)議Q3，引理3成立，詳細證明過程如圖4所示。

圖4 引理3的證明過程

若按角色A的方式執(zhí)行協(xié)議Q3，有類似的結(jié)論成立。所以有定理3成立。

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

4.4 協(xié)議組合證明

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

根據(jù)模態(tài)順序組合規(guī)則S1[9]，由定理1、定理2，有公式Φ[Q1Q2]ψ2成立。由該公式和定理3，再次應(yīng)用模態(tài)順序組合規(guī)則S1，可得如下公式：Φ[Q1Q3Q3]ψ，其中，

即改進型的Otway-Rees協(xié)議滿足密鑰的保密屬性。

5 結(jié)束語

安全協(xié)議是現(xiàn)代網(wǎng)絡(luò)系統(tǒng)安全性的基石，安全協(xié)議安全性分析是一項緊迫且意義重大的工作。自BAN邏輯[10]被提出以來，用形式化的方法分析安全協(xié)議的安全性已成為信息安全研究的熱點之一[3]。

本文選取認證密鑰分配協(xié)議Otway-Rees協(xié)議作為研究對象，利用協(xié)議組合邏輯作為協(xié)議證明工具展開研究。給出了Otway-Rees協(xié)議常見的攻擊形式，分析了存在的缺陷，提出了改進方案（AOR協(xié)議）；為了更好地形式化描述AOR協(xié)議，對傳統(tǒng)的PCL進行了擴展；緊接著，用擴展后的PCL對改進的協(xié)議中各個實體的行為和協(xié)議的安全屬性進行形式化描述，將改進后的協(xié)議進行模塊化劃分，并利用PCL進行組合證明。最后，得出是改進后的AOR協(xié)議具有密鑰保密屬性。

[1] 范紅,馮登國.安全協(xié)議理論與方法[M].北京:科學(xué)出版社, 2003.FAN H, FENG D G. Theories and Methods for Security Protocols[M].Beijing: Science Press, 2003.

[2] 卿斯?jié)h.安全協(xié)議20年研究進展[J].軟件學(xué)報.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] 李建華,張愛新,薛質(zhì)等.網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗證[M].北京:機械工業(yè)出版社.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.