1 引言

安全協議的分析一直受到重視和廣泛關注，專家和學者們提出了很多分析安全

協議的形式化方法。這些安全協議的形式化分析方法，基本上可以分為四類

^[1]：模態邏輯法、模型檢測法（狀態空間搜索法）、定理證明法和安全協議

的可證明安全法。

而串空間(Strand Space)是基于定理證明的一種分析方法。1998 年，Fabrega、Herzog和Guttman提出了協議的串(strand)空間模型^[2]，并應用該理論證明了Needham-Schroeder-Lowe公鑰認證協議的正確性。“該方法吸納了NRL協議分析器^[3]，Schneider秩函數和Paulson歸納法^[4]等思想”，是一種新型有效的協議形式化分析方法。串空間模型是一個有很多優點的安全協議形式化分析方法^[5]：可以進行基本的協議正確性證明；通過引入入侵者串，能找出攻擊方法；可以給出基于串空間模型的協議設計方法。由于其功能的全面性,串空間方法的研究得到了較大的發展。

基金項目：云南省教育廳科學研究基金項目（07C10075）；昆明理工大學科學研究基金項目（2007-29）

本文用串空間模型分析了改進的Woo-Lam認證協議。

2 Strand空間基本概念

本節介紹串空間理論的基本概念^[6]：消息術語，串，串空間以及從，最后給出介紹攻擊者串模型的形式。

2.1消息術語（terms）

協議參與者可能交換的消息稱為消息術語。 一個協議中所有參與者間可能交換的消息

集合稱為消息術語集A。術語可由原子術語經過級連和加密得到，原子術語可分為文本術語

和密鑰術語。

定義1 符號術語是一個有序對〈 ，t>,t∈A，為+或一，記作+t或-t，+t表示發出術語；-t表示接收到術語．(±A) ^*是符號術語的有限序列的集合．

定義2 術語a是術語b的子術語，即a b，如果下列條件成立：

(1)若b∈T,則要求b=a；

(2)若b∈K 則要求b=a；

(3)若b={g}_k 則要求a g或{g}_k=a；

(4)b=g·h，則要求ag或ah．

原子的消息術語分為兩種：一種是明文消息術語（比如參與者標識、隨機數等）；另一種為密鑰消息術語（包括對稱密鑰、非對稱密鑰等）。因此消息術語集A被劃分為明文消息

術語集T 和密鑰消息術語集K兩部分。

2．2 串（Strand）,串空間（Strand Space）和從（Bundle）

定義3 一個Strand Space是一個集合∑, 以及映射 ：tr: ∑ (±A)^* ．

(1)結點是一個有序對<s,i>，S∈∑,i滿足1≤i<length((tr(s)))．結點n=<s,i>屬于Strand ，表示為n∈s ．結點的集合記為N。

(2)如果n=<s,i>∈N，那么index(n)=i，strand(n)=s．如果(tr(s ))_i=<,a>,那么term(n)=+a(=+)或term(n)=-a(=-)；對于術語a，用node(+a)或node(-a)表示它所在的結點。

(3)n_l,n₂∈N，那么n₁n₂表示term(n₁)=+a，term(n₂)=-a。

(4)n_l,n₂∈N，那么n_l n₂表示n_l,n₂屬于同一個s,且index(n₂)=index(n₁)+1。

(5)術語t從結點n產生，當且僅當sign(n)=+；tterm (n)；而且對于同一個Strand上任何先于n的結點 ,tterm( )。

(6)術語t從結點n惟一產生，當且僅當惟一的結點n產生術語t。

所以，Strand空間構成一個有向圖(N，E)，N 是結點集合，邊E=(∪)。

定義4 CE是邊的集合，Nc N是由C中邊相連的結點集合。C是Bundle，如果：

(1)C是有限集．

(2)如果n_l∈Nc，且sign(n₁)=-，那么有惟一n₂，滿足n₂n_l∈Nc。

(3)如果n_l∈Nc，且有n₂n_l，那么n₂n_l∈Nc。

(4)C是無環的。

因為Bundle是串空間的一個子集,用來表示一個完整的協議，是一個圖，所以在邊和串下，結點的關系形成偏序關系，表示為 _c。C的任何非空結點子集，在 _c下都有最小元。

2．3 攻擊者模型

我們可以用一組Strand P來表示攻擊者模型：

(1)M[t].產生原子文本消息：<+t>,t∈T．

(2)F[g].接收消息：<-g>．

(3)T[g].接收并多次發送消息：<-g，+g，+g>．

(4)C[g,h].級連收到的消息：<-g,-h，+g·h>．

(5)S[g,h].分割收到的消息：<-g·h，+g，+h>．

(6)K[k].發送密鑰：<+ k>,k∈Key_P，Key_P=K_i∪k_p^-1∪K_px ．

(7)E[k,h].加密消息：<-h，+{h}_k >， k∈Key_P．

(8)D[k,h].解密消息：<-{h}_k +h>)，k^-1 ∈Key_p．          

其中，Key_p為攻擊者的密鑰集合，包括i的公鑰K_i 、他的私鑰K_p^-1 與x的共享密鑰K_px。

3 改進的Woo-Lam協議分析

Woo-Lam協議^[7]是基于對稱密鑰的認證協議^[8]，此協議是一個單向認證協議，只要求B認證A，不要求A認證B^[9]，所以對此協議進行了改進，使之成為雙向認證協議。

改進的Woo-Lam協議如下：

(1)AB:A,N_a

(2)BA:N_b,B

(3)AB:{N_b}K_AS

(4)BA:{N_a}K_BS

(5)BS:{A,{N_b}K_AS}K_BS

(6)AS:{B,{N_a}K_BS}K_AS

(7)SB:{N_b}K_BS

(8)SA:{N_a}K_AS

它的串空間模型：

（1）       集合Init[A,B,N_a,N_b]中的元素s∈∑且具有如下跡：

〈+A,-N_b,-B,+N_a,+{N_b}K_AS,-{N_a}K_BS,+{B,{N_a}K_BS}K_AS,+{N_a}K_AS〉

（2）       集合Resp[A,B,N_a,N_b]中的元素s∈∑且具有如下跡：

〈-A,+N_b,+B,-N_a,-{N_b}K_AS,+{N_a}K_BS,+{A,{N_b}K_AS}K_BS,-{N_b}K_BS〉

（3）       集合Serv[A,B,N_a,N_b]中的元素s∈∑且具有如下跡：

〈-{A,{N_b}K_AS}K_BS, -{B,{N_a}K_BS}K_AS,+{N_b}K_BS,+{N_a}K_AS〉

 圖1改進的 Woo-Lam協議的串空間模型圖

下面分別證明以下3個目標：

目標l：存在一個發起者strand t，它的消息序列為Init[x，y，N_a,N_b]．

證明：構造集合F={n︱(n∈C∧N_aterm(n)∧N_a≠term(n))∨ (n∈C∧N_bterm(n)∧N_b≠term(n))}，可以看出n₇∈F，所以F不空，根據串空間性質，F必有c最小元，設為m，sign(m)=+．下面，首先證明 m p,p∈P和ms．

（1）證明 mp，p∈P．分別討論p的每一個可能的消息序列：

M[t].tr(p)為<+t>,因為t∈T,所以如果N_at,那么N_a=t,所以mp。

F[g].tr(p)為<-g>，因為惟一的結點的sign(-g)=-,所以mp。

T[g].tr(p)為<-g，+g，+g>,因為sign(m)=+，所以若m=node(+g) ∈F， 這與m是最小元矛盾，所以m≠node(+g),也就是說mp

C[g,h].tr(p)為<-g,-h，+g·h>，因為合法的主體的可接受的消息中沒有級連類型，所以mp

S[g,h].tr(p)為<-g·h，+g，+h>，由于g和h的對稱性，假設m=node(+g)，那么node(-g·h) ∈F，這與m是最小元矛盾，所以mp．

K[k].tr(p)為：<+ k>,k∈Key_P，Key_P=K_i∪k_p^-1∪K_px,因為N_a k，所以mp。

E[k,h].tr(p)為：<-h，+{h}_k >， k∈Key_P，因為對稱密鑰K_ASkey_p,K_BSkeyp，所以{h}_k不被合法主體接受，mp。

D[k,h].tr(p)為：<-{h}_k,+h>)，k^-1 ∈Key_p，若m=node(+h)，那么N_ah，所以有N_a{h}_k,且N_a≠{h}_k;這樣，node(-{h}_k) ∈F,這與m是最小元矛盾，所以m≠node(+h)，也就是說mp。

（2）證明ms

由于服務器集合Serv[A,B,N_a,N_b]的跡為:

〈-{A,{N_b}K_AS}K_BS, -{B,{N_a}K_BS}K_AS,+{N_b}K_BS,+{N_a}K_AS〉，根據F的定義node(-{A,{N_b}K_AS}K_BS)，node(-{B,{N_a}K_BS}K_AS),node(+{N_b}K_BS),node(+{N_a}K_AS) ∈F。

由于node(-{A,{N_b}K_AS}K_BS)，node(+{N_b}K_BS)+{N_b}K_BS, node(-{B,{N_a}K_BS}K_AS)，node(+{N_a}K_AS) +{N_a}K_BS,所以m≠node(+{N_b}K_BS), m≠node(+{N_a}K_BS),又由于sign(-{A,{N_b}K_AS}K_BS)=-,sign(-{B,{N_a}K_BS}K_AS)=-,所以m≠node(-{A,{N_b}K_AS}K_BS), m≠node(-{B,{N_a}K_BS}K_AS),所以m s.

由于mp,p∈P和ms，而且m Resp，所以只有m∈Init，就說明了存在一個發起者Strand t，它的消息序列為Init[A,B,N_a,N_b]。

目標2：證明發起者的身份既可以是A也可以是B，即x=A或x=B

證明：A是根據協議執行完畢后，根據N_a是否一樣來認證對方是否為B，B也是根據N_b是否一樣來認證對方是否是A。構造集合R=(n︱term(n)= {N_a}K_AS∨{N_b}K_BS)，顯然n₇∈G,所以G不空，根據串空間性質，G必有 c最小元，設為m，sign(m)=+．

由于K_AS,K_BS是共享密鑰，所以m∈Init, m∈Resp或m∈Serv．則說明認證的主體可能是A，也可能是B，即x=A或x=B．

目標3：證明A,B都要進行身份認證，也即y=B或y=A.

證明：因為發起者既可以是A也可以是B，我們通過N_a或N_b來判斷認證主體是A或B。構造集合U＝{n︱term(n)=N_a ∨term(n)=N_b } ,若發起者是A，它的消息序列為〈+A,-N_b,-B,+N_a,+{N_b}K_AS,-{N_a}K_BS,+{B,{N_a}K_BS}K_AS,+{N_a}K_AS>，顯然-N_b，+N_a∈U，所以U不空；同理若發起者是B，也知U也不空，根據串空間性質，U必有 c最小元，設為m，sign(m)=+。m∈Init或 m∈Resp，即y=B，或y=A，也就是A,B都要進行身份認證。由此證明了是一個雙向認證協議。

4 改進前后的Woo-Lam協議的比較

為了說明改進后的協議的優勢，我們把改進后的Woo-Lam協議與原來的Woo-Lam協議進行比較，比較結果見表1。

表1改進前后的Woo-Lam協議的比較

從表1可看出雖然改進后的Woo-Lam協議消息條數和加密次數增多，但是改進后的協議，發起者可以是A，也可以 是B，并且要求B要認證A，也要求A認證B，是一雙向認證協議。原來的協議只要求B認證A，不要求A認證B，是單向協議。

5 結論

本文針對Woo-Lam協議中存在的問題，對其進行了改進，提出了一種新的Woo-Lam協議。并使用串空間模型對改進的協議進行了分析，證明其協議的正確性。首先建立協議的串空間模型，然后對協議進行證明，得出結論，通過列表比較可看出改進后的Woo-Lam協議的優越性，改進后的Woo-Lam協議成為了雙向認證協議。我們把基于串空間模型的方法用于包含第三方主體的認證協議。協議雖在保密性上做的還不完善，但使其協議從單向的認證協議成為了雙向認證協議。

在一下步的工作中，我們可以繼續在Woo-Lam協議的保密性上進行改進，使其更完善。

參考文獻(Reference)

[1] 束妮娜，王亞弟.密碼協議的形式化分析[J].計算機應用研究, 2001,18(07).113－117.

SHU Ni-na, WANG Ya-di. Formal Analysis of Cryptographic Protocols [J]. Application Research Of Computers, 2001,18(07).113－117.

[2] Thayer F，Herzog J C，Guttman J D. Strand space: why is a security protocol correct[C].In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. IEEE Computer Security press,1998(5):160-171

[3]Paul Syverson, Catherine Meadows. A Logical Language for Specifying Cryptographic Protocol Requirements[C], Proceeding of the 1993 IEEE Symposium on Research on Security and Privacy.IEEE Computer Society Press,1993.165-177.

[4]I.C Paulson. Proving Properties of Security Protocols by Induction[C].  Proceeding of the IEEE Computer Security Foundations Work shop X.IEEE computer Society,1997.70-83.

[5]鄧淼磊,邱罡,周利華.基于串空間和狀態的認證協議分析方法[J].計算機科學.2007,34(10).96-98

DENG Miao-Lei,QIU Gang,ZHOU Li-Hua. Analysis of Authentication Protocols Based on Strand Space and State Transition [J]. Computer Science. 2007,34(10).96-98

[6] Thayer，F．，Herzog，J．C．，Guttman，J．D．Strand space：Why is a security protocol correct? In：Proceedings of the 1998 IEEE.Symposium on Security and Privacy．1998,160-171

[7] Woo T Y C,Lam S S. Authentication for distributed systems[J]. Computer,1992,25(1):35-39

[8]李謝華,李建華,楊樹堂等.認證測試方法在安全協議分析中的應用[J].計算機工程. 2006,32(2).19-22.

LI Xie-hua,LI Jian-hua,YANG Shu-tang. Application of Authentication Test in Security Protocol Analysis [J]. Computer Engineering. 2006,32(2).19-22

[9]劉東喜,白英彩.基于Strand空間的認證協議證明方法研究[J].軟件學報,2002,13(07):1313-1316.

LIU Dong-xi, PAI Ying-cai. Study on Proof Method of Authentication Protocols Based on Strand Space [J]. Journal of Software, 2002,13(07):1313-1316.

作者簡介：

楊曉婕(1986-)，女，彝族，云南大理人，碩士研究生，主要研究方向為信息安全理論與技術。

繆祥華(1972-)，男，貴州盤縣人，副教授，博士，碩士生導師，主要研究方向為信息安全理論與技術。

仇細平(1983-)，女，湖南株洲人，碩士研究生，主要研究方向為信息安全理論與技術。

09093