陳鐵明，何卡特，江 頡

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

隨著無(wú)線傳感器網(wǎng)絡(luò)WSN(Wireless Sensor Networks)應(yīng)用越來(lái)越廣泛，WSN安全問(wèn)題已日益突出，WSN 安全協(xié)議設(shè)計(jì)成為一項(xiàng)關(guān)鍵技術(shù)[1－3]。因此，將形式化方法應(yīng)用到WSN安全協(xié)議的建模與分析成為當(dāng)前的一個(gè)研究熱點(diǎn)[4]。

具IN的其安全性的reFeature cy模型檢測(cè)作為安全協(xié)議驗(yàn)證的一種重要的形式化方法，已取得了巨大成功[5]，影響較廣的方法與工具包括 SPIN[6]、SMV[7]、UPPAAL[8]等，且目前被不斷研究應(yīng)用于新型安全協(xié)議的形式化分析。針對(duì)無(wú)線傳感網(wǎng)絡(luò)，已有不少學(xué)者開(kāi)展了基于模型檢測(cè)的WSN安全協(xié)議驗(yàn)證方法研究。Tobarra等人對(duì)TinySec和 LEAP協(xié)議進(jìn)行 HLPSL(High-Level Protocol Specification Language)建模分析和驗(yàn)證，發(fā)現(xiàn)了兩條攻擊路徑[9];Ballarini等人利用概率模型檢測(cè)工具PRISM對(duì)WSN介質(zhì)訪問(wèn)控制層協(xié)議S-MAC進(jìn)行了形式化分析[10];Fehnker等人將模型檢測(cè)工具UPPAAL應(yīng)用于WSN協(xié)議的安全性分析，并加入圖形化建模和模擬[11－12]。在國(guó)內(nèi)也已有學(xué)者對(duì)SPINS安全協(xié)議簇中的SNEP協(xié)議進(jìn)行了SPIN/Promela建模分析和驗(yàn)證，發(fā)現(xiàn)協(xié)議存在不足之處[13]。

本文嘗試?yán)媚Ｐ蜋z測(cè)方法及SPIN工具分析一種基于位置的WSN安全協(xié)議[14]，并基于模型檢測(cè)結(jié)果設(shè)計(jì)和改進(jìn)該安全方案，將基于模型檢測(cè)的形式化方法有效應(yīng)用于WSN安全協(xié)議的分析與改進(jìn)。

1 模型檢測(cè)與SPIN工具

模型檢測(cè)最早由Clark和Emerson等人提出，其基本思想是用狀態(tài)遷移系統(tǒng)(S)表示系統(tǒng)的行為，用模態(tài)/時(shí)序邏輯公式(F)描述系統(tǒng)應(yīng)滿足的性質(zhì)，將“系統(tǒng)是否具有所期望的性質(zhì)”轉(zhuǎn)化為數(shù)學(xué)問(wèn)題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個(gè)模型”，用公式表示為 S■F?[15]。

模型檢測(cè)有兩種形式說(shuō)明語(yǔ)言，性質(zhì)說(shuō)明語(yǔ)言用于描述系統(tǒng)的性質(zhì)，模型描述語(yǔ)言用于描述系統(tǒng)的模型。模型檢測(cè)技術(shù)就是用于檢驗(yàn)由模型描述語(yǔ)言描述的系統(tǒng)模型是否滿足由性質(zhì)說(shuō)明語(yǔ)言描述的系統(tǒng)性質(zhì)。模型檢測(cè)是一種較成熟的安全協(xié)議分析和驗(yàn)證技術(shù)，與其他形式化方法相比有如下優(yōu)勢(shì):(1)模型檢測(cè)可搜索協(xié)議運(yùn)行的整個(gè)狀態(tài)空間;(2)當(dāng)檢測(cè)到錯(cuò)誤時(shí)可返回一條反例路徑;(3)易于實(shí)現(xiàn)分析自動(dòng)化。

SPIN(Simple Promela Interpreter)是由貝爾實(shí)驗(yàn)室開(kāi)發(fā)的一款模型檢測(cè)工具，其模型描述語(yǔ)言為Promela，性質(zhì)說(shuō)明語(yǔ)言為L(zhǎng)TL(Linear Temporal Logic，線性時(shí)序邏輯)。SPIN的最新版本可提供直觀的反例顯示和單步推進(jìn)查看等交互功能，可實(shí)現(xiàn)快速協(xié)議建模和反例分析。

圖1 基于SPIN的無(wú)線傳感網(wǎng)絡(luò)安全協(xié)議設(shè)計(jì)、驗(yàn)證與改進(jìn)過(guò)程

利用SPIN工具進(jìn)行WSN安全協(xié)議的設(shè)計(jì)、驗(yàn)證和改進(jìn)研究的基本過(guò)程如圖1。首先對(duì)安全協(xié)議實(shí)體進(jìn)行Promela建模，將協(xié)議實(shí)體轉(zhuǎn)化為進(jìn)程(proctype)描述，實(shí)體間消息交互表示為信道(chan)通信;再根據(jù)Delov-Yao模型構(gòu)建協(xié)議入侵者模型，采用LTL邏輯描述待驗(yàn)證的協(xié)議性質(zhì)，最后將Promela協(xié)議模型和LTL協(xié)議性質(zhì)公式導(dǎo)入到SPIN模型檢測(cè)工具進(jìn)行自動(dòng)驗(yàn)證。若驗(yàn)證過(guò)程沒(méi)有發(fā)現(xiàn)錯(cuò)誤，則說(shuō)明協(xié)議滿足所描述的性質(zhì);否則，SPIN工具將產(chǎn)生一條反例路徑。協(xié)議設(shè)計(jì)者可通過(guò)分析反例路徑修改安全協(xié)議實(shí)體，再對(duì)修改后的安全協(xié)議重新進(jìn)行建模與驗(yàn)證，如此迭代改進(jìn)，最終可獲得滿足性質(zhì)要求的WSN安全協(xié)議。

2 基于位置的WSN安全協(xié)議

無(wú)線傳感器網(wǎng)絡(luò)通常情況下部署在無(wú)人值守且難以維護(hù)的環(huán)境中，傳感節(jié)點(diǎn)數(shù)量眾多，且節(jié)點(diǎn)較為脆弱，易受到各種物理攻擊。據(jù)此，Zhang等人首次提出了基于位置的攻擊容忍安全方案[14]，采用基于IBE的WSN安全設(shè)計(jì)，可將受攻擊的威脅限制在一個(gè)有限的節(jié)點(diǎn)位置活動(dòng)范圍內(nèi)。

下文將對(duì)Zhang等人提出的安全方案做簡(jiǎn)要介紹。為便于讀者閱讀，先給出文章中用到的一些基本符號(hào)說(shuō)明，具體見(jiàn)表1。

表1 基于位置的安全協(xié)議基本符號(hào)說(shuō)明

文獻(xiàn)[14]給出了加密系統(tǒng)的初始化假設(shè)如下:

系統(tǒng)選擇一個(gè)安全參數(shù)k∈Z+，執(zhí)行以下算法:

(1)根據(jù)輸入k，產(chǎn)生一個(gè)素?cái)?shù)q，生成一個(gè)q階加法群G1、一個(gè)q階乘法群G2和一個(gè)可接受的雙線映射，在G2中選擇一個(gè)生成元P;

根據(jù)節(jié)點(diǎn)A的ID及其位置信息，計(jì)算基于位置的ID公鑰為:LQA=H1(IDA‖lA，私鑰為:ldA=sLQA=sH1(IDA‖lA)。

現(xiàn)假設(shè)節(jié)點(diǎn)B是節(jié)點(diǎn)A的鄰居節(jié)點(diǎn)，則A與B完成雙向認(rèn)證的過(guò)程如下:

(1)A→＊:IDA

(2)B→A:IDB，lB，nB，hKBA(nA‖n)

(3)A→B:hKAB(nA‖n)

認(rèn)證協(xié)議開(kāi)始時(shí)協(xié)議發(fā)起方A先向其射頻范圍內(nèi)廣播一個(gè)認(rèn)證請(qǐng)求消息，包含A的ID，A的位置信息以及一個(gè)A產(chǎn)生的隨機(jī)數(shù);鄰居節(jié)點(diǎn)B在收到認(rèn)證請(qǐng)求后，向A返回一條響應(yīng)消息，包含B的ID，B的位置信息，B產(chǎn)生的隨機(jī)數(shù)以及利用B的私鑰和A的公鑰計(jì)算得到的消息認(rèn)證碼;A收到B發(fā)送的響應(yīng)消息后再回復(fù)一個(gè)利用A的私鑰和B的公鑰計(jì)算得到的消息認(rèn)證碼，從而完成雙向認(rèn)證。

上述消息認(rèn)證碼使用的密鑰滿足:

由于ldA和ldB僅為A和B分別私有，因此可保證KB，A和KA，B能且僅能被A和B計(jì)算得到。A可通過(guò)計(jì)算得到，再與從 B收到的響應(yīng)信息中的進(jìn)行對(duì)比，判斷兩者是否相等完成對(duì)節(jié)點(diǎn)B的身份認(rèn)證;同樣B也可以通過(guò)計(jì)算得到與從A收到的響應(yīng)信息中的進(jìn)行對(duì)比，判斷兩者是否相等，從而完成鄰居節(jié)點(diǎn)間的雙向認(rèn)證。

這里基于位置的一個(gè)重要安全特性在于:B在收到信息(1)時(shí)首先會(huì)判斷A的位置是否在其射頻范圍內(nèi)，即|lA－lB|≤RB，A在收到信息(2)時(shí)同樣會(huì)先判斷B的位置是否在其射頻范圍內(nèi)|lA－lB|≤RA，以此確保所聲稱的對(duì)方節(jié)點(diǎn)是否為真實(shí)的鄰居節(jié)點(diǎn)，有效避免非鄰居節(jié)點(diǎn)的安全攻擊。

3 安全協(xié)議的形式化驗(yàn)證

3．1 節(jié)點(diǎn)位置固定的安全驗(yàn)證

3．1．1 協(xié)議誠(chéng)信實(shí)體建模

采用有窮自動(dòng)機(jī)描述Zhang方案中的誠(chéng)實(shí)實(shí)體在協(xié)議運(yùn)行中可能經(jīng)歷的狀態(tài)，認(rèn)證協(xié)議誠(chéng)實(shí)實(shí)體包括認(rèn)證協(xié)議發(fā)起方和協(xié)議響應(yīng)方。協(xié)議發(fā)起方A的自動(dòng)機(jī)模型如圖2所示:從idle狀態(tài)跳轉(zhuǎn)到狀態(tài)A1，向其射頻范圍內(nèi)發(fā)送一個(gè)廣播認(rèn)證請(qǐng)求req，然后跳轉(zhuǎn)到狀態(tài)A2，等待其鄰居節(jié)點(diǎn)即協(xié)議響應(yīng)方B的響應(yīng)消息;收到響應(yīng)消息ack_1后首先通過(guò)響應(yīng)中的位置信息計(jì)算響應(yīng)節(jié)點(diǎn)是否為真實(shí)的鄰居節(jié)點(diǎn)，并計(jì)算消息認(rèn)證碼進(jìn)行認(rèn)證，若認(rèn)證失敗，則跳轉(zhuǎn)回idle協(xié)議初始狀態(tài);若認(rèn)證成功則發(fā)送確認(rèn)消息ack_2給響應(yīng)方B。協(xié)議響應(yīng)方B的自動(dòng)機(jī)模型如圖3所示:當(dāng)有節(jié)點(diǎn)發(fā)起認(rèn)證請(qǐng)求時(shí)，B自動(dòng)從idle狀態(tài)跳轉(zhuǎn)到B1狀態(tài)，等待接收認(rèn)證請(qǐng)求。B收到認(rèn)證請(qǐng)求后首先通過(guò)收到的位置信息計(jì)算協(xié)議發(fā)起節(jié)點(diǎn)是否為B的鄰居節(jié)點(diǎn)，若不是鄰居節(jié)點(diǎn)，則協(xié)議結(jié)束，B跳轉(zhuǎn)回idle狀態(tài);若是B的鄰居節(jié)點(diǎn)，則向協(xié)議發(fā)起方回復(fù)一個(gè)響應(yīng)消息ack_1，并等待協(xié)議發(fā)起方發(fā)回的消息認(rèn)證碼;若時(shí)間超時(shí)仍沒(méi)有收到消息，則B跳轉(zhuǎn)回idle狀態(tài)，認(rèn)證失敗;若收到對(duì)方發(fā)回的消息認(rèn)證碼ack_2，則對(duì)該認(rèn)證碼進(jìn)行認(rèn)證，成功則表示此次協(xié)議雙向認(rèn)證成功，若認(rèn)證失敗則跳轉(zhuǎn)回idle狀態(tài)。

圖2 認(rèn)證協(xié)議發(fā)起方A的狀態(tài)轉(zhuǎn)換圖

圖3 認(rèn)證協(xié)議響應(yīng)方B的狀態(tài)轉(zhuǎn)換圖

值得注意的是，協(xié)議發(fā)起方A在執(zhí)行認(rèn)證協(xié)議過(guò)程中可能會(huì)移動(dòng)節(jié)點(diǎn)位置，同樣B在認(rèn)證協(xié)議執(zhí)行過(guò)程中也可能會(huì)移動(dòng)節(jié)點(diǎn)位置。

下面將介紹基于SPIN工具的模型檢測(cè)過(guò)程。由于WSN及基于位置的安全協(xié)議的特殊性，首先需對(duì)傳感節(jié)點(diǎn)的位置信息進(jìn)行建模。采用如下二維坐標(biāo)表示傳感節(jié)點(diǎn)的位置信息:

通過(guò)自定義函數(shù)cal_distance計(jì)算兩個(gè)節(jié)點(diǎn)間的歐拉距離。

受到水電站施工地理位置、地質(zhì)條件以及經(jīng)濟(jì)技術(shù)的影響，那么這些因素也會(huì)對(duì)水輪發(fā)電機(jī)組運(yùn)行狀態(tài)造成影響。由于每個(gè)水電站都是專門設(shè)計(jì)的，使得不同水電站的水輪發(fā)電機(jī)組振動(dòng)情況不盡相同，可比性較差，可見(jiàn)其振動(dòng)故障具有不規(guī)則性。

同時(shí)定義三個(gè)全局消息通道實(shí)現(xiàn)協(xié)議描述中的三輪消息的傳輸:

其中N為信道容量，當(dāng)N=0時(shí)表示采用會(huì)面點(diǎn)通信(信道為同步通信通道)，當(dāng)N＞0時(shí)表示采用異步通信，此時(shí)信道可以對(duì)接收到的信息進(jìn)行緩存。sk表示用于消息認(rèn)證碼的會(huì)話密鑰，可通過(guò)認(rèn)證雙方中任一個(gè)節(jié)點(diǎn)的公鑰與另一個(gè)節(jié)點(diǎn)的私鑰計(jì)算得到，定義如下:

節(jié)點(diǎn)的公鑰和私鑰都基于節(jié)點(diǎn)的ID及其位置信息，私鑰僅為對(duì)應(yīng)的節(jié)點(diǎn)所私有，公鑰則可被其他節(jié)點(diǎn)通過(guò)其位置信息和ID計(jì)算得到。

3．1．2 入侵者節(jié)點(diǎn)建模

根據(jù)Dolev-Yao模型[16]，入侵者節(jié)點(diǎn)具有如下攻擊能力:

(1)能夠截獲協(xié)議發(fā)起方A與協(xié)議響應(yīng)方B之間通信的所有消息。

(2)若截獲的消息無(wú)法解密，入侵者可轉(zhuǎn)發(fā)消息，或者先作存儲(chǔ)以備重放。

(3)若截獲的消息沒(méi)有加密，則入侵者可以任意修改截獲的消息并轉(zhuǎn)發(fā)，或先作存儲(chǔ)以便隨時(shí)重放。

(4)入侵者可冒充A或B的ID發(fā)送消息，例如可冒充A發(fā)起認(rèn)證協(xié)議。

(5)可以解密已知密鑰加密的任意消息。

入侵者的Promela描述較誠(chéng)實(shí)實(shí)體A與B復(fù)雜得多，下面給出抽象的Promela關(guān)鍵代碼:

入侵者行為應(yīng)包括所有的可能，且執(zhí)行是不確定的，可涵蓋協(xié)議執(zhí)行的整個(gè)狀態(tài)空間。上述抽象代碼中的主要符號(hào)含義說(shuō)明見(jiàn)表2。

表2 抽象代碼中的符號(hào)說(shuō)明

3．1．3 協(xié)議性質(zhì)描述

認(rèn)證協(xié)議的認(rèn)證性用來(lái)確定通信對(duì)方的身份是否與其在消息中聲稱的身份一致。下面采用LTL邏輯描述Zhang安全協(xié)議的認(rèn)證性。

文獻(xiàn)[17]給出了對(duì)認(rèn)證協(xié)議執(zhí)行模型檢測(cè)的一般方法。鑒于無(wú)線傳感器網(wǎng)絡(luò)的特殊性，本文對(duì)Promela擴(kuò)展定義如下變量:

bool req_a=0，當(dāng)協(xié)議發(fā)起者(A)開(kāi)始廣播認(rèn)證請(qǐng)求時(shí)置1;

bool req_b=0，當(dāng)協(xié)議響應(yīng)者(B)收到A發(fā)出的廣播請(qǐng)求時(shí)置1;

bool ack_1_b=0，當(dāng)B向A發(fā)送消息2時(shí)置1;

bool ack_1_a=0，當(dāng)A收到B發(fā)送的消息2并認(rèn)證通過(guò)時(shí)置1;

bool ack_2_a=0，當(dāng)A向B發(fā)送消息3時(shí)置1;

bool ack_2_b=0，當(dāng)B收到消息3并驗(yàn)證通過(guò)時(shí)置1;

bool authenticated=0，當(dāng)以上六個(gè)值都為1時(shí)置1，即表示A與B完成雙向認(rèn)證。

bool not_neighbor=0，當(dāng)A與B兩節(jié)點(diǎn)距離超過(guò)射頻范圍時(shí)置1。

利用以上變量構(gòu)造LTL公式如下:

其中[]表示一直(always)，U表示直到(until)，＜＞表示最終(eventually)。若G1不滿足則表示有入侵節(jié)點(diǎn)冒充B和A通信，若G2不滿足則表示有入侵節(jié)點(diǎn)冒充A與B通信。G3表示B在收到A的認(rèn)證請(qǐng)求后總會(huì)存在一條路徑使得兩者實(shí)現(xiàn)雙向認(rèn)證，G4表示若A與B的距離超過(guò)了節(jié)點(diǎn)的射頻范圍，則兩節(jié)點(diǎn)不可能完成雙向認(rèn)證。

3．1．4 協(xié)議分析結(jié)果

將協(xié)議實(shí)體的Promela模型與上述LTL性質(zhì)描述公式導(dǎo)入到SPIN中執(zhí)行模型檢測(cè)。結(jié)果顯示G1，G2，G4都滿足，在檢驗(yàn)G3時(shí)發(fā)現(xiàn)一條反例，反例路徑如圖4所示。

圖4 SPIN驗(yàn)證性質(zhì)G3時(shí)產(chǎn)生的反例路徑

反例路徑表明當(dāng)節(jié)點(diǎn)A在發(fā)送消息1后若移動(dòng)了位置，再發(fā)送認(rèn)證請(qǐng)求時(shí)就會(huì)導(dǎo)致消息2始終無(wú)法通過(guò)認(rèn)證，從而使A的合法鄰居節(jié)點(diǎn)B始終無(wú)法與A完成雙向認(rèn)證。結(jié)合SPIN反例分析原始協(xié)議，容易找出導(dǎo)致認(rèn)證失敗的原因。因?yàn)槿艄?jié)點(diǎn)A移動(dòng)位置，即假設(shè)lA改變?yōu)閘A，但執(zhí)行認(rèn)證協(xié)議時(shí)節(jié)點(diǎn)A擁有的依然是基于lA的ID私鑰ldA，即沒(méi)有基于lA的ID私鑰ldA，因此即使A節(jié)點(diǎn)移動(dòng)后仍處在B節(jié)點(diǎn)的鄰居位置范圍內(nèi)，也將無(wú)法通過(guò)B的安全認(rèn)證。

3．2 節(jié)點(diǎn)位置移動(dòng)的安全驗(yàn)證

為使節(jié)點(diǎn)能在一定范圍內(nèi)移動(dòng)而不影響協(xié)議的認(rèn)證性，需將節(jié)點(diǎn)私鑰和公鑰的計(jì)算與節(jié)點(diǎn)固定的具體位置信息無(wú)關(guān)，為此可提出如下改進(jìn)方案:

假設(shè)某個(gè)數(shù)據(jù)網(wǎng)關(guān)管轄的簇中心位置為L(zhǎng)0，簇內(nèi)節(jié)點(diǎn)的合法活動(dòng)范圍半徑為R0，則簇L0內(nèi)節(jié)點(diǎn)i的標(biāo)識(shí)可由L0‖IDi唯一確定，在對(duì)節(jié)點(diǎn)i的密鑰管理過(guò)程中我們可通過(guò)L0‖IDi計(jì)算節(jié)點(diǎn)的私鑰和公鑰，從而使節(jié)點(diǎn)私鑰和公鑰計(jì)算不依賴于節(jié)點(diǎn)的固定位置，以便使節(jié)點(diǎn)i可在簇L0的合法活動(dòng)范圍內(nèi)自由移動(dòng)。

我們可類似對(duì)改進(jìn)后的方案進(jìn)行建模和驗(yàn)證，需要注意的是當(dāng)鄰居節(jié)點(diǎn)收到A的廣播信息后，原始方案僅需判斷A是否在B的射頻范圍內(nèi)，現(xiàn)在則還需判斷A移動(dòng)后的位置是否超出了簇內(nèi)節(jié)點(diǎn)的合法活動(dòng)范圍。同樣A在收到B回復(fù)的消息2時(shí)也要先判斷兩個(gè)不等式|lB－l0|≤R0，|lA－lB|≤RA是否成立。若前者不成立，則說(shuō)明節(jié)點(diǎn)B移動(dòng)后的位置超出了合法范圍;若后者不成立，則說(shuō)明節(jié)點(diǎn)B不是節(jié)點(diǎn)A的鄰居節(jié)點(diǎn)。只有當(dāng)兩者都成立時(shí)，協(xié)議才能正常進(jìn)行。

建模驗(yàn)證4．1．3節(jié)提出的G1～G44條性質(zhì)。通過(guò)SPIN模型檢測(cè)，G1、G2、G3驗(yàn)證成功，說(shuō)明修改后的協(xié)議克服了原協(xié)議節(jié)點(diǎn)無(wú)法移動(dòng)的問(wèn)題，但在檢驗(yàn)性質(zhì)G4時(shí)發(fā)現(xiàn)了錯(cuò)誤反例，反例路徑見(jiàn)圖5所示。

圖5 SPIN驗(yàn)證性質(zhì)G4時(shí)的反例路徑

根據(jù)SPIN產(chǎn)生的反例圖，不難給出協(xié)議可能面臨的一個(gè)具體過(guò)程描述如下:

(1)A→＊:IDA

(2)C→＊:IDA

(3)B→C(A):IDB，lB，nB，hKB，A(nA‖n)

(4)C(B)→A:IDB，lC，nB，hKB，A(nA‖n)

(5)A→C(B):hKA，B(nA‖n)

(6)C(A)→B:hKA，B(nA‖n)

反例路徑實(shí)際上表明了認(rèn)證協(xié)議的一種中間人攻擊，即A與B并非鄰居節(jié)點(diǎn)，但通過(guò)入侵者節(jié)點(diǎn)C作為中間人卻完成了雙向驗(yàn)證。由于改進(jìn)的方案支持了節(jié)點(diǎn)在有效范圍內(nèi)的自由活動(dòng)，因此帶來(lái)了中間人入侵的威脅，且這種中間人攻擊將導(dǎo)致改進(jìn)的協(xié)議無(wú)法保障正常節(jié)點(diǎn)間的安全認(rèn)證。究其原因，如上述步驟(4)所述中間人成功施行了加密消息的重放，因此還可進(jìn)一步設(shè)計(jì)改進(jìn)方案以避免中間人攻擊。

4 基于位置的WSN安全協(xié)議改進(jìn)

4．1 方案描述

為克服中間人攻擊，可采用時(shí)間戳代替原協(xié)議中的隨機(jī)數(shù)。當(dāng)然，這里假設(shè)WSN擁有一種穩(wěn)定可靠的時(shí)間同步機(jī)制，作為時(shí)間戳方案的基本保障。改進(jìn)后的鄰居節(jié)點(diǎn)安全認(rèn)證協(xié)議描述如下:

(1)A→＊:IDA

(2)B→A:IDB，lB，tB，hKB，A(tA‖t)

(3)A→B:hKA，B(tA‖t)

4．2 安全驗(yàn)證

引入時(shí)間戳后需要增加對(duì)系統(tǒng)的時(shí)間刻畫，本文采用了文獻(xiàn)[18]在Promela中引入的離散時(shí)間機(jī)制(由于計(jì)算消耗和狀態(tài)空間的原因，Promela自身不支持浮點(diǎn)型)。為方便討論，這里給出表3的刻畫離散時(shí)間所涉及的符號(hào)和函數(shù)說(shuō)明。

表3 Promela刻畫離散時(shí)間的符號(hào)和函數(shù)說(shuō)明

對(duì)增加時(shí)間戳后的方案再次進(jìn)行Promela建模和模型檢測(cè)分析。首先在4．2節(jié)所述的協(xié)議描述基礎(chǔ)上，增加如下一些行為刻畫:

(1)在協(xié)議發(fā)起者 A發(fā)起協(xié)議之前需要用udelay函數(shù)進(jìn)行一個(gè)不確定延時(shí)，以表示協(xié)議可能在一個(gè)不確定的時(shí)刻發(fā)起;

(2)在每次協(xié)議實(shí)體(包括誠(chéng)實(shí)實(shí)體和入侵者)發(fā)送消息后需要利用delay函數(shù)進(jìn)行一個(gè)適當(dāng)時(shí)間的延時(shí)，用以表示正常傳輸延時(shí);

(3)A在發(fā)送消息1時(shí)將當(dāng)前系統(tǒng)時(shí)間賦值給，代替隨即數(shù);同理B在發(fā)送消息2時(shí)將當(dāng)前系統(tǒng)時(shí)間賦值給，代替隨即數(shù)。

(4)B在接收消息1時(shí)將計(jì)算tB是否小于等于一個(gè)正常設(shè)定的傳輸延時(shí)，若tB－t則說(shuō)明協(xié)議消息過(guò)時(shí)存在重放攻擊的安全隱患，終止協(xié)議。

協(xié)議實(shí)體建模后再次驗(yàn)證性質(zhì)G1～G4，均未發(fā)現(xiàn)錯(cuò)誤的反例路徑，說(shuō)明改進(jìn)的基于位置的攻擊容忍安全協(xié)議克服了Zhang方案中節(jié)點(diǎn)不能移動(dòng)的問(wèn)題，使節(jié)點(diǎn)可在一個(gè)合法移動(dòng)范圍內(nèi)完成認(rèn)證協(xié)議，同時(shí)還能有效抵抗惡意的中間人攻擊。

基于位置的WSN安全協(xié)議的形式化分析和改進(jìn)研究表明，模型檢測(cè)不僅可以直接進(jìn)行WSN安全協(xié)議的分析與驗(yàn)證，并且還可幫助完成協(xié)議的設(shè)計(jì)改進(jìn)。

5 結(jié)論

隨著無(wú)線傳感網(wǎng)絡(luò)應(yīng)用的展開(kāi)，對(duì)于WSN安全問(wèn)題的研究迫在眉睫，其中無(wú)線傳感網(wǎng)絡(luò)安全協(xié)議的設(shè)計(jì)和分析更是成為當(dāng)前的研究熱點(diǎn)之一。本文采用模型檢測(cè)方法對(duì)Zhang等人提出的基于位置的攻擊容忍安全方案進(jìn)行建模和分析，發(fā)現(xiàn)節(jié)點(diǎn)移動(dòng)后將導(dǎo)致鄰居節(jié)點(diǎn)無(wú)法認(rèn)證的問(wèn)題，然后直接改進(jìn)提出支持節(jié)點(diǎn)可移動(dòng)的安全解決方案并再次建模驗(yàn)證，發(fā)現(xiàn)存在中間人認(rèn)證攻擊，最后通過(guò)將隨機(jī)數(shù)改為時(shí)間戳，獲得一個(gè)可通過(guò)模型檢測(cè)安全驗(yàn)證的改進(jìn)方案。本文的工作表明，模型檢測(cè)不僅可以分析和驗(yàn)證基于位置的新型WSN安全協(xié)議，并且還可有效協(xié)助設(shè)計(jì)和改進(jìn)WSN安全協(xié)議，體現(xiàn)了形式化方法在WSN安全建模和分析中的應(yīng)用前景。本文采用的是SPIN工具提供的Promela語(yǔ)言描述WSN安全協(xié)議的形式化模型，需要較多的領(lǐng)域知識(shí)和人工經(jīng)驗(yàn)，因此下一步的研究將嘗試提出面向WSN安全協(xié)議的專用描述語(yǔ)言，并研究描述語(yǔ)言和Promela語(yǔ)言之間的自動(dòng)轉(zhuǎn)換，基于SPIN開(kāi)發(fā)WSN安全協(xié)議的自動(dòng)化分析與驗(yàn)證工具。

[1]陳鐵明，白素剛，蔡家楣．TinyIBE:面向無(wú)線傳感器網(wǎng)絡(luò)的身份公鑰加密系統(tǒng)[J]．傳感技術(shù)學(xué)報(bào)，2009，22(8):1193－1197．

[2]陳鐵明，葛亮，蔡家楣，等．TinyTCSec:一種新的輕量級(jí)無(wú)線傳感器網(wǎng)絡(luò)鏈路加密協(xié)議[J]．傳感技術(shù)學(xué)報(bào)，2011，24(2):275－282．

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

[4]Novotny M．Formal Analysis of Security Protocols for Wireless Sensor Networks[J]．Tatra Mt Math Publ，2010，47:81－97．

[5]Clarke E M．The Birth of Model Checking[M]．25 Years of Model Checking．Heidelberg:Springer，2008:1－26．

[6]Holzmann G J．The Spin Model Checker Primer and Reference Manual[M]．New Jersey:Addison Wesley，2003．

[7]SMV home page，http://www．cs．cmu．edu/～modelcheck/smv．html．

[8]Kim G Larsen，Paul Pettersson，Wang Yi．Uppaal in a Nutshell[J]．International Journal on Software Tools for Technology Transfer，1997，1(2):134－152．

[9]Llanos Tobarra，Diego Cazorla，F(xiàn)ernando Cuartero，et al．Model Checking Wireless Sensor Network Security Protocols:TinySec+LEAP[J]．IFIP International Federation for Information Processing，2007，248:95－106．

[10]Ballarini P，Miller A．Model Checking Medium Access Control for SensorNetworks[C]//Second InternationalSymposium on Leveraging Applications of Formal Methods，Verification and Validation，15－19 Nov．2006，255－262．

[11]Fehnker Ansgar，van Hoesel Lodewijk，Mader Angelika，et al．Modelling and Verification of the LMAC Protocol for Wireless SensorNetworks[C]//6th InternationalIntergrated Formal Methods Conference Oxford，UK，2－5 July，2007，253－272．

[12]Fehnker A，F(xiàn)ruth M，McIver A K．Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols[M]．Methods，Models and Tools for Fault Tolerance，Heidelberg:Springer，2009:1－24．

[13]敬超，常亮，古天龍．基于SPIN的無(wú)線傳感網(wǎng)絡(luò)安全協(xié)議建模與分析[J]．計(jì)算機(jī)科學(xué)，2009，36(10):132－136．

[14]Zhang Y，Liu W．Location-Based Compromise-Tolerant Security Mechanisms for Wireless Sensor Networks[J]．IEEE Journalof Selected Areas in Communications，2006，24(2):247－260．

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

[16]Dolev D，Yao A C．On the Security of Public Key Protocols[C]//FOCS，IEEE．1981，29:350－357．

[17]Marrero W，Clarke E，Jha S，et al．A Model Checker for Authentication Protocols 1997[C]//DIMACS Workshop on Design and Formal Verification of Security Protocols．Sep 1997:147－166．

[18]Bosnacki D．Enhancing State Space Reduction Techniques for Model Checking[D]．Technical University Eindhoven，Eindhover，The Netherlands，2001．Available at http://www．win．tue．nl/～dragan/Thesis/．