肖躍雷， 朱志祥， 張 勇

(1. 西安郵電大學(xué) 物聯(lián)網(wǎng)與兩化融合研究院, 陜西 西安 710061；2. 陜西省信息化工程研究院, 陜西 西安 710075；3. 西北工業(yè)大學(xué) 計算機(jī)學(xué)院, 陜西 西安 710072)

一種分析和改進(jìn)安全協(xié)議的新方法

肖躍雷1,2,3， 朱志祥1,2， 張 勇1,2

(1. 西安郵電大學(xué) 物聯(lián)網(wǎng)與兩化融合研究院, 陜西 西安 710061；2. 陜西省信息化工程研究院, 陜西 西安 710075；3. 西北工業(yè)大學(xué) 計算機(jī)學(xué)院, 陜西 西安 710072)

分析安全協(xié)議的執(zhí)行過程，給出驅(qū)動模塊(Driving Module，DM)的定義，利用串空間模型構(gòu)建常規(guī)DM和攻擊DM，由此給出一種基于驅(qū)動模塊的模型檢驗方法。理論分析顯示，該方法搜索廣度和深度完善，能避免狀態(tài)空間爆炸問題，可用于獲得有缺陷安全協(xié)議的攻擊劇本，并證明無缺陷安全協(xié)議的安全性。用該方法分析Otway-Rees協(xié)議和TLS協(xié)議，獲得了Otway-Rees協(xié)議的攻擊劇本，得出了Otway-Rees協(xié)議的兩個安全改進(jìn)版本，說明了TLS協(xié)議的安全性。

驅(qū)動模塊；串空間模型；安全協(xié)議；模型檢驗；攻擊劇本

隨著計算機(jī)網(wǎng)絡(luò)的飛速發(fā)展和廣泛運用，網(wǎng)絡(luò)安全問題也日益引起人們的關(guān)注。安全協(xié)議提供安全服務(wù)，是保證網(wǎng)絡(luò)安全的基礎(chǔ)。自20世紀(jì)70年代末以來，安全協(xié)議的研究已經(jīng)成為一個熱點，有眾多的形式化研究方法涌現(xiàn)出來，具有代表性的就是著名的DOLEV-YAO模型[1]和BAN邏輯[2]。目前分析安全協(xié)議的形式化方法主要有[3]：(1)推理構(gòu)造法，一種基于知識與信念推理的模態(tài)邏輯方法，如BAN邏輯[2]；(2)攻擊構(gòu)造法，一種基于代數(shù)模型的狀態(tài)檢驗方法，如Murφ[4]、基于CSP的FDR[5]和基于時序邏輯的NRL[6]；(3)證明構(gòu)造法，一種基于不變集的代數(shù)定理證明方法，如Paulson方法[7]和串空間模型[8-14]。

攻擊構(gòu)造法可以直接看到一個安全協(xié)議的漏洞是如何被攻擊的，但通常無法證明安全協(xié)議是安全的，而且在規(guī)模較大的安全協(xié)議分析中通常無法避免狀態(tài)空間爆炸問題。要證明一個安全協(xié)議是安全的，必須依賴于證明構(gòu)造法。

本文擬引入驅(qū)動模塊(Driving Module，DM)的概念，結(jié)合模型檢驗方法和串空間模型給出一種分析和改進(jìn)安全協(xié)議的新方法，且使其同時具備攻擊構(gòu)造法和證明構(gòu)造法的特點。

1 分析與改進(jìn)安全協(xié)議的新方法

1.1 符號定義

為了分析安全協(xié)議，先對安全協(xié)議的消息符號進(jìn)行一般化定義。

Xi(i=1,2,…): 協(xié)議主體；

YXi:Xi產(chǎn)生的隨機(jī)數(shù)；

MXiXj：Xi和Xj的通信標(biāo)識符；

dXi： 表示Xi產(chǎn)生的用于DH(Diffie-Hellman)交換的臨時公鑰；

DHXiXj： 表示Xi和Xj的DH交換值，其值為[10]

DHXiXj=DH(dXi,dXj);

kXiXj： 表示Xi和Xj的會話密鑰;

KXiXj： 表示Xi和Xj的共享密鑰；

{h}K： 表示加密消息，其中h為被加密的消息，K為加密密鑰；

[h]K-1： 表示簽名消息，其中h為被加密的消息，K為加密密鑰；

*： 表示協(xié)議主體不能驗證的值，但其長度必須遵守協(xié)議的規(guī)定；

1.2 驅(qū)動模塊

安全協(xié)議是協(xié)議主體之間進(jìn)行的一些事件序列。安全協(xié)議執(zhí)行過程中協(xié)議主體行為主要為發(fā)送消息和接收消息。任何一個安全協(xié)議都有始發(fā)點和終止點，始發(fā)點發(fā)送消息驅(qū)動協(xié)議的進(jìn)行，終止點接收消息而結(jié)束整個協(xié)議執(zhí)行過程。對于安全協(xié)議執(zhí)行過程的中間部分，協(xié)議主體接收消息之后必然發(fā)送新的消息給其他協(xié)議主體，這顯然構(gòu)成了一個消息驅(qū)動過程。

定義1 協(xié)議主體X接收消息或不接收消息而發(fā)送新的消息給其他協(xié)議主體的協(xié)議執(zhí)行過程為一個驅(qū)動模塊(DM)，X稱為DM的主體。

對于一個安全協(xié)議而言，該協(xié)議的合法參與者稱為常規(guī)協(xié)議主體，而非法參與者便稱為攻擊協(xié)議主體。若DM的主體為常規(guī)協(xié)議主體，則該DM為常規(guī)DM；若DM的主體為攻擊協(xié)議主體，則該DM為攻擊DM。

1.2.1 常規(guī)DM構(gòu)建

由于常規(guī)DM的主體為常規(guī)協(xié)議主體，而常規(guī)協(xié)議主體的協(xié)議執(zhí)行過程必須遵守正常協(xié)議的執(zhí)行規(guī)則，所以常規(guī)DM可以根據(jù)文獻(xiàn)[8]中常規(guī)者串得到。例如，NSPK協(xié)議[15]中發(fā)起者A的常規(guī)者串為〈+{NaA}Kb，-{NaNb}Ka，+{Nb}Kb〉，從中可構(gòu)建出兩個常規(guī)DM

〈+{YX1X1}〉KX2,

其中+表示發(fā)送消息，-表示接收消息。

1.2.2 攻擊DM構(gòu)建

攻擊DM的主體為攻擊協(xié)議主體，而攻擊協(xié)議主體的協(xié)議執(zhí)行過程是對協(xié)議執(zhí)行的各種攻擊行為，所以攻擊DM可以根據(jù)文獻(xiàn)[8,10]中的攻擊者跡得到。攻擊者的能力主要由兩方面因素來描述：一是攻擊者獲得它可掌握的消息；二是攻擊者由它所能掌握的消息產(chǎn)生新消息的能力。由攻擊者跡[8,10]得到攻擊DM。

DM1(發(fā)送文本項)：〈+t〉;

DM2(發(fā)送隨機(jī)數(shù))：〈+r〉;

DM3(發(fā)送密鑰項)：〈+K〉;

DM4(級聯(lián)各組件消息)：〈-h1，-h2，-…，+h〉;

DM5(分割為組件消息)：〈-h，+h1，+h2，+…〉;

DM6(加密消息)：〈-K，-h，+{h}K〉;

DM7(解密消息)：〈-{h}K，-K-1，+h〉;

DM8(簽名消息)：〈-K-1，-h，+[h]K-1〉;

DM9(對消息執(zhí)行Hash)：〈-h，+Hash(h)〉;

DM10(發(fā)送臨時公鑰)：〈+d〉;

DM11(發(fā)送DH交換值)：〈-d1，-d2，+DH(d1，d2) 〉。

以上各DM中,h1和h2為組件，h為消息，K為加密密鑰，K-1為解密密鑰。組件是指不可分割的消息[9]。

1.3 安全目標(biāo)

以NSPK協(xié)議為例，NSPK協(xié)議的安全目標(biāo)是以常規(guī)DM序列表示的NSPK協(xié)議(協(xié)議終止點也表示為DM形式)，具體描述為

〈+{NaA}Kb〉→〈-{NaA}Kb，+{NaNb}Ka〉→〈-{NaNb}Ka，+{Nb}Kb〉→〈-{Nb}Kb〉,

其中，第1個常規(guī)DM稱為始發(fā)常規(guī)DM，第2和3個常規(guī)DM稱為過程常規(guī)DM，第4個常規(guī)DM稱為終止常規(guī)DM。

1.4 模型檢驗算法

由DM的定義可知，任何安全協(xié)議的協(xié)議過程都可以描述成一系列DM過程。不管是正常協(xié)議還是攻擊協(xié)議(通常稱為攻擊劇本)，都可以用以上定義的DM描述出來。為了得到這些攻擊劇本，基于DM對安全協(xié)議執(zhí)行自底向上的模型檢驗，其過程是依據(jù)DM中的消息進(jìn)行的。模型檢驗的機(jī)理如圖1所示，其中m1、m2、m、r1、r2、s1、s2為消息項，①表示父結(jié)點DM的接收消息都由常規(guī)DM發(fā)送，②表示父結(jié)點DM的接收消息都由攻擊DM發(fā)送，③表示父結(jié)點DM的接收消息由常規(guī)DM和攻擊DM共同發(fā)送。

圖1 模型檢驗機(jī)理

按照模型檢驗的機(jī)理，對安全協(xié)議的終止常規(guī)DM執(zhí)行模型檢驗可形成不同的DM結(jié)點路徑。這些DM結(jié)點路徑包括正常協(xié)議的DM結(jié)點路徑和攻擊協(xié)議的DM結(jié)點路徑(攻擊劇本的過程)。由于每一條DM結(jié)點路徑都是依據(jù)消息進(jìn)行模型檢驗的，所以自然形成一條消息模型檢驗路徑。

模型檢驗算法的具體過程是，先取安全協(xié)議的終止常規(guī)DM為根結(jié)點，依據(jù)根結(jié)點DM中接收消息的格式分別搜索常規(guī)DM集和攻擊DM集，并按模型檢驗機(jī)理生成各個子結(jié)點，再以可得到的各子結(jié)點為父結(jié)點再作類似的搜索，直至生成的子結(jié)點數(shù)為零。其中，搜索過程必須滿足的搜索條件包括

(1) 協(xié)議的假設(shè)條件;

(2) DM的約束條件;

(3) 搜索攻擊DM中的DM5或DM7時，要保證它們的接收消息在分割消息集和解密消息集中;

(4) 同一條消息模型檢驗路徑上不能出現(xiàn)兩個相同的消息。

分割消息集是指各常規(guī)DM的發(fā)送消息經(jīng)過直接分割或分割和解密組合的間接分割過程可獲得到消息集。解密消息集是指各常規(guī)DM的發(fā)送消息經(jīng)過直接解密或分割和解密組合的間接解密過程可獲得到消息集。

C語言實現(xiàn)的模型檢驗算法的主要部分如下。

Model_Checking(S0)

{S=S0; //S為DM結(jié)點隊列;S0為初始DM結(jié)點隊列,值為安全目標(biāo)的最后一個接收消息為接收者所驗證的DM.

while(S!=NULL) //S隊列非空.

{ dm_node=get_head(S); //取S隊列的頭結(jié)點.

S1=get_next_dmnode(dm_node); //生成下一層DM結(jié)點,S1為下一層DM結(jié)點的隊列.

S=Add_dmlist(S1); //將下一層DM結(jié)點加入S隊列.

}

}

get_net_dmnode(dm_node)

{count=0; //創(chuàng)建DM結(jié)點樹和DM搜索樹的標(biāo)記點.

dms=get_dm(dm_node); //獲取DM的并以隊列表示.

while(dms!=NULL) //DM隊列非空.

{dm=get_head(dms); //取dms隊列的頭結(jié)點.

if(count==0) create_dmtree(); //創(chuàng)建DM搜索樹.

if(search_condition==true)

next_dms=product_next_dms(dm); //若符合搜索條件,則生成下一層DM.

Add_dmtree(next_dms); //將下一層DM增加到DM搜索樹上.

}

if(count==0) create_dmnodetree(); //創(chuàng)建DM結(jié)點樹.

if(search_condition==true)

next_dmnodes =product_next_dmnodes(next_dms); //若符合搜索條件,則生成下一層DM結(jié)點.

Add_dmnodetree(next_dmnodes); //將下一層DM結(jié)點增加到DM結(jié)點樹上.

count=count+1; //將標(biāo)記點的值加1.

return next_dmnodes; //返回下一層結(jié)點.

}

1.5 分析與討論

對于一個存在諸多攻擊漏洞的安全協(xié)議來說，好的模型檢驗方法能檢測出很多的攻擊漏洞,這一性能與模型檢驗方法的搜索深度和廣度有著密切的關(guān)系。若搜索深度和廣度都是完善的，則安全協(xié)議的所有攻擊漏洞都能被檢測出來?？梢宰C明，分析和改進(jìn)安全協(xié)議的新方法不僅具有完善的搜索深度和廣度，而且可以避免狀態(tài)空間爆炸問題。

根據(jù)模型檢驗機(jī)理可知，任一個DM的搜索都是基于常規(guī)DM集和攻擊DM集的，而常規(guī)DM集和攻擊DM集分別代表所分析安全協(xié)議的常規(guī)者能力和攻擊者能力。搜索條件(1)和(2)是協(xié)議規(guī)則的約束條件，所以它們是合理的搜索條件。搜索條件(3)是攻擊者從常規(guī)者所發(fā)送消息中獲取和構(gòu)造消息的約束條件，收斂于搜索條件(1)和(2)，所以它是合理的搜索條件。搜索條件(4)是用于避免DM搜索過程死循環(huán)的約束條件，所以它也是合理的搜索條件。因此，新方法的搜索深度和廣度都是完善的。

新方法是基于DM的搜索，其中每個DM相當(dāng)于一個狀態(tài)。要證明該方法可以避免狀態(tài)空間爆炸問題，就是證明DM的單級搜索狀態(tài)數(shù)量和搜索路徑的長度都是有限的。對于一個DM而言，其后繼DM是常規(guī)DM和攻擊DM。當(dāng)后繼DM是常規(guī)DM時，由于常規(guī)DM是依據(jù)安全協(xié)議過程而產(chǎn)生的，且收斂于搜索條件(1)和(2)，所以該DM的單級搜索狀態(tài)數(shù)量和搜索路徑的長度都是有限的。

攻擊DM1、DM2、DM3和DM10代表攻擊者自己產(chǎn)生消息的能力，而其他攻擊DM代表攻擊者依據(jù)常規(guī)DM的發(fā)送消息構(gòu)造消息的能力。若后繼DM是攻擊DM1、DM2、DM3和DM10，則生成相應(yīng)攻擊DM后結(jié)束搜索過程。若后續(xù)DM是攻擊DM5和DM7，則通過分析可知，它們收斂于搜索條件(1)和(2)。若后續(xù)DM是攻擊DM4、DM6、DM8、DM9和DM11，則生成相應(yīng)的攻擊DM，但最終收斂于搜索條件(1)、(2)和(3)。此外，搜索條件(4)避免了DM搜索過程的死循環(huán)。也就是說，對于一個DM而言，當(dāng)后繼DM是攻擊DM時，該DM的單級搜索狀態(tài)數(shù)量和搜索路徑的長度都是有限的。因此，該方法可以避免狀態(tài)空間爆炸問題。

2 應(yīng)用實例

2.1 Otway-Rees協(xié)議的分析

Otway-Rees協(xié)議[16]的規(guī)范描述為

A→B：MAB{NaMAB}Kas，

B→S：MAB{NaMAB}Kas{NbMAB}Kbs，

S→B：M{Nakab}Kas{NbMAB}，

B→A：M{Nakab}Kas，

其安全目標(biāo)描述為

〈+MAB{NaMAB}Kas〉→〈-MAB{NaMAB}Kas，+MAB{NaMAB}Kas{NbMAB}Kbs〉→〈-MAB{NaMAB}Kas{NbMAB}Kbs，+M{Nakab}Kas{Nbkab}Kbs〉→〈-M{Nakab}Kas{Nbkab}Kbs，+M{Nakab}Kas〉→〈-M{Nakab}Kas〉

按常規(guī)DM定義，若以P表示攻擊者，則Otway-Rees協(xié)議的常規(guī)DM可描述如下。

(1)

(2)

(3)

(4)

Otway-Rees協(xié)議的假設(shè)條件如下。

(1)Kas，Kbs?KP。

(2) 服務(wù)器S對協(xié)議主體X1和X2之間時間間隔很短的兩次會話密鑰申請不進(jìn)行限制，而其他協(xié)議主體對時間間隔很短的兩次相同通信申請進(jìn)行限制。

利用C語言實現(xiàn)的模型檢驗算法，對Otway-Rees協(xié)議進(jìn)行了模型檢驗，共可得到了14條DM結(jié)點路徑，其中 8種為無并發(fā)過程冗余、具有真正攻擊意義的攻擊劇本。若令

Ya=Na,Yb=Nb,Mab=M,

則這8種攻擊劇本可描述如下。

(1)α.1A→B:MAB{NaMAB}Kas,

α.2B→S:MAB{NaMAB}Kas{NbMAB}Kbs,

α.3.1S→P(B):M{Nakab}Kas{Nbkab}Kbs,

β.2P(B)→S:MAB{NaMAB}Kas{NbMAB}Kbs,

α.4B→A:M{Nakab}Kas。

(2)α.1A→B:MAB{NaMAB}Kas,

α.2B→S:MAB{NaMAB}Kas{NbMAB}Kbs,

α.3.1S→P(B):M{Nakab}Kas{NbMAB}Kbs,

β.2P(B)→S:MAB{NaMAB}Kas{NbMAB}Kbs,

(3)α.1A→B:MAB{NaMAB}Kas,

α.2.1B→P(S):MAB{NaMAB}Kas{NbMAB}Kbs,

α.2.2P(B)→S:MAB{NaMAB}Kas{NbMAB}Kbs,

α.3.1S→P(B):M{Nakab}Kas{Nbkab}Kbs,

α.3.2P(S)→B:M{Nakab}Kas{NbMAB}Kbs,

α.4B→A:M{Nakab}Kas。

(4)α.1.1A→P(B):MAB{NaMAB}Kas,

α.1.2P(A)→B:MAB{NaMAB}Kas,

α.2B→S:MAB{NaMAB}Kas{NbMAB}Kbs,

α.3.1S→P(B):M{Nakab}Kas{Nbkab}Kbs,

α.3.2P(S)→B:M{NaMAB}Kas{Nbkab}Kbs,

α.4B→A:M{NaMAB}Kas。

(6)α.1P(A)→B:MpAB*p,

α.2B→P(S):MpAB*p{NbMpAB}Kbs,

α.3P(S)→B:Mp*p{NbMpAB}Kbs,

α.4B→P(A):Mp*p。

(7)α.1A→B:MAB{NaMAB}Kas,

α.2B→P(S):MAB{NaMAB}Kas{NbMAB}Kbs,

α.3P(S)→B:M{NaMAB}Kas{NbMAB}Kbs,

α.4B→A:M{NaMAB}Kas。

(8)α.1A→P(B):MAB{NaMAB}Kas,

α.4P(S)→A:M{NaMAB}Kas。

分析Otway-Rees協(xié)議所得的攻擊劇本包含目前國內(nèi)外對該協(xié)議的所有攻擊劇本[8,17]，可證實新方法有效。

2.2 Otway-Rees協(xié)議的改進(jìn)

從攻擊劇本可以獲知：(1)響應(yīng)者B對發(fā)起者A發(fā)送消息的新鮮性無法考究；(2)響應(yīng)者B和發(fā)起者A接收認(rèn)證服務(wù)器S產(chǎn)生的消息時，都存在類型缺陷攻擊的問題；(3) 因認(rèn)證服務(wù)器S以組件的形式發(fā)送產(chǎn)生的消息，這給并發(fā)攻擊創(chuàng)造了條件；(4)認(rèn)證服務(wù)器S用通信標(biāo)識符M的匹配來確定接收消息的一致性，這樣可以確定響應(yīng)者B產(chǎn)生的消息部分必須是新鮮的。

利用常規(guī)DM模式以逆向的方法對Otway-Rees協(xié)議進(jìn)行改進(jìn)，并保證逆向消息傳遞的唯一可達(dá)性，可得出兩種Otway-Rees協(xié)議的改進(jìn)版，它們的規(guī)范描述分別如下。

(1)A→B:MAB{MABNaTa}Kas,

B→S:MAB{MABNaTa}Kas{MABNb}Kbs,

S→B:M{Nbkab{Nakab}Kas}Kns,

B→A:M{Nakab}Kas。

(2)A→B:MAB{MABNa}Kas,

B→A:MAB{MABNa}Kas{MABNb}Kbs,

A→S:MAB{MABNa{MABNb}Kbs}Kas,

S→A:M{Nakab{Nbkab}Kbs}Kas,

A→B:M{Nbkab}Kbs。

上式中Ta表示A產(chǎn)生的時戳。改進(jìn)版(1)是利用發(fā)起者A的時戳來標(biāo)識發(fā)送消息的新鮮性，而改進(jìn)版(2)則是利用增加一次握手來保證發(fā)起者A發(fā)送消息的新鮮性。雖然改進(jìn)版(1)在通信效率上優(yōu)于改進(jìn)版(2)，但是改進(jìn)版(1)需要建立時間同步機(jī)制，所以改進(jìn)版(1)僅適用于已建立時間同步機(jī)制的應(yīng)用場景，而改進(jìn)版(2)沒有這樣的限制。可以驗證，這兩種Otway-Rees協(xié)議的改進(jìn)版都是安全的。

2.3 TLS協(xié)議的分析

TLS協(xié)議簡化版[10]的規(guī)范描述為

A→B：A，

B→A：{T2AB}kab,

其中g(shù)x為B產(chǎn)生的臨時公鑰，gy為A產(chǎn)生的臨時公鑰，kab=Hash(gxy)。

TLS協(xié)議簡化版的安全目標(biāo)描述為

根據(jù)常規(guī)DM定義，若以P表示攻擊者，則TLS協(xié)議簡化版的常規(guī)DM描述為

(1)

〈+X1〉(X1=A或B，X2=A或B或P，X1≠X2)。

(2)

(3)

(4)

TLS協(xié)議簡化版的假設(shè)條件為

(2)協(xié)議主體X1和X2對時間間隔很短的兩次相同通信申請進(jìn)行限制。

利用C語言實現(xiàn)的模型檢驗算法，對TLS協(xié)議簡化版進(jìn)行了模型檢驗，結(jié)果僅得到1條DM結(jié)點路徑，即TLS協(xié)議簡化版的安全目標(biāo)，因此，TLS協(xié)議是安全的，與文獻(xiàn)[10]的串空間模型證明結(jié)果是一致的。

3 結(jié)語

通過分析安全協(xié)議的執(zhí)行過程，引入驅(qū)動模塊(DM)的概念，基于串空間模型構(gòu)建常規(guī)DM和攻擊DM，得出一種基于DM的模型檢驗方法。該方法的搜索廣度和深度都是完善的，而且可以避免狀態(tài)空間爆炸問題，這使得它不僅可以用于搜索有缺陷安全協(xié)議的攻擊劇本，而且可用于證明無缺陷安全協(xié)議的安全性。利用該方法對Otway-Rees協(xié)議進(jìn)行分析，獲得了它的攻擊劇本并提出了Otway-Rees協(xié)議的兩個安全改進(jìn)版本，以及通過對TLS協(xié)議簡化版的分析，證明了TLS協(xié)議是安全的。

[1] Dolev D, Yao A. On the security of public key protocols[J]. IEEE Transactions on Information Theory,1983, 29(2): 198-208.

[2] Burrows M, Abadi M, Needham R. A logic of authentication[J]. ACM Transactions on Computer System, 1990, 8(1): 18-36.

[3] 慕建君. 一種形式化分析安全協(xié)議的新模型[J]. 西安電子科技大學(xué)學(xué)報,2006,33(3):381-385.

[4] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Murφ[C]// Proceedings of the 1997 IEEE Symposium on Security and Privacy. USA: IEEE Computer Society Press, 1997:141-151.

[5] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR Tools and Algorithms for the Construction and Analysis of Systems[C]// Volume 1055 of Lecture Notes in Computer Science. Beilin: Springer Verlag, 1996:147-166.

[6] Meadows C. The NRL Protocol Analyzer: an overview[J]. Journal of Logic Programming, 1996, 26(2): 113-131.

[7] Paulson L C. Proving Properties of Security Protocols by Induction[C]//Proceedings of the IEEE Computer Security Foundations Workshop X. New York: IEEE Computer Society Press, 1997: 70-83.

[8] Thayer Fábrega F J, Herzog J C, Guttman J D. Strand Spaces: Why Is a Security Protocol Correct[C]//Proceedings of the 1998 IEEE Symposium on Security and Privacy. New York: IEEE Computer Press, 1998:160-171.

[9] Guttman J D, Thayer F J. Authentication tests[C]//Proceedings of the 2000 IEEE Symposium on Security and Privacy. USA: IEEE Computer Society Press, 2000:150-164.

[10] Herzog J C. The Diffie-Hellman key-agreement scheme in the strand space model[C]//Proc of the 16th IEEE Computer Security Foundations Workshop. Pacific Grove: IEEE Computer Society, 2003:234-247.

[11] 董學(xué)文,馬建峰,牛文生,等. 基于串空間的Ad Hoc安全路由協(xié)議攻擊分析模型[J]. 軟件學(xué)報，2011，22(7)：1641-1651.

[12] 泰彬彬,王俊芳. 基于串空間認(rèn)證測試的DTLS協(xié)議認(rèn)證性分析[J]. 計算機(jī)與網(wǎng)絡(luò)，2014，40(496)：51-55.

[13] 吳名歡,程小輝. Casper/FDR和串空間在物聯(lián)網(wǎng)通信協(xié)議中的形式化分析[J]. 桂林理工大學(xué)學(xué)報，2014，34(2)：338-344.

[14] Xiao Yuelei, Wang Yumin, Pang Liaojun. A Verification of trusted network access protocols in the strand space model[J]. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, 2012, E95-A(3)：665-668.

[15] Needham R. Schroeder M. Using encryption for authentication in large networks of computers[J]. Communications of the ACM, 1978, 21(12): 993-999.

[16] Otway D, Rees O. Efficient and timely mutual authentication[J]. ACM Operating Systems Review, 1987, 21(1):8-10.

[17] 王貴林,卿斯?jié)h,周展飛. 認(rèn)證協(xié)議的一些新攻擊方法[J].軟件學(xué)報,2001,12(6):907-913.

[責(zé)任編輯:瑞金]

《西安郵電大學(xué)學(xué)報》版權(quán)聲明

為適應(yīng)我國信息化建設(shè)的需要，擴(kuò)大刊物影響，拓寬信息交流渠道，本刊已加入“中國知網(wǎng)CNKI系列期刊數(shù)據(jù)庫”、“中國核心期刊(遴選)數(shù)據(jù)庫”(萬方數(shù)據(jù)——數(shù)字化期刊群)、“中國期刊網(wǎng)”等數(shù)據(jù)庫。本刊已許可以上數(shù)據(jù)庫以數(shù)字化方式復(fù)制、匯編、發(fā)行、信息網(wǎng)絡(luò)傳播本刊所載文章的全文信息。稿件一經(jīng)刊登，將在本刊稿酬中一次性支付著作權(quán)使用報酬(包括印刷版、光盤版和網(wǎng)絡(luò)版等各種使用方式的報酬)。作者向本刊提交文章的行為即視為同意我刊上述聲明。

西安郵電大學(xué)學(xué)報編輯部

A new method for analyzing and improving security protocols

XIAO Yuelei1,2,3, ZHU Zhixiang1,2, ZHANG Yong1,2

(1. Institute of IOT and IT-based Industrialization, Xi’an University of Post and Telecommunications, Xi’an 710061, China;2. Shaanxi Provincial Information Engineering Research Institute, Xi’an 710075, China;3. College of Computer Science and Engineering, Northwestern Polytechnical University, Xi’an 710072, China)

By analyzing the process of security protocols, the definition of driving module (DM) is introduced, and then regular and penetrator DMs are formed according to the Strand Space Model (SSM). Based on this, a DM-based model checking method is proposed. Theoretical analysis indicates that this method is prefect in terms of searching breadth and depth, and can avoid the state space explosion problem. Therefore, this method can be used not only to get the attack scenarios of a flawed security protocol, but also to prove that an unflawed security protocol is secure. Moreover, the Otway-Rees protocol and the TLS protocol are analyzed based on this method. As a result, various attack scenarios of the Otway-Rees protocol are discovered and two secure improved Otway-Rees protocols are put forward, and therefore the TLS protocol is proved to be secure.

driving module, strand space model, security protocols, model checking, attack scenarios

2015-04-17

國家自然科學(xué)基金資助項目(61402367)；陜西省信息化技術(shù)研究計劃資助項目(2013-008)；西安郵電大學(xué)青年教師科研基金資助項目(401-1201)

肖躍雷(1979-),男,博士,講師，從事信息安全研究。E-mail:xiao_yuelei@163.com 朱志祥(1959-),男,博士,教授,從事多媒體通信、信息化應(yīng)用及網(wǎng)絡(luò)安全研究。E-mail:zhuzhix369@163.com

10.13682/j.issn.2095-6533.2015.05.003

TP393.08

A

2095-6533(2015)05-0017-07