魯來鳳，段新東，馬建峰

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

1 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 PCL擴(kuò)展

1) 擴(kuò)展1

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

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

2) 擴(kuò)展2

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

3.2 協(xié)議本身建模

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

3.3 安全屬性建模

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

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

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

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

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

下面將對(duì)各個(gè)子協(xié)議模塊及組合協(xié)議進(jìn)行證明。

4.1 子模塊Q1證明

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

證明 引理1描述的是以角色A的形式執(zhí)行協(xié)議Q1的情形，詳細(xì)的證明過程如圖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成立，詳細(xì)證明過程如圖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成立，詳細(xì)證明過程如圖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]ψ，其中，

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

5 結(jié)束語

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

本文選取認(rèn)證密鑰分配協(xié)議Otway-Rees協(xié)議作為研究對(duì)象，利用協(xié)議組合邏輯作為協(xié)議證明工具展開研究。給出了Otway-Rees協(xié)議常見的攻擊形式，分析了存在的缺陷，提出了改進(jìn)方案（AOR協(xié)議）；為了更好地形式化描述AOR協(xié)議，對(duì)傳統(tǒng)的PCL進(jìn)行了擴(kuò)展；緊接著，用擴(kuò)展后的PCL對(duì)改進(jìn)的協(xié)議中各個(gè)實(shí)體的行為和協(xié)議的安全屬性進(jìn)行形式化描述，將改進(jìn)后的協(xié)議進(jìn)行模塊化劃分，并利用PCL進(jìn)行組合證明。最后，得出是改進(jìn)后的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ìn)展[J].軟件學(xué)報(bào).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é)議的形式化分析與驗(yàn)證[M].北京:機(jī)械工業(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.