基于模型檢測(cè)的無(wú)線體域網(wǎng)安全協(xié)議形式化驗(yàn)證

基于模型檢測(cè)的無(wú)線體域網(wǎng)安全協(xié)議形式化驗(yàn)證

陳鐵明，虞震波，王婷，方趙林

(浙江工業(yè)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，浙江 杭州 310023)

摘要：在研究無(wú)線體域網(wǎng)(WBAN)安全屬性的基礎(chǔ)上，為了對(duì)無(wú)線體域網(wǎng)安全協(xié)議進(jìn)行安全分析，保證協(xié)議設(shè)計(jì)之初的安全性，提出并實(shí)現(xiàn)了一種基于模型檢測(cè)的無(wú)線體域網(wǎng)安全協(xié)議形式化分析和驗(yàn)證方法.基于模型檢測(cè)工具PAT研究建模語(yǔ)言CSP#及其擴(kuò)展方法，提出一種支持網(wǎng)絡(luò)節(jié)點(diǎn)可移動(dòng)的抽象建模數(shù)據(jù)結(jié)構(gòu)，便于對(duì)WBAN協(xié)議的形式化建模；根據(jù)Dolev-Yao模型，結(jié)合WBAN節(jié)點(diǎn)位置的可移動(dòng)性，建立攻擊者抽象模型.以Chitra等提出的基于雙天線的WBAN安全協(xié)議為例，在PAT工具中應(yīng)用筆者提出的方法對(duì)其進(jìn)行建模并加以分析驗(yàn)證，體現(xiàn)了方法的實(shí)用性. 2) CU與待認(rèn)證傳感器節(jié)點(diǎn)的建模如下：

關(guān)鍵詞：無(wú)線體域網(wǎng)；模型檢測(cè)；安全協(xié)議；PAT；CSP#；線性時(shí)序邏輯

收稿日期：2015-04-17

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目(61103044)

作者簡(jiǎn)介：陳鐵明(1978—)，男，浙江諸暨人，副教授，博士，研究方向?yàn)榫W(wǎng)絡(luò)信息安全，E-mail:tmchen@zjut.edu.cn.

中圖分類號(hào)：TP309.7

文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：1006-4303(2015)05-0497-06

Abstract:Based on the research of wireless body area network (WBAN) security attributes, a formal analysis and verification method for WBAN security protocols is proposed and implemented in this paper. The method can ensure the security of WBAN protocols in the early stage of protocol design. First, the modeling language CSP# which is supported by the model checker PAT is extended with an abstract modeling data structure supporting the node mobility, which could simplify the modeling of WBAN protocols. Then, an abstract attacker model is established through the combination of Dolev-Yao model and WBAN node mobility. Finally, the WBAN security protocol proposed by Chitra et al. is modeled and verified using our method embedded in PAT, which reflects the usability and efficiency of this method.

Keywords:wireless body area networks; model checking; security protocols; PAT; CSP#; linear temporal logic

Formal verification of wireless body area network security

protocols based on model checking

CHEN Tieming, YU Zhenbo, WANG Ting, FANG Zhaolin

(College of Computer Science and Technology, Zhejiang University of Technology, Hangzhou 310023, China)

隨著無(wú)線通信技術(shù)和無(wú)線傳感技術(shù)的不斷發(fā)展，無(wú)線傳感器網(wǎng)絡(luò)的研究和應(yīng)用獲得了巨大成功[1-4].無(wú)線體域網(wǎng)(Wireless body area network, WBAN)是無(wú)線傳感網(wǎng)在智能定位、醫(yī)學(xué)領(lǐng)域的分支，主要應(yīng)用于人體區(qū)域,負(fù)責(zé)采集人體機(jī)能數(shù)據(jù)以供醫(yī)療分析[5].安全協(xié)議作為構(gòu)成無(wú)線傳感網(wǎng)絡(luò)的關(guān)鍵部分，其數(shù)據(jù)的安全性、認(rèn)證的可靠性是制約WBAN正常通信的最重要因素.自從Dolev和Yao提出將模型檢測(cè)技術(shù)應(yīng)用于安全協(xié)議分析和驗(yàn)證[6]，模型檢測(cè)技術(shù)以其簡(jiǎn)潔明了的建模過(guò)程和高度自動(dòng)化的分析驗(yàn)證成為了當(dāng)前主流的形式化分析技術(shù)[7].Aladdin等通過(guò)時(shí)序Petri網(wǎng)對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行建模，確保了協(xié)議的正確可靠[8].Kashif等使用SPIN模型[9]檢測(cè)工具對(duì)WSN路由協(xié)議進(jìn)行形式化分析，發(fā)現(xiàn)了攻擊漏洞[10].Lowe利用進(jìn)程代數(shù)使用CSP(Communicating sequential process)方法[11]對(duì)NSPK協(xié)議進(jìn)行了形式化分析，發(fā)現(xiàn)了一個(gè)十幾年來(lái)未知的攻擊.2015年Wang等使用模型檢測(cè)技術(shù)對(duì)WBAN的MAC層安全協(xié)議做了形式化分析[12].然而目前對(duì)WBAN安全協(xié)議的形式化分析工作仍比較少，因此對(duì)WBAN安全協(xié)議進(jìn)行形式化分析驗(yàn)證的重要性不言而喻.

上述方法均采用某種形式化建模語(yǔ)言實(shí)現(xiàn)對(duì)安全協(xié)議的形式化描述，進(jìn)而被相應(yīng)支持該形式化語(yǔ)言的工具接受并實(shí)現(xiàn)自動(dòng)化模型檢測(cè)過(guò)程.雖然模型檢測(cè)工具的自動(dòng)化驗(yàn)證程度高，分析過(guò)程嚴(yán)謹(jǐn)，但是系統(tǒng)建模的過(guò)程仍比較復(fù)雜，需要具有專業(yè)知識(shí)經(jīng)驗(yàn)的人工支持，建模過(guò)程的好壞直接影響到驗(yàn)證結(jié)果的正確性.因此面向不同應(yīng)用領(lǐng)域定制開(kāi)發(fā)專用的建模語(yǔ)言也是一種發(fā)展趨勢(shì).利用新型模型檢測(cè)工具PAT(Process analysis toolkit)框架[13]的高度可擴(kuò)展性，提出一個(gè)基于數(shù)據(jù)結(jié)構(gòu)的CSP#語(yǔ)言擴(kuò)展模塊，提高WBAN安全協(xié)議的形式化建模和分析效率，實(shí)現(xiàn)了一種面向WBAN位置相關(guān)安全協(xié)議的專用建模與驗(yàn)證方法.

1PAT模型檢測(cè)工具

PAT是由新加坡國(guó)立大學(xué)PAT研究小組自主開(kāi)發(fā)的一套模型檢測(cè)工具，支持并發(fā)、實(shí)時(shí)系統(tǒng)、UML狀態(tài)機(jī)等系統(tǒng)的建模驗(yàn)證，能夠?qū)SP#，RTS，LTS等多種語(yǔ)言進(jìn)行模擬驗(yàn)證和反例生成.

PAT是一個(gè)可擴(kuò)展、模塊化的通用架構(gòu)，其系統(tǒng)框架[14]如圖1所示，整個(gè)框架分為4層，這種分層架構(gòu)方便了模塊的擴(kuò)展，并將建模驗(yàn)證過(guò)程分為3步：編譯、抽象和驗(yàn)證.從圖1中可以看出：最上層的建模層(Modeling layer)，包含了多個(gè)不同領(lǐng)域、不同目標(biāo)系統(tǒng)的建模模塊，可以使用某種建模語(yǔ)言(如CSP#)對(duì)不同的系統(tǒng)進(jìn)行建模；第二層是抽象層(Abstraction layer)，能夠?qū)ι蠈右呀?jīng)建模完成的系統(tǒng)進(jìn)行抽象分析，包括對(duì)不同系統(tǒng)的數(shù)據(jù)、環(huán)境等的抽象；第三層是中間呈現(xiàn)層(Intermediate representation layer)，負(fù)責(zé)將輸入的系統(tǒng)模型轉(zhuǎn)化為一種中間狀態(tài)(如標(biāo)簽遷移系統(tǒng)LTS)，以對(duì)應(yīng)底層不同的模型檢測(cè)算法；底層是分析層(Analysis layer)，包含模型檢測(cè)技術(shù)的關(guān)鍵算法，如死鎖檢測(cè)算法、LTL性質(zhì)檢測(cè)算法等.

PAT工具具有如此良好的擴(kuò)展性，因此可以利用建模層的抽象功能對(duì)建模層語(yǔ)言模塊進(jìn)行抽象，擴(kuò)展PAT的CSP#模塊(即并行模塊)，方便WBAN領(lǐng)域安全協(xié)議的建模驗(yàn)證.抽象后的語(yǔ)言模塊能夠自動(dòng)轉(zhuǎn)化為PAT已經(jīng)支持的語(yǔ)言，從而簡(jiǎn)化系統(tǒng)描述和實(shí)現(xiàn)過(guò)程，使得建模過(guò)程更人性化、更易使用.借助PAT工具良好的擴(kuò)展性，可方便對(duì)WBAN安全協(xié)議的建模.

圖1　模型檢測(cè)工具PAT的系統(tǒng)框架圖 Fig.1　The system framework of PAT

2無(wú)線體域網(wǎng)節(jié)點(diǎn)位置建模

2.1基于雙天線的無(wú)線體域網(wǎng)協(xié)議

無(wú)線體域網(wǎng)節(jié)點(diǎn)位置隨著人的移動(dòng)而變化，且傳感器節(jié)點(diǎn)體積小、容量和能源有限，很容易受到外界的攻擊，導(dǎo)致WBAN安全問(wèn)題層出不窮.為此，Javali等首次提出了基于雙天線的無(wú)線體域網(wǎng)安全認(rèn)證方案[15]，該方案基于接受信號(hào)強(qiáng)度(Received signal strength, RSS)，利用雙天線本身位置的分離性，能夠有效的將攻擊手段排除在其射頻范圍外.

該方案模型假設(shè)有一個(gè)雙天線的可信任實(shí)體節(jié)點(diǎn)CU和若干個(gè)單天線的待認(rèn)證節(jié)點(diǎn)，圖2給出了CU和傳感器節(jié)點(diǎn)布置圖.圖中節(jié)點(diǎn)E為攻擊者節(jié)點(diǎn)，B為誠(chéng)實(shí)實(shí)體節(jié)點(diǎn)，A1和A2分別代表CU的兩條天線.從圖2中可以看出：節(jié)點(diǎn)E到A1,A2的距離分別為e1,e2，節(jié)點(diǎn)B到A1,A2距離為d1,d2.

圖2　無(wú)線體域網(wǎng)安全認(rèn)證協(xié)議模型節(jié)點(diǎn)布置圖 Fig.2　The node layout of WBAN security authentication protocol model

節(jié)點(diǎn)E與可信任節(jié)點(diǎn)CU之間的通信過(guò)程如下：

1) CU→E:Probe={IDcu}

2) E→CU:Resp[0]={IDE,P0,L0,K0}

…

i) E→CU:Resp[i]={IDE,Pi,Li,Ki}

…

n) E→CU:Resp[n]={IDE,Pn,Ln,Kn}

其中：Pi為發(fā)送方發(fā)送消息時(shí)的能量；Ki為隨機(jī)數(shù)；Li為發(fā)送方的位置信息.

首先CU給傳感器節(jié)點(diǎn)向其射頻范圍內(nèi)廣播一個(gè)探測(cè)包Probe用以發(fā)現(xiàn)未認(rèn)證節(jié)點(diǎn)，傳感器節(jié)點(diǎn)收到探測(cè)包后發(fā)送一個(gè)響應(yīng)包Resp[i]，包含節(jié)點(diǎn)此時(shí)的發(fā)送能量，位置信息以及隨機(jī)數(shù)，CU收到響應(yīng)包后，計(jì)算包的RSSI(Receivedsignalstrengthindication)值為

其中：di為此時(shí)傳感器節(jié)點(diǎn)與CU的距離；α為節(jié)點(diǎn)間的距離能量指數(shù).

計(jì)算A1和A2的RSSI平均值RDavg，計(jì)算公式為

其中：j={1,2,…,n}，n為p和q之間的較小值.

4) CU將RDavg和RSSI門(mén)檻值RDth進(jìn)行比較，將小于RDth的傳感器節(jié)點(diǎn)視為攻擊者節(jié)點(diǎn)，大于RDth的傳感器節(jié)點(diǎn)則為誠(chéng)實(shí)節(jié)點(diǎn).最后CU給誠(chéng)實(shí)節(jié)點(diǎn)發(fā)送AssocResp[ACCEPT]消息.

2.2支持節(jié)點(diǎn)可移動(dòng)的抽象方法

由于人的日常行為使WBAN節(jié)點(diǎn)位置經(jīng)常發(fā)生移動(dòng)，要求在建模過(guò)程中考慮節(jié)點(diǎn)可能移動(dòng)到的位置，加大了建模的復(fù)雜度.利用CSP#語(yǔ)言的擴(kuò)展性對(duì)節(jié)點(diǎn)的移動(dòng)進(jìn)行抽象，可以有效提高建模的準(zhǔn)確率，下面采用二維坐標(biāo)對(duì)傳感節(jié)點(diǎn)的位置信息進(jìn)行抽象：

public class Location: ExpressionValue {

public intx; //節(jié)點(diǎn)位置x坐標(biāo)

public inty; //節(jié)點(diǎn)位置y坐標(biāo)

public int CalculateDistance(Location){…}

…

};

類Location中包含節(jié)點(diǎn)的二維坐標(biāo)，并通過(guò)自定義函數(shù)CalculateDistance()計(jì)算兩個(gè)節(jié)點(diǎn)間的歐氏距離，從而判斷節(jié)點(diǎn)位置是否移動(dòng)或超出射頻范圍.例如，假設(shè)節(jié)點(diǎn)A和B的位置信息分別為(xa,ya)，(xb,yb)，R表示節(jié)點(diǎn)傳輸距離，當(dāng)((xa-xb)(xa-xb)+(ya-yb)(ya-yb))>R·R時(shí)，說(shuō)明節(jié)點(diǎn)A和B間的距離超出了節(jié)點(diǎn)的射頻范圍.

知識(shí)集類KnowledgeSet用于存儲(chǔ)協(xié)議執(zhí)行過(guò)程中的數(shù)據(jù)信息，如：ID，隨機(jī)數(shù)等會(huì)直接影響協(xié)議能否正常執(zhí)行的變量.其中內(nèi)置SortedListlist用于存儲(chǔ)某個(gè)節(jié)點(diǎn)的知識(shí)，并隨著協(xié)議執(zhí)行不斷更新，UnitType表示知識(shí)類型，Object表示知識(shí)內(nèi)容.比如SortedList存儲(chǔ)了節(jié)點(diǎn)E的位置信息.UnitType枚舉了協(xié)議中所有的常量，枚舉類型保證了協(xié)議執(zhí)行過(guò)程中變量的值不會(huì)沖突.

public class KnowledgeSet : ExpressionValue {

public SortedList list;

public bool Add(UnitType, Object); //增加知識(shí)集

public Object Get(UnitType); //提取知識(shí)集

…

};

在上述抽象的基礎(chǔ)上，封裝成WSNNode結(jié)構(gòu)，擴(kuò)展PAT建模層的CSP#語(yǔ)言模塊，加入新的函數(shù)庫(kù)和語(yǔ)義，WSNNode類圖如圖3所示.

圖3　面向WBAN傳感節(jié)點(diǎn)建模的WSNNode類圖 Fig.3　The class diagram of WBAN sensor model

WSNNode結(jié)構(gòu)代表傳感器節(jié)點(diǎn)，其中包含了協(xié)議正常執(zhí)行的所有信息，包括節(jié)點(diǎn)ID、傳輸半徑、位置信息、知識(shí)集信息、隨機(jī)數(shù)等內(nèi)容.WSNNode結(jié)構(gòu)和新函數(shù)庫(kù)的設(shè)計(jì)極大地簡(jiǎn)化了WBAN安全協(xié)議的建模與驗(yàn)證.

3形式化建模與驗(yàn)證

3.1WBAN協(xié)議形式化建模及性質(zhì)描述

3.1.1協(xié)議誠(chéng)實(shí)實(shí)體節(jié)點(diǎn)建模

采用有窮狀態(tài)機(jī)描述協(xié)議中信任節(jié)點(diǎn)CU在協(xié)議執(zhí)行過(guò)程中的狀態(tài)遷移情況，如圖4所示.

圖4　協(xié)議信任節(jié)點(diǎn)CU的狀態(tài)轉(zhuǎn)換圖 Fig.4　The State transition diagram of trusted sensor CU

圖4中idle為CU的初始狀態(tài)；當(dāng)CU廣播一個(gè)探測(cè)包后自動(dòng)跳轉(zhuǎn)到State1狀態(tài)，并等待有未認(rèn)證的傳感器節(jié)點(diǎn)回送ACK確認(rèn)消息；收到ACK確認(rèn)消息后跳轉(zhuǎn)到State2狀態(tài)，判斷響應(yīng)節(jié)點(diǎn)是否在其射頻范圍內(nèi)；若在其射頻范圍內(nèi)，則與響應(yīng)節(jié)點(diǎn)重復(fù)交互n次消息，這n次消息由CU的兩條天線A1和A2隨機(jī)接收，結(jié)束交互后跳轉(zhuǎn)到State3狀態(tài)；State3狀態(tài)將計(jì)算著n次消息RSSI值的平均值RDavg，并跳轉(zhuǎn)到State4狀態(tài)；State4狀態(tài)將RSSI平均值與門(mén)檻RDth進(jìn)行比較，若RDavg>RDth則該傳感器節(jié)點(diǎn)為合法節(jié)點(diǎn)，認(rèn)證結(jié)束，跳轉(zhuǎn)到idle狀態(tài)；否則，認(rèn)證失敗，重新跳轉(zhuǎn)到idle狀態(tài).

需要注意的是，在認(rèn)證過(guò)程中，響應(yīng)節(jié)點(diǎn)可能會(huì)移動(dòng)節(jié)點(diǎn)位置，同樣信任節(jié)點(diǎn)CU在認(rèn)證過(guò)程中也會(huì)移動(dòng)節(jié)點(diǎn)位置.

下面介紹如何利用基于CSP#擴(kuò)展的利用抽象節(jié)點(diǎn)可移動(dòng)的建模方法對(duì)協(xié)議信任節(jié)點(diǎn)CU進(jìn)行建模.先對(duì)接下來(lái)需要涉及的CSP#語(yǔ)言語(yǔ)法進(jìn)行簡(jiǎn)單說(shuō)明：P()=Exp代表一個(gè)進(jìn)程或某主體的行為，其中()內(nèi)可帶參數(shù)，Exp代表過(guò)程描述，例如P()=e→P()代表進(jìn)程P循環(huán)執(zhí)行事件e；事件e可帶參數(shù)，例如e.exp1.exp2，其中exp1和exp2為變量；符號(hào)?和!代表輸入輸出通道，其中?為接受消息，!為發(fā)送消息；[]代表選擇，例如公式P[]Q表示可能執(zhí)行P，也可能執(zhí)行Q.

1) 定義兩個(gè)全局消息通道，作為協(xié)議中實(shí)體間消息傳遞的載體：

channel ca 0;

channel cb 0;

其中：通道ca用于承載CU廣播探測(cè)包的消息；通道cb用于傳遞CU與待認(rèn)證傳感器節(jié)點(diǎn)的n條重復(fù)消息，由于這n條消息的格式相同，故用同一通道代替.

PInitPre(NodeCU, Loc) =//初始化CU節(jié)點(diǎn)信息

IntruderInitial {

Node_A1.addItem(NodeCU, Loc, LCU_A1);

Node_A2.addItem(NodeCU, Loc, LCU_A2);

} -> PInit ();

PInit()=//開(kāi)始執(zhí)行協(xié)議

ca! Node_A1. everyone -> PInit() []

ca! Node_A2. everyone -> PInit() []

ca? Node_A1. to1 -> PInit() []

ca? Node_A2. to1 -> PInit() []

cb! Node_A1. tox. Power. Loc. Nonce -> PInit()[]

cb! Node_A2. tox. Power. Loc. Nonce -> PInit();

變量LCU_A1與LCU_A2分別代表了CU的兩條天線，其位置坐標(biāo)距離相差1 cm.LE代表攻擊節(jié)點(diǎn)的位置信息.用一個(gè)枚舉類型來(lái)初始化各個(gè)節(jié)點(diǎn)的ID信息，以避免重復(fù)ID的現(xiàn)象.

3.1.2節(jié)點(diǎn)可移動(dòng)的攻擊者建模

對(duì)攻擊者E的建模最為復(fù)雜.結(jié)合攻擊者位置的可移動(dòng)性以及攻擊者可以利用改變發(fā)送功率的方式偽造信號(hào)強(qiáng)度，對(duì)Dolev-Yao模型[16]進(jìn)行擴(kuò)展，攻擊者節(jié)點(diǎn)應(yīng)具有以下能力：

1) 可以竊聽(tīng)并截獲協(xié)議執(zhí)行過(guò)程中節(jié)點(diǎn)傳輸?shù)南ⅲ愿`取CU的正常通信范圍.

2) 可以冒充協(xié)議誠(chéng)實(shí)節(jié)點(diǎn)發(fā)送消息.

3) 根據(jù)截獲的消息，動(dòng)態(tài)增長(zhǎng)自己的知識(shí)集(KnowledgeSet對(duì)象)，從而產(chǎn)生新的攻擊消息.

4) 利用節(jié)點(diǎn)可移動(dòng)性，在誠(chéng)實(shí)節(jié)點(diǎn)射頻范圍外利用功率大、收發(fā)能力強(qiáng)的收發(fā)器向周圍節(jié)點(diǎn)發(fā)送信息，誘使周圍節(jié)點(diǎn)認(rèn)為攻擊節(jié)點(diǎn)在其射頻范圍內(nèi).

使用基于CSP#擴(kuò)展抽象節(jié)點(diǎn)可移動(dòng)的建模方法對(duì)攻擊者E建模，主要分為兩大部分：一、對(duì)網(wǎng)絡(luò)中的消息進(jìn)行截獲，破壞誠(chéng)實(shí)節(jié)點(diǎn)與CU的正常通信，以及竊取正常節(jié)點(diǎn)的信息；二、攻擊者移動(dòng)位置，偽裝成誠(chéng)實(shí)節(jié)點(diǎn)與CU通信.關(guān)鍵代碼如下：

PIntruderPre(NodeE, Loc) =

IntruderInitial {

NodeE.addItem(NodeE, Loc);

} -> PIntruder();

PIntruder() =

cA?ID_X . to1 ->//截獲并存儲(chǔ)消息

InterceptChanA {

…//截獲通道ca中的探測(cè)包并保存.

NodeE.addItem(…) ;

}-> PIntruder() []

cA?ID_X . to1. PowerX. LocX. NonceX ->

InterceptChanA {

…//截獲通道cb中的認(rèn)證消息并保存.

NodeE.addItem(…) ;

}-> PIntruder() []

//重放截獲的消息或根據(jù)獲取知識(shí)產(chǎn)生新消息

cA! NodeE. tox -> PIntruder() []

cB! NodeE. tox. Power. Loc. Nonce -> PIntruder() ;

攻擊者節(jié)點(diǎn)通過(guò)NodeE.addItem()函數(shù)將截獲的消息存入知識(shí)集KnowledgeSet對(duì)象中，隨后從知識(shí)集KnowledgeSet中任意選取ID、能量值、位置信息、隨機(jī)數(shù)組合成一個(gè)節(jié)點(diǎn)Node發(fā)送到通道中，攻擊者將枚舉所有可能的組合.

為了抽象節(jié)點(diǎn)的射頻范圍內(nèi)的所有移動(dòng)可能性，在初始階段定義了信任節(jié)點(diǎn)CU和攻擊者E的傳輸距離RadiusCU和RadiusE，給出如下PAT模型用于自動(dòng)生成所有可能的節(jié)點(diǎn)位置：

[]x1:{0…RadiusCU};y1:{0…RadiusCU};x2:{0…RadiusE};y2:{0…RadiusE}

@(PInitPre(NodeCU,newLocation(x1,y1))|||PIntruderPre(NodeE,newLocation(x2,y2)))

其中：符號(hào)[]表示x,y每次在其取值范圍內(nèi)任取一個(gè)值；|||表示協(xié)議發(fā)起方與接收方并發(fā)執(zhí)行.

針對(duì)位置可移動(dòng)的情況，攻擊者節(jié)點(diǎn)對(duì)位置的選擇不局限于其自身的可移動(dòng)范圍RadiusE.在最后的實(shí)驗(yàn)結(jié)果中我們可以看到，若RadiusE與CU的射頻范圍RadiusCU有重疊則攻擊者可冒充誠(chéng)實(shí)節(jié)點(diǎn)與CU通信，所以攻擊者的行為是不確定的，它的執(zhí)行是無(wú)限循環(huán)上述代碼，枚舉所有可能的狀態(tài)，從而能夠搜索整個(gè)狀態(tài)空間.

3.1.3LTL性質(zhì)描述

采用線性時(shí)序邏輯[17](Linear temporal logic, LTL)對(duì)協(xié)議屬性進(jìn)行規(guī)范描述.為了更方便的描述協(xié)議性質(zhì)，對(duì)CSP#擴(kuò)展定義如下變量：

#defineiniRunningEU(req_CU==true)；//當(dāng)攻擊者節(jié)點(diǎn)偽裝成誠(chéng)實(shí)節(jié)點(diǎn)給信任節(jié)點(diǎn)CU回送ACK確認(rèn)消息時(shí)置true.

#defineresCommitEU(ack_2_E==true)；//當(dāng)CU與節(jié)點(diǎn)E完成n次消息交互，并完成認(rèn)證時(shí)置true.

#defineMoveInRadius(OutRadius==true)；//當(dāng)攻擊者節(jié)點(diǎn)移入CU的射頻范圍時(shí)置true.

協(xié)議的認(rèn)證性是指確認(rèn)對(duì)方的真實(shí)身份，并保證其真實(shí)身份與消息中所聲稱的身份相一致.分析Chitra等提出的WBAN安全協(xié)議時(shí)，采用文[15]的方法進(jìn)行檢測(cè)：當(dāng)攻擊者E收到信任節(jié)點(diǎn)CU廣播的探測(cè)包，則待認(rèn)證的響應(yīng)方E必須回送一個(gè)確認(rèn)消息，同時(shí)開(kāi)始認(rèn)證過(guò)程，此時(shí)攻擊者E的位置必定在CU的射頻范圍內(nèi).因此可用LTL公式G:[](MoveInRadius→<>!(iniRunningEU→resCommitEU))表示協(xié)議的認(rèn)證性.其中<>表示最終(eventually)，[]表示一直(always)，!表示否定.若公式G不滿足，則表示有攻擊者闖入CU的射頻范圍內(nèi)，并認(rèn)證成功.

3.2實(shí)驗(yàn)結(jié)果與分析

將WBAN安全認(rèn)證協(xié)議的抽象CSP#模型和上一小節(jié)描述的LTL性質(zhì)導(dǎo)入PAT工具中進(jìn)行模擬驗(yàn)證.結(jié)果顯示公式G驗(yàn)證失敗，其反例路徑如圖5所示.

圖5　反例路徑圖 Fig.5　The path diagram of counter-example

反例路徑中間欄是被攻擊者截獲或篡改的消息，節(jié)點(diǎn)CU的兩條天線初始位置分別為(0,0)和(0,1)，節(jié)點(diǎn)E的初始位置為(0,6)，在與CU進(jìn)行認(rèn)證的過(guò)程中位置移動(dòng)到(0,4)，此時(shí)節(jié)點(diǎn)E已移入CU的射頻范圍，并在射頻范圍內(nèi)停留足夠長(zhǎng)的時(shí)間，從而滿足文[15]對(duì)認(rèn)證性的描述并完成認(rèn)證.說(shuō)明此種基于雙天線的WBAN安全協(xié)議存在缺陷：無(wú)法抵御可移動(dòng)攻擊者的入侵.結(jié)合原始協(xié)議可以得出驗(yàn)證失敗的原因：當(dāng)節(jié)點(diǎn)E移入CU的射頻范圍內(nèi)時(shí)，CU計(jì)算出的RSSI值大于RSSI門(mén)檻值RDth，若節(jié)點(diǎn)E在CU的射頻范圍內(nèi)的時(shí)間足夠長(zhǎng)，則n次消息認(rèn)證的RSSI平均值RDavg將大于RDth，最終認(rèn)證成功.

4結(jié)論

在PAT工具的基礎(chǔ)上，提出了一種支持節(jié)點(diǎn)可移動(dòng)的抽象建模數(shù)據(jù)結(jié)構(gòu)，擴(kuò)展了CSP#語(yǔ)言模塊.對(duì)Chitra等提出的安全認(rèn)證方案進(jìn)行建模和分析，發(fā)現(xiàn)若可移動(dòng)攻擊者的移動(dòng)范圍與信任節(jié)點(diǎn)CU的射頻范圍有交集，則有被攻擊的可能.研究發(fā)現(xiàn)：對(duì)建模過(guò)程進(jìn)行抽象能夠有效降低建模的復(fù)雜性，更直觀地發(fā)現(xiàn)協(xié)議存在的問(wèn)題，體現(xiàn)了抽象方法的實(shí)用性.因此下一步的研究將在更高層次抽象建模語(yǔ)言和模塊，針對(duì)無(wú)線體域網(wǎng)領(lǐng)域開(kāi)發(fā)專用建模語(yǔ)言，并研究抽象描述語(yǔ)言和CSP#的自動(dòng)轉(zhuǎn)換，實(shí)現(xiàn)模型檢測(cè)真正的自動(dòng)化.

參考文獻(xiàn)：

[1]陳鐵明,江頡,王小號(hào),等.一種改進(jìn)的基于位置的攻擊容忍WSN安全方案[J].傳感技術(shù)學(xué)報(bào),2012,25(4):545-551.

[2]陳慶章,張海洋,陳辰,等.基于WSN的人體姿態(tài)辨識(shí)系統(tǒng)設(shè)計(jì)[J].浙江工業(yè)大學(xué)學(xué)報(bào),2014,42(6):591-593.

[3]周曉,李杰,邊裕挺.基于無(wú)線傳感網(wǎng)絡(luò)的環(huán)境溫度檢測(cè)系統(tǒng)設(shè)計(jì)[J].浙江工業(yè)大學(xué)學(xué)報(bào),2013,41(4):440-443.

[4]陸歡佳,俞立,董齊芬,等.基于無(wú)線傳感網(wǎng)的樓宇環(huán)境檢測(cè)系統(tǒng)設(shè)計(jì)[J].浙江工業(yè)大學(xué)學(xué)報(bào),2011,39(6):683-687.

[5]JURIK A, WEAVER A. Remote medical monitoring[J]. Computer,2008,41(4):96-99.

[6]NOVOTNY M. Formal analysis of security protocols for wireless sensor networks[J]. Tatra Mountains Mathematical Publications,2010,47(1):81-97.

[7]林惠民,張文輝.模型檢測(cè)：理論、方法與應(yīng)用[J].電子學(xué)報(bào),2002,30(12A):1907-1912.

[8]ALADDIN M, THOMAS B, ARMAND T. Network protocol modeling: a time Petri net modular approach[C]//16th International Conference on Software, Telecommunications and Computer Networks. Split: IEEE Press,2008:273-277.

[9]HOLZMANN G J. The spin model checker primer and reference manual[M]. New Jersey: Addison Wesley,2003.

[10]JAVED K, KASHIF A, TROUBITSYNA E. Implementation of spin model checker for formal verification of distance vector routing protocol[J]. International Journal of Computer Science and Information Security,2010,8(3):1-6.

[11]LOWE G, ROSCOE B. Using CSP to detect errors in the TMN protocol[J]. IEEE Transactions on Software Engineering,1997,23(10):659-669.

[12]WANG Y Y, DONG H L, YU Y T, et al. Analyzing IEEE802.15.6 protocol with stochastic model checking[J]. Journal of Computational Information Systems,2015,11(3):935-947.

[13]SUN J, LIU Y AND DONG J S. Model checking CSP revisited: introducing a process analysis toolkit[J]. Communications in Computer and Information Science,2009,17(7):307-322.

[14]LIU Y, SUN J, DONG J S. Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney: Springer Press,2010:371-377.

[15]JAVALI C, REVADIGAR G, LIBMAN L, et al. SeAK: secure authentication and key generation protocol based on dual antennas for wireless body area networks[C]//10th International Workshop. Oxford: Springer Press,2014:74-89.

[16]DOLEV D, YAO A C. On the security of public key protocols[J]. IEEE Transactions on Information Theory,1981,29(2):350-357.

[17]BAIER C, KATOEN J P, LARSEN K G. Principles of model checking[M]. Cambridge: The MIT Press, 2008.

(責(zé)任編輯：劉巖)