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

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

?

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

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

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

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

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

1 引言

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

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

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

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

2 SPG-EFSM模型

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

定義1、定義2給出了認證目標集、單向認證和雙向認證的概念；SPG-EFSM模型的描述由定義3給出.

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

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

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

(1)

認證結果集定義為R={Succeed,Failed}.

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

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

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

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

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

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

G——目標集合G={gn|n∈P}；

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

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

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

T——轉移過程集合,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給出認證關系的條件判斷函數(shù),a(x,π(i),π(o))是關于變量、輸入?yún)?shù)和輸出參數(shù)的處理過程.

其中,協(xié)議的目標集合用于協(xié)議的安全屬性需求,這里重點考慮認證性.協(xié)議認證是通過一個轉移過程t=〈s,s′,i,o,p(x,π(i)),a(x,π(i),π(o))〉來驗證的,s,s′分別是未認證態(tài)、認證態(tài),輸入i為G,輸出o為R,條件判斷函數(shù)p(x,π(i))是定義2給出了的認證關系.當p(x,π(i))=0時,未通過認證,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)轉移函數(shù):

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

ttakesmachinefrom

(4)

輸出函數(shù):

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

={o∈OR|?t∈T,

toutputsORfromuponi}

(5)

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

3.1 攻擊場景分類

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

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

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

①當(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.

②當(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.

③當(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.

④當(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.

⑤當(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.

⑥當(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.

⑦當(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.

⑧當(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.例如,雙方認證協(xié)議規(guī)范為{M1,M2},M1,M2分別代表發(fā)起者、響應者的狀態(tài)機,當實施Attack1時,參與者Alice選擇M1,Malice選擇M2.當涉及到多個session,參與者Alice可能選擇多個狀態(tài)機,用MAi來表示參與者Alice選擇第i個狀態(tài)機.算法通過狀態(tài)機的推斷,轉移過程、消息的選擇,剔除了不合理的測試分支,提高了算法的效率.

該攻擊算法分四個部分:

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

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

③具體攻擊.根據(jù)當前各狀態(tài)機的狀態(tài)進行有針對性的Intercept或Inject.先根據(jù)當前各狀態(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中注入的轉移過程Tture,并用lookahead(Ω,Mk.S,X,t)選擇可以能產(chǎn)生有效輸出的消息,然后更新狀態(tài)Mk.S,MM.S.

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

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

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

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

Woo-lam協(xié)議是經(jīng)典的認證協(xié)議.在此協(xié)議中假定Alice和Trent共享對稱密鑰KAT,Bob和Trent共享對稱密鑰KBT,協(xié)議的最終目標是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é)議開始到結束的每一個狀態(tài)S,其中S0表示初始狀態(tài),SRi表示接受第i條消息,SSi表示發(fā)送第i條消息,SA表示認證狀態(tài).

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

Woo-lam協(xié)議測試結果通過表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é)議的認證錯誤

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

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

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é)議另一更新方案的認證錯誤

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

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

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

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

4.2.2 μTESLA協(xié)議測試

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

4.3 結果分析與評估

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

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

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

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

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

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

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

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

5 總結

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

[1]周彥偉,楊波,張文政.異構無線網(wǎng)絡可控匿名漫游認證協(xié)議[J].電子學報,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]李順東,楊坤偉,鞏林明,等.標準模型下可公開驗證的匿名IBE方案[J].電子學報,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è)大學講師，西安電子科技大學博士,主要研究方向為協(xié)議測試、漏洞挖掘.

E-mail:heyunhua610@163.com

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

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；責任編輯：李勇鋒

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

TP309

A

0372-2112 (2016)11-2788-08

??學報URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.11.031