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

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

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

?

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

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

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

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

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

1 引言

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

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

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

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

2 SPG-EFSM模型

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

定義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)識,P為參與者集合；認(rèn)證集二表示為C2={m→n|m∈P∩n∈P},m→n代表參與者n期望向參與者m認(rèn)證自己身份標(biāo)識；參與者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é)議達到了m認(rèn)證了n,記m?n.

(2)如果有(m?n)∩(n?m),則稱m與n達到了雙向認(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)機輸入集合；

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

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é)議的安全屬性需求,這里重點考慮認(rèn)證性.協(xié)議認(rèn)證是通過一個轉(zhuǎn)移過程t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉來驗證的,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時,未通過認(rèn)證,o=Failed.a(x,π(i),π(o))表示對消息的處理過程,如對加密消息進行解密、取消息中的某個元素.

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

定理1 SPG-EFSM是確定性的FSM,并且是一個可達圖.

證明 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 攻擊場景分類

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

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

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

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

該攻擊算法分四個部分:

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

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

③具體攻擊.根據(jù)當(dāng)前各狀態(tài)機的狀態(tài)進行有針對性的Intercept或Inject.先根據(jù)當(dāng)前各狀態(tài)機來推斷截獲或注入的狀態(tài)機集合MD,再根據(jù)MD選擇進行Intercept或Inject.如果選擇Intercept,就從MD中選取可以進行截取的Mk,然后進行Intercept,并更新Mk和Malice的狀態(tài)機MD.S,MM.S.如果選擇Inject,就從MD中選取可以進行注入的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ù),用來避免無限測試.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.2.2 μTESLA協(xié)議測試

μTESLA協(xié)議測試結(jié)果通過表4給出.攻擊者Malice在協(xié)議中干擾基站(Base Station)發(fā)給節(jié)點(Node)的消息,促使發(fā)給節(jié)點的消息延時一個時間間隔,也稱為“認(rèn)證漂移”.這個過程可等價于傳統(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é)果分析與評估

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

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

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

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

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

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

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

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

5 總結(jié)

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

[1]周彥偉,楊波,張文政.異構(gòu)無線網(wǎng)絡(luò)可控匿名漫游認(rèn)證協(xié)議[J].電子學(xué)報,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)模型下可公開驗證的匿名IBE方案[J].電子學(xué)報,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é)博士,主要研究方向為協(xié)議測試、漏洞挖掘.

E-mail:heyunhua610@163.com

楊 超 男,1979年出生,陜西西安人,西安電子科技大學(xué)副教授,主要研究方向為密碼學(xué)與網(wǎng)絡(luò)安全,云計算及移動智能計算安全.

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ǔ)研究計劃(No.2014JQ8295);中央高?；究蒲袠I(yè)務(wù)費(No.JB140303);國家自然科學(xué)基金面上基金(No.61672415)

TP309

A

0372-2112 (2016)11-2788-08

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

10.3969/j.issn.0372-2112.2016.11.031