基于模型檢測的無線傳感網(wǎng)安全協(xié)議形式化分析與改進(jìn)*

陳鐵明，何卡特，江 頡

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

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

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

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

1 模型檢測與SPIN工具

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

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

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

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

利用SPIN工具進(jìn)行WSN安全協(xié)議的設(shè)計(jì)、驗(yàn)證和改進(jìn)研究的基本過程如圖1。首先對安全協(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模型檢測工具進(jìn)行自動驗(yàn)證。若驗(yàn)證過程沒有發(fā)現(xiàn)錯誤，則說明協(xié)議滿足所描述的性質(zhì);否則，SPIN工具將產(chǎn)生一條反例路徑。協(xié)議設(shè)計(jì)者可通過分析反例路徑修改安全協(xié)議實(shí)體，再對修改后的安全協(xié)議重新進(jìn)行建模與驗(yàn)證，如此迭代改進(jìn)，最終可獲得滿足性質(zhì)要求的WSN安全協(xié)議。

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

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

下文將對Zhang等人提出的安全方案做簡要介紹。為便于讀者閱讀，先給出文章中用到的一些基本符號說明，具體見表1。

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

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

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

(1)根據(jù)輸入k，產(chǎn)生一個素?cái)?shù)q，生成一個q階加法群G1、一個q階乘法群G2和一個可接受的雙線映射，在G2中選擇一個生成元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)證的過程如下:

(1)A→＊:IDA

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

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

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

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

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

這里基于位置的一個重要安全特性在于:B在收到信息(1)時首先會判斷A的位置是否在其射頻范圍內(nèi)，即|lA－lB|≤RB，A在收到信息(2)時同樣會先判斷B的位置是否在其射頻范圍內(nèi)|lA－lB|≤RA，以此確保所聲稱的對方節(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é)議誠信實(shí)體建模

采用有窮自動機(jī)描述Zhang方案中的誠實(shí)實(shí)體在協(xié)議運(yùn)行中可能經(jīng)歷的狀態(tài)，認(rèn)證協(xié)議誠實(shí)實(shí)體包括認(rèn)證協(xié)議發(fā)起方和協(xié)議響應(yīng)方。協(xié)議發(fā)起方A的自動機(jī)模型如圖2所示:從idle狀態(tài)跳轉(zhuǎn)到狀態(tài)A1，向其射頻范圍內(nèi)發(fā)送一個廣播認(rèn)證請求req，然后跳轉(zhuǎn)到狀態(tài)A2，等待其鄰居節(jié)點(diǎn)即協(xié)議響應(yīng)方B的響應(yīng)消息;收到響應(yīng)消息ack_1后首先通過響應(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的自動機(jī)模型如圖3所示:當(dāng)有節(jié)點(diǎn)發(fā)起認(rèn)證請求時，B自動從idle狀態(tài)跳轉(zhuǎn)到B1狀態(tài)，等待接收認(rèn)證請求。B收到認(rèn)證請求后首先通過收到的位置信息計(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ù)一個響應(yīng)消息ack_1，并等待協(xié)議發(fā)起方發(fā)回的消息認(rèn)證碼;若時間超時仍沒有收到消息，則B跳轉(zhuǎn)回idle狀態(tài)，認(rèn)證失敗;若收到對方發(fā)回的消息認(rèn)證碼ack_2，則對該認(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é)議過程中可能會移動節(jié)點(diǎn)位置，同樣B在認(rèn)證協(xié)議執(zhí)行過程中也可能會移動節(jié)點(diǎn)位置。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

表2 抽象代碼中的符號說明

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

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

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

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

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

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

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

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

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

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

bool not_neighbor=0，當(dāng)A與B兩節(jié)點(diǎn)距離超過射頻范圍時置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)證請求后總會存在一條路徑使得兩者實(shí)現(xiàn)雙向認(rèn)證，G4表示若A與B的距離超過了節(jié)點(diǎn)的射頻范圍，則兩節(jié)點(diǎn)不可能完成雙向認(rèn)證。

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

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

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

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

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

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

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

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

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

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

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

(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)，但通過入侵者節(jié)點(diǎn)C作為中間人卻完成了雙向驗(yàn)證。由于改進(jìn)的方案支持了節(jié)點(diǎn)在有效范圍內(nèi)的自由活動，因此帶來了中間人入侵的威脅，且這種中間人攻擊將導(dǎo)致改進(jìn)的協(xié)議無法保障正常節(jié)點(diǎn)間的安全認(rèn)證。究其原因，如上述步驟(4)所述中間人成功施行了加密消息的重放，因此還可進(jìn)一步設(shè)計(jì)改進(jìn)方案以避免中間人攻擊。

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

4．1 方案描述

為克服中間人攻擊，可采用時間戳代替原協(xié)議中的隨機(jī)數(shù)。當(dāng)然，這里假設(shè)WSN擁有一種穩(wěn)定可靠的時間同步機(jī)制，作為時間戳方案的基本保障。改進(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)證

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

表3 Promela刻畫離散時間的符號和函數(shù)說明

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

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

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

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

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

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

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

5 結(jié)論

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

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

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

[3]陳鐵明，江頡，王小號，等．一種改進(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ǎ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]林惠民，張文輝．模型檢測:理論、方法與應(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/．