何云華,楊 超,張俊偉,馬建峰

(1.西安電子科技大學(xué)計(jì)算機(jī)網(wǎng)絡(luò)與信息安全教育部重點(diǎn)實(shí)驗(yàn)室,陜西西安 710071; 2.北方工業(yè)大學(xué)計(jì)算機(jī)學(xué)院信息安全系，北京 100029)

?

協(xié)議認(rèn)證性安全屬性測(cè)試方法

何云華1,2,楊 超1,張俊偉1,馬建峰1

(1.西安電子科技大學(xué)計(jì)算機(jī)網(wǎng)絡(luò)與信息安全教育部重點(diǎn)實(shí)驗(yàn)室,陜西西安 710071; 2.北方工業(yè)大學(xué)計(jì)算機(jī)學(xué)院信息安全系，北京 100029)

認(rèn)證性建立通信雙方的信任關(guān)系,是安全通信的重要保障.傳統(tǒng)的協(xié)議測(cè)試方法只關(guān)注協(xié)議功能的正確性,無法滿足認(rèn)證性等安全屬性測(cè)試的要求.因此,提出了一種針對(duì)協(xié)議認(rèn)證性的安全屬性測(cè)試方法,利用帶目標(biāo)集合的有限狀態(tài)機(jī)模型SPG-EFSM來擴(kuò)展描述協(xié)議安全屬性,并在攻擊場景分類的基礎(chǔ)上設(shè)計(jì)了認(rèn)證攻擊算法.通過攻擊算法找到了Woo-lam協(xié)議和μTESLA協(xié)議的認(rèn)證性漏洞,該方法具有可行性、覆蓋率高等特點(diǎn).

協(xié)議測(cè)試；安全屬性；認(rèn)證性測(cè)試；形式化模型；攻擊分類

1 引言

通信協(xié)議作為網(wǎng)絡(luò)和分布式應(yīng)用的基礎(chǔ)[1],其固有的復(fù)雜性和潛在的敵對(duì)環(huán)境,使得協(xié)議的安全性面臨巨大的挑戰(zhàn).大量基于邏輯推理的方法被用來分析、驗(yàn)證通信協(xié)議的安全性[2,3],如認(rèn)證性、保密性、不可否認(rèn)性和完整性等安全屬性.但是,這些方法大多集中在協(xié)議規(guī)范分析與驗(yàn)證方面,忽略了另一個(gè)不可信、不安全因素——協(xié)議實(shí)現(xiàn)引入的漏洞[4].

最常見的協(xié)議實(shí)現(xiàn)安全漏洞測(cè)試方法是隨機(jī)測(cè)試[5](Random testing),通過注入大量隨機(jī)、異?；蝈e(cuò)誤的輸入到待測(cè)協(xié)議中來觀察系統(tǒng)是否會(huì)出現(xiàn)異常,但其測(cè)試數(shù)據(jù)的生成缺乏準(zhǔn)確、高效的指導(dǎo),測(cè)試數(shù)據(jù)的分布不受控制[6].針對(duì)該問題,描述協(xié)議數(shù)據(jù)流的測(cè)試方法逐步受到了關(guān)注,使用上下文無關(guān)文法(BNF)[7]或結(jié)構(gòu)化的Frame語法[8]描述消息字段之間的相關(guān)性.但是,此類方法不支持有狀態(tài)轉(zhuǎn)移的協(xié)議控制流的建模.數(shù)據(jù)流與控制流相結(jié)合的測(cè)試方法成為了進(jìn)一步的研究熱點(diǎn).Jing C等人[9]對(duì)TTCN-3控制流描述模型進(jìn)行了語法和語義擴(kuò)展,但所描述的語法變異類型有限.Yamaguchi等人[10]將抽象語法樹(AST)和控制流圖(CFG)相結(jié)合,在實(shí)際測(cè)試中也獲得了較好的效果.但為了滿足特定的安全需求,例如認(rèn)證性或機(jī)密性,通信協(xié)議往往對(duì)協(xié)議消息本身進(jìn)行了加密等處理,存在大量不可知參數(shù),這使得上述測(cè)試方法,很難識(shí)別消息的各個(gè)字段,構(gòu)造出合適的測(cè)試?yán)?因此,設(shè)計(jì)專用的協(xié)議安全屬性測(cè)試方法是迫切需求的.

但是,此類研究才剛剛起步.Mashtizadeh等人[11]提出密碼-控制流模型,該模型假定攻擊者能產(chǎn)生消息認(rèn)證碼用于控制流測(cè)試.該方法側(cè)重于控制協(xié)議狀態(tài)的跳轉(zhuǎn)和返回,未考慮協(xié)議消息構(gòu)造方法.Shu G等人[12]提出了以協(xié)議消息作為其輸入/輸出參數(shù)的協(xié)議描述模型,該模型利用密鑰K、隨機(jī)數(shù)N等參數(shù)組成的元組來表示消息,并建立了用于表示攻擊者行為及協(xié)議安全屬性的攻擊者模型.該方法對(duì)加密消息具有一定處理能力,但其攻擊者模型不能準(zhǔn)確的表示協(xié)議某些特定的安全屬性.例如協(xié)議認(rèn)證性,必須要結(jié)合參與者初始認(rèn)證目標(biāo)與協(xié)議執(zhí)行完后狀態(tài)才能準(zhǔn)確的描述.另外,該方法沒有考慮某些特殊情形,包括一次會(huì)話有多個(gè)參與者、一個(gè)參與者參與多個(gè)會(huì)話、擁有合法身份的攻擊者參與會(huì)話等情形.

針對(duì)以上問題,本文提出了協(xié)議認(rèn)證性安全屬性測(cè)試方法.首先提出一種描述協(xié)議安全屬性的有限狀態(tài)機(jī)擴(kuò)展模型SPG-EFSM(Symbolic Parameterized Goal-Extended Finite State Machine),擴(kuò)展定義參與方目標(biāo)集,用條件判斷函數(shù)來對(duì)比目標(biāo)集合與協(xié)議執(zhí)行后的結(jié)果,以實(shí)現(xiàn)安全屬性的驗(yàn)證；在此基礎(chǔ)上,對(duì)協(xié)議攻擊場景進(jìn)行了分類,該分類綜合考慮了擁有合法身份的攻擊者參與,存在認(rèn)證中心的多方參與,參與者參與多個(gè)會(huì)話等情況；然后,結(jié)合了Dolev-Yao攻擊模型[13],設(shè)計(jì)了協(xié)議認(rèn)證性攻擊算法,該算法包涵了上述所有的分類；最后,通過對(duì)廣泛應(yīng)用的Woo-lam協(xié)議[14]和μTESLA協(xié)議[15]進(jìn)行了測(cè)試,發(fā)現(xiàn)存在于Woo-lam協(xié)議及其各種更新版本中的已知和未知安全漏洞,以及μTESLA協(xié)議的認(rèn)證漂移問題.

2 SPG-EFSM模型

SPG-EFSM是一種包含安全屬性定義和驗(yàn)證的協(xié)議描述模型,是Shu G提出的EFSM擴(kuò)展模型[12]的改進(jìn).SPG-EFSM擴(kuò)展描述了協(xié)議目標(biāo)集合,基于目標(biāo)集合定義安全屬性,通過對(duì)比目標(biāo)集合與協(xié)議執(zhí)行后的結(jié)果來指示協(xié)議的安全屬性是否存在漏洞,該驗(yàn)證規(guī)則由條件判斷函數(shù)來實(shí)現(xiàn).認(rèn)證性是協(xié)議安全屬性的重要部分,本文著重對(duì)認(rèn)證性安全屬性測(cè)試.

定義1、定義2給出了認(rèn)證目標(biāo)集、單向認(rèn)證和雙向認(rèn)證的概念；SPG-EFSM模型的描述由定義3給出.

定義1 認(rèn)證集一表示為C1={→m|m∈P},→m代表期望認(rèn)證參與者m身份標(biāo)識(shí),P為參與者集合；認(rèn)證集二表示為C2={m→n|m∈P∩n∈P},m→n代表參與者n期望向參與者m認(rèn)證自己身份標(biāo)識(shí)；參與者n目標(biāo)集合表示為:

gn={c|((?c=→m)∈C1∩m≠n)∪

((?c=m→n′)∈C2∩n=n′);m,n,n′∈P}

(1)

認(rèn)證結(jié)果集定義為R={Succeed,Failed}.

定義2 已知m,n,m′,n′∈P,→n′∈gm,m′→n∈gn.

(1)如果有(m=m′)∩(n=n′),并且協(xié)議能正確執(zhí)行完成,則稱協(xié)議達(dá)到了m認(rèn)證了n,記m?n.

(2)如果有(m?n)∩(n?m),則稱m與n達(dá)到了雙向認(rèn)證,記m?n.

定義3 SPG-EFSM由七元組組成〈S,A,G,I,O,X,T〉.

其中S——狀態(tài)集合；

A——原子集合{Key,Nonce,Int}和相應(yīng)派生規(guī)則{E(),H(),MAC(),·},用于描述消息,如E(kT,kab·H(na))；

G——目標(biāo)集合G={gn|n∈P}；

I——輸入集合I=I′∪G,其中I′是原有狀態(tài)機(jī)輸入集合；

O——輸出集合O=O′∪R,其中O′是原有狀態(tài)機(jī)輸出集合；

X——L(A)參數(shù)構(gòu)成的有限集合,具有默認(rèn)初值,其中L(A)代表由A構(gòu)成的消息集合；

T——轉(zhuǎn)移過程集合,t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉∈T,其中s,s′分別代表初態(tài)、終態(tài),π(i),π(o)分別代表輸入、輸出的參數(shù),p(x,π(i))是增加了定義2給出認(rèn)證關(guān)系的條件判斷函數(shù),a(x,π(i),π(o))是關(guān)于變量、輸入?yún)?shù)和輸出參數(shù)的處理過程.

其中,協(xié)議的目標(biāo)集合用于協(xié)議的安全屬性需求,這里重點(diǎn)考慮認(rèn)證性.協(xié)議認(rèn)證是通過一個(gè)轉(zhuǎn)移過程t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉來驗(yàn)證的,s,s′分別是未認(rèn)證態(tài)、認(rèn)證態(tài),輸入i為G,輸出o為R,條件判斷函數(shù)p(x,π(i))是定義2給出了的認(rèn)證關(guān)系.當(dāng)p(x,π(i))=0時(shí),未通過認(rèn)證,o=Failed.a(x,π(i),π(o))表示對(duì)消息的處理過程,如對(duì)加密消息進(jìn)行解密、取消息中的某個(gè)元素.

為了確保測(cè)試有效地實(shí)施,協(xié)議測(cè)試要求狀態(tài)機(jī)模型是確定的可達(dá)圖[12].定理1證明了SPG-EFSM模型是一個(gè)確定的可達(dá)圖.

定理1 SPG-EFSM是確定性的FSM,并且是一個(gè)可達(dá)圖.

證明 SPG-EFSM可表示為FSM(SG,IG,OR,fnext,foutput)的形式.

其中狀態(tài)集合:

SG={|(s∈S)∩(V?X)∩(gm∈G)}

(2)

輸入/輸出集合:

IG=G∪L(A),OR=R∪L(A)

(3)

狀態(tài)轉(zhuǎn)移函數(shù):

fnext:SG×IG→SG,fnext( ,i) =

ttakesmachinefrom

(4)

輸出函數(shù):

foutput:SG×IG→OR,foutput(,i)

={o∈OR|?t∈T,

toutputsORfromuponi}

(5)

3 協(xié)議認(rèn)證攻擊算法

3.1 攻擊場景分類

為了有效地實(shí)施攻擊,本節(jié)對(duì)攻擊場景進(jìn)行了分類.一方面,攻擊場景分類可以快速的建立攻擊策略,另一方面,攻擊分類建立在Dolev-Yao強(qiáng)攻擊模型[13]基礎(chǔ)上,能夠最大化攻擊者的能力.本節(jié)從是否存在多個(gè)參與者、是否利用接收者預(yù)言機(jī)服務(wù)[16]、是否擁有合法身份的攻擊者等三個(gè)方面對(duì)攻擊場景進(jìn)行分類,具體定義如下:

本文用(L-ID,Depend,T)表示攻擊情形,其中L-ID為攻擊者的合法身份,L-ID=1(L-ID=0)為擁有(無)合法身份；Depend為接收者的預(yù)言機(jī)服務(wù),Depend=1(Depend=0)為利用(不利用)接收者預(yù)言機(jī)服務(wù)；T為認(rèn)證中心,T=1(T=0)為存在(不存在)認(rèn)證中心.

定義4 設(shè)A,B為參與者,U為用戶集,LU為合法用戶集,M為攻擊者,Attack為M進(jìn)行的一次攻擊,則Attack可以分為以下八類:

①當(dāng)(L-CD,Depend,T)=(0,0,0)時(shí),存在Attack1,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A?gB)∩(→M("A")∈gM),不存在T,協(xié)議執(zhí)行完畢,使得A?M("B")或A?B.

②當(dāng)(L-CD,Depend,T)=(0,0,1)時(shí),存在Attack2,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A?gB)∩(→M("B")∈gM),存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或A?B.

③當(dāng)(L-CD,Depend,T)=(1,0,0)時(shí),存在Attack3,即:

若M∈U,A,B∈LU,(B→A∈gA)∩ (→A?gB)∩(→M("B")∈gM),不存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或A?B.

④當(dāng)(L-CD,Depend,T)=(1,0,1)時(shí),存在Attack4,即:

若M∈U,A,B∈LU,(B→A∈gA)∩ (→A?gB)∩(→M("B")∈gM),存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或A?B.

⑤當(dāng)(L-CD,Depend,T)=(0,1,0)時(shí),存在Attack5,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),不存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或無法完成A?B.

⑥當(dāng)(L-CD,Depend,T)=(0,1,1)時(shí),存在Attack6,即:

若M∈U-LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或無法完成A?B.

⑦當(dāng)(L-CD,Depend,T)=(1,1,0)時(shí),存在Attack7,即:

若M∈LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),不存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或無法完成A?B.

⑧當(dāng)(L-CD,Depend,T)=(1,1,1)時(shí),存在Attack8,即:

若M∈LU,A,B∈LU,(B→A∈gA)∩ (→A∈gB)∩(→M("B")∈gM),存在T,如果協(xié)議執(zhí)行完畢,使得A?M("B")或無法完成A?B.

3.2 攻擊算法

根據(jù)定義4,提出了一種通用的攻擊算法.該算法是基于主動(dòng)測(cè)試的思想,攻擊者M(jìn)alice可以任意截獲和注入消息,攻擊者知識(shí)集合Ω隨攻擊過程的進(jìn)行而增大.針對(duì)某一個(gè)具體的協(xié)議而言,并不是所有Attack都可選擇,要根據(jù)協(xié)議規(guī)范{M1,M2,…,MC}來進(jìn)行選擇適合Attack.根據(jù)Attack來選取參與者的狀態(tài)機(jī)Mi.例如,雙方認(rèn)證協(xié)議規(guī)范為{M1,M2},M1,M2分別代表發(fā)起者、響應(yīng)者的狀態(tài)機(jī),當(dāng)實(shí)施Attack1時(shí),參與者Alice選擇M1,Malice選擇M2.當(dāng)涉及到多個(gè)session,參與者Alice可能選擇多個(gè)狀態(tài)機(jī),用MAi來表示參與者Alice選擇第i個(gè)狀態(tài)機(jī).算法通過狀態(tài)機(jī)的推斷,轉(zhuǎn)移過程、消息的選擇,剔除了不合理的測(cè)試分支,提高了算法的效率.

該攻擊算法分四個(gè)部分:

①選擇狀態(tài)機(jī).先由協(xié)議規(guī)范{M1,…,MC}確定適當(dāng)?shù)腁ttack,再根據(jù)Attack來確定用戶U的MU、攻擊者的MM.

②更新目標(biāo)集合.目標(biāo)集合G的更新包括用戶gU的更新和攻擊者gM的更新,由用戶U和Malice選取的狀態(tài)機(jī)在協(xié)議中的角色來確定.

③具體攻擊.根據(jù)當(dāng)前各狀態(tài)機(jī)的狀態(tài)進(jìn)行有針對(duì)性的Intercept或Inject.先根據(jù)當(dāng)前各狀態(tài)機(jī)來推斷截獲或注入的狀態(tài)機(jī)集合MD,再根據(jù)MD選擇進(jìn)行Intercept或Inject.如果選擇Intercept,就從MD中選取可以進(jìn)行截取的Mk,然后進(jìn)行Intercept,并更新Mk和Malice的狀態(tài)機(jī)MD.S,MM.S.如果選擇Inject,就從MD中選取可以進(jìn)行注入的Mk,求得Mk中注入的轉(zhuǎn)移過程Tture,并用lookahead(Ω,Mk.S,X,t)選擇可以能產(chǎn)生有效輸出的消息,然后更新狀態(tài)Mk.S,MM.S.

④攻擊判斷.如果找到認(rèn)證性的漏洞,算法結(jié)束；如果沒有找到漏洞,再重復(fù)步驟1到步驟4,當(dāng)嘗試超過最大值Max,算法結(jié)束.Max是按需設(shè)定的嘗試次數(shù),用來避免無限測(cè)試.

該算法涵蓋定義4給出的八種攻擊類型.如果該算法可以處理攻擊者以合法或非法身份參與,是否利用接收者預(yù)言機(jī)服務(wù),是否存在認(rèn)證中心等情況,那么該算法涵蓋這八種攻擊類型.該算法通過目標(biāo)集合來表示攻擊擁有合法或非法身份的情況.例如,Malice以合法身份與Alice進(jìn)行通信可表示為:gM={B→M},gB={→M}；Malice以非法身份偽裝Alice與Bob進(jìn)行通信可表示為:gM={B→M("A")},gB={→A}.該算法通過參與者選取多個(gè)狀態(tài)機(jī)來表示參與者在不同session中的角色.例如,當(dāng)Malice截獲到Alice發(fā)給Bob的消息msg時(shí),發(fā)現(xiàn)自己不能閱讀,便偽裝Alice發(fā)msg給Bob以獲得預(yù)言機(jī)服務(wù),這可表示為:gM={A→M("B"),B→M("A")},gA={→B},gB={→A}；當(dāng)Malice沒有利用Bob預(yù)言機(jī)服務(wù)可表示為:gM={A→M("B")},gA={→B}.該算法通過選取{M1,…,MC}中C的取值來表示是否存在認(rèn)證中心的情況,即多方參與的情況.因此,該算法涵蓋了這八種攻擊類型.

4 協(xié)議的測(cè)試與結(jié)果分析

4.1 Woo-lam協(xié)議描述與測(cè)試

Woo-lam協(xié)議是經(jīng)典的認(rèn)證協(xié)議.在此協(xié)議中假定Alice和Trent共享對(duì)稱密鑰KAT,Bob和Trent共享對(duì)稱密鑰KBT,協(xié)議的最終目標(biāo)是Alice向Bob證實(shí)自己的身份.Woo-lam協(xié)議的主要交互過程請(qǐng)參見文獻(xiàn)[14].

4.1.1 Woo-lam協(xié)議規(guī)范描述

SPG-EFSM模型描述Woo-lam協(xié)議的協(xié)議規(guī)范如圖1所示.假定攻擊者M(jìn)alice可以截獲每一條消息,知道Alice、Bob、Trent從協(xié)議開始到結(jié)束的每一個(gè)狀態(tài)S,其中S0表示初始狀態(tài),SRi表示接受第i條消息,SSi表示發(fā)送第i條消息,SA表示認(rèn)證狀態(tài).

4.1.2 Woo-lam協(xié)議測(cè)試

Woo-lam協(xié)議測(cè)試結(jié)果通過表1給出.攻擊者M(jìn)alice在協(xié)議中偽裝了Alice與Bob進(jìn)行會(huì)話,Malice以合法身份與Bob進(jìn)行會(huì)話,Malice維護(hù)偽裝Alice的狀態(tài)機(jī)和合法身份會(huì)話的狀態(tài)機(jī).由于存在兩次會(huì)話,所以Malice、Bob、Trent分別都存在著兩個(gè)狀態(tài)機(jī).從表1可以看出,攻擊算法發(fā)現(xiàn)了Woo-lam協(xié)議存在Attack4,是典型攻擊[16]中的平行會(huì)話攻擊.

表1 檢測(cè)到Woo-lam協(xié)議的認(rèn)證錯(cuò)誤

Woo-lam協(xié)議存在Attack4的一個(gè)修改方案是在3.Alice→Bob:E(KAT,NB)加入Alice的身份信息,但這種方案也存在攻擊,由表2給出.攻擊者M(jìn)alice在協(xié)議中偽裝了Alice、Trent與Bob進(jìn)行會(huì)話,Malice維護(hù)偽裝Alice、Trent的狀態(tài)機(jī),來指導(dǎo)攻擊進(jìn)行.從表2可以看出,攻擊算法發(fā)現(xiàn)了Woo-lam協(xié)議存在Attack2,是典型攻擊[16]中的反射攻擊.

表2 檢測(cè)到修改后的Woo-lam協(xié)議的認(rèn)證錯(cuò)誤

Woo-lam協(xié)議的另一個(gè)更新方案是把第4個(gè)交互流程改為4.Bob→Trent:E(KBT,Alice·NB·E(KAT,NB)),但這種方案也存在攻擊,由表3給出.Bob與擁有合法身份的Malice進(jìn)行會(huì)話時(shí),Malice在協(xié)議中偽裝了Alice、Trent與Bob進(jìn)行會(huì)話,Malice維護(hù)偽裝Alice、Trent的狀態(tài)機(jī)以及合法身份會(huì)話的狀態(tài)機(jī).從表3可以看出,攻擊算法發(fā)現(xiàn)了Woo-lam協(xié)議存在Attack4,是典型攻擊[16]中的交錯(cuò)攻擊.

表3 檢測(cè)到Woo-lam協(xié)議另一更新方案的認(rèn)證錯(cuò)誤

4.2 μTESLA協(xié)議描述與測(cè)試

μTESLA協(xié)議是無線傳感器網(wǎng)絡(luò)中經(jīng)典的廣播認(rèn)證協(xié)議[15],其運(yùn)行過程包括安全初始化、節(jié)點(diǎn)加入、數(shù)據(jù)包認(rèn)證等階段,詳細(xì)請(qǐng)參見文獻(xiàn)[15].

4.2.1 μTESLA協(xié)議規(guī)范描述

SPG-EFSM模型描述μTESLA協(xié)議規(guī)范如圖2所示.基站(B)的狀態(tài)機(jī)MB位于圖2(a)中,先后經(jīng)歷了初始化、接收加入節(jié)點(diǎn)請(qǐng)求、給加入節(jié)點(diǎn)分發(fā)相關(guān)參數(shù)、數(shù)據(jù)包發(fā)送等過程.節(jié)點(diǎn)(N)的狀態(tài)機(jī)MN位于2(b)中,它有五種狀態(tài):初始狀態(tài)、請(qǐng)求加入、接收系統(tǒng)參數(shù)、接收基站數(shù)據(jù)包、認(rèn)證基站數(shù)據(jù)包.其中S0、SRi、SSi的定義與4.1.1節(jié)相同,pid和sid分別代表了節(jié)點(diǎn)和基站的身份標(biāo)識(shí),Pj表示基站發(fā)送的第j個(gè)數(shù)據(jù)包.

4.2.2 μTESLA協(xié)議測(cè)試

μTESLA協(xié)議測(cè)試結(jié)果通過表4給出.攻擊者M(jìn)alice在協(xié)議中干擾基站(Base Station)發(fā)給節(jié)點(diǎn)(Node)的消息,促使發(fā)給節(jié)點(diǎn)的消息延時(shí)一個(gè)時(shí)間間隔,也稱為“認(rèn)證漂移”.這個(gè)過程可等價(jià)于傳統(tǒng)有線網(wǎng)絡(luò)的攔截和轉(zhuǎn)發(fā)過程,因此可將此過程表述為:Malice偽裝Node接收Base Station的消息,Malice偽裝Base Station發(fā)送消息給Node.從表4可以看出,攻擊算法發(fā)現(xiàn)了μTESLA協(xié)議存在Attack5.

4.3 結(jié)果分析與評(píng)估

(1)SPG-EFSM的描述能力分析.

從圖1、圖2中可以看出,SPG-EFSM模型可以清晰直觀地描述Woo-lam協(xié)議參與者狀態(tài)機(jī)(MA、MB、MT)和μTESLA協(xié)議參與者狀態(tài)機(jī)(MB、MN).協(xié)議運(yùn)行時(shí)各參與者之間的認(rèn)證關(guān)系也能被SPG-EFSM模型清晰、準(zhǔn)確表現(xiàn)出來.例如在表1中,第二行的gB說明了Bob在本次測(cè)試過程中將與Alice建立認(rèn)證關(guān)系,從第三行的gB可以看出Bob又試圖與Malice建立認(rèn)證關(guān)系,倒數(shù)第二行中給出的A?B表明了協(xié)議執(zhí)行完后,達(dá)到了Bob認(rèn)證Alice狀態(tài).

表4 μTESLA協(xié)議的認(rèn)證錯(cuò)誤

表5 本文攻擊算法與其他方法性能比較

(2)攻擊算法的性能分析.

令Max=n,協(xié)議輪數(shù)為m,則該算法的時(shí)間復(fù)雜度為O(nm),等同于Guoqiang Shu提出算法的時(shí)間復(fù)雜度.然而,該攻擊算法能夠表示擁有合法身份的攻擊者參與、多個(gè)會(huì)話和多方參與等特殊情況.與其他方法相比,攻擊算法在覆蓋率方面也有較大的優(yōu)勢(shì),能夠以較少的時(shí)間復(fù)雜度達(dá)到較高覆蓋率,如表5所示.

(3)測(cè)試方案的新型漏洞探測(cè)能力分析.

該測(cè)試方案發(fā)現(xiàn)了Woo-lam協(xié)議及其更新協(xié)議當(dāng)中的漏洞,包括平行會(huì)話攻擊,反射攻擊,交錯(cuò)攻擊等典型攻擊.測(cè)試還發(fā)現(xiàn)了μTESLA協(xié)議的典型漏洞——認(rèn)證漂移問題和DoS攻擊.從Attack2、Attack4中發(fā)現(xiàn)Woo-lam協(xié)議的安全性依賴于參與者的合法身份標(biāo)識(shí),也即認(rèn)證中心與參與者之間的對(duì)稱密鑰,但這并不可靠.例如,在Attack4中Malice利用Trent的預(yù)言機(jī)服務(wù),獲得了對(duì)Alice的合法身份標(biāo)識(shí),成功欺騙Bob認(rèn)證了Alice,而Alice認(rèn)為他與Bob達(dá)到了認(rèn)證關(guān)系.

5 總結(jié)

針對(duì)協(xié)議安全性測(cè)試缺乏對(duì)安全屬性描述及其相關(guān)測(cè)試方法的問題,本文提出了一種用于檢測(cè)協(xié)議認(rèn)證安全屬性的測(cè)試方法.首先建立SPG-EFSM模型,擴(kuò)展描述目標(biāo)集合,通過結(jié)合參與者目標(biāo)與協(xié)議執(zhí)行后狀態(tài)進(jìn)一步描述認(rèn)證安全屬性.然后,基于SPG-EFSM模型將協(xié)議攻擊場景分類,以攻擊者擁有合法身份、多方參與、多個(gè)會(huì)話等特殊情況；在此基礎(chǔ)上,結(jié)合了Dolev-Yao攻擊模型,設(shè)計(jì)了一種包含上述分類的協(xié)議認(rèn)證性攻擊算法.通過對(duì)Woo-lam協(xié)議和μTESLA協(xié)議認(rèn)證性的測(cè)試發(fā)現(xiàn),本方法具有可行性、覆蓋率高等特點(diǎn).

[1]周彥偉,楊波,張文政.異構(gòu)無線網(wǎng)絡(luò)可控匿名漫游認(rèn)證協(xié)議[J].電子學(xué)報(bào),2016,44(5):1117-1123.

ZHOU Yan-wei,YANG Bo,ZHANG Wen-zheng.Controllable and anonymous roaming protocol for heterogeneous wireless network[J].Acta Electronica Sinica,2016,44(5):1117-1123.(in Chinese)

[2]Dalal Alrajeh,Jeff Kramer,Alessandra Russo,et al.Elaborating requirements using model checking and inductive learning [J].IEEE Transactions on Software Engineering,2013,39(3):361-383.

[3]李順東,楊坤偉,鞏林明,等.標(biāo)準(zhǔn)模型下可公開驗(yàn)證的匿名IBE方案[J].電子學(xué)報(bào),2016,44(3):673-678.

LI Shun-dong,YANG Kun-wei,GONG Lin-ming,et al.A publicly verifiable anonymous IBE scheme in the standard model[J].Acta Electronica Sinica,2016,44(3):673-678.(in Chinese)

[4]Wen Tang,Sui Ai-Fen,Wolfgang Schmid.A model guided security vulnerability discovery approach for network protocol implementation[A].Proceedings of the 13th International Conference on Communication Technology[C].Beijing,China:IEEE,2011.675-680.

[5]Andrea Arcuri,Muhammad Zohaib Iqbal,Lionel Briand.Random testing:theoretical results and practical implications[J].IEEE Transactions on Software Engineering,2012,38(2):258-277.

[6]G Fraser,A Arcuri.Whole test suite generation[J].IEEE Transactions on Software Engineering,2013,39(2):276-291.

[7]Oulu University Secure Programming Group.PROTOS:Security Testing of Protocol Implementation [OL].http://www.ee.oulu.fi/research/ouspg/protos/index.html,2012-06-12.

[8]Tal O,Knight S,Dean T.Syntax-based vulnerability testing of frame-based network protocols[A]. Proceedings of the 21nd Conference on Privacy,Security and Trust[C].Fredericton:IEEE,2004.13-15.

[9]Jing C,Wang Z,Yin X,et al.Mutation testing of protocol messages based on extended TTCN-3[A].Proceedings of the 22nd International Conference on Advanced Information Networking and Applications[C].Okinawa:IEEE,2008.667-674.

[10]Fabian Yamaguchi,Nico Golde,Daniel Arp,et al.Modeling and discovering vulnerabilities with code property graphs[A].Proceedings of IEEE Symposium on Security and Privacy[C].San Jose:IEEE,2014.590-604.

[11]Gali Mashtizadeh,Andrea Bittau,Dan Boneh,et al.CCFI:cryptographically enforced control flow integrity [A].Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security[C].New York:ACM,2015.941-951.

[12]Shu G,Lee G.Formal methods and tools for testing communication protocol system security[D].Ohio,USA:Ohio State University,2008.

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

[14]Woo T,Lam S.Authentication for distributed systems[J].ACM Transactions on Computer Systems,1992,25(1):35-39.

[15]Perrig A,Szewczyk R,et al.SPINS:Security protocols for sensor networks [J].Wireless Networks,2002,8(5):521-534.

[16]Wenbo Mao.Modern Cryptography:Theory and Practice[M].New Jersey,USA:Prentice Hall,2004.

何云華 男,1987年出生,湖北荊門人,北方工業(yè)大學(xué)講師，西安電子科技大學(xué)博士,主要研究方向?yàn)閰f(xié)議測(cè)試、漏洞挖掘.

E-mail:heyunhua610@163.com

楊 超 男,1979年出生,陜西西安人,西安電子科技大學(xué)副教授,主要研究方向?yàn)槊艽a學(xué)與網(wǎng)絡(luò)安全,云計(jì)算及移動(dòng)智能計(jì)算安全.

E-mail:chaoyang@mail.xidian.edu.cn

Authentication Testing of Security Protocols—A Method for Testing Protocol Security Properties

HE Yun-hua1，2,YANG Chao1,ZHANG Jun-wei1,MA Jian-feng1

(1.KeyLaboratoryofComputerNetworkandInformationSecurityofMinistryofEducation,XidianUniversity,Xi’an,Shaanxi710071,China； 2.DepartmentofInformationSecurity,CollegeofComputerScience,NorthChinaUniversityofTechnology,Beijing100029,China)

Authentication builds the trust relationship between communication parties,which is a magnitude guarantee for secure communications.However,existing protocol testing techniques focus on validating the protocol specification.Those techniques can not satisfy the requirements of testing protocol authentication as their lack of the method for describing security properties.Therefore,a protocol security property testing method is proposed for testing protocol authentication.This testing method uses a new formal model-Symbolic Parameterized Goal Extended Finite State Machine (SPG-EFSM) for describing protocols and their security properties.Then,a protocol attack algorithm is designed for testing protocol authentication based on different attack scenarios.Through test experiments on the well-known protocol Woo-lam and μTESLA,it is found that the SPG-EFSM based attack algorithm can find several protocol security flaws and has better feasibility and high coverage.

protocol testing；security properties；authentication testing；formal model；attack classification

2015-10-27；

2016-05-19；責(zé)任編輯：李勇鋒

國家自然科學(xué)基金青年基金(No.61303219);陜西省自然科學(xué)基礎(chǔ)研究計(jì)劃(No.2014JQ8295);中央高?；究蒲袠I(yè)務(wù)費(fèi)(No.JB140303);國家自然科學(xué)基金面上基金(No.61672415)

TP309

A

0372-2112 (2016)11-2788-08

??學(xué)報(bào)URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.11.031