基于模型檢測的無線傳感網安全協議形式化分析與改進*

陳鐵明，何卡特，江 頡

(浙江工業大學計算機科學與技術學院，杭州310023)

隨著無線傳感器網絡WSN(Wireless Sensor Networks)應用越來越廣泛，WSN安全問題已日益突出，WSN 安全協議設計成為一項關鍵技術[1－3]。因此，將形式化方法應用到WSN安全協議的建模與分析成為當前的一個研究熱點[4]。

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

本文嘗試利用模型檢測方法及SPIN工具分析一種基于位置的WSN安全協議[14]，并基于模型檢測結果設計和改進該安全方案，將基于模型檢測的形式化方法有效應用于WSN安全協議的分析與改進。

1 模型檢測與SPIN工具

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

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

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

圖1 基于SPIN的無線傳感網絡安全協議設計、驗證與改進過程

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

2 基于位置的WSN安全協議

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

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

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

文獻[14]給出了加密系統的初始化假設如下:

系統選擇一個安全參數k∈Z+，執行以下算法:

(1)根據輸入k，產生一個素數q，生成一個q階加法群G1、一個q階乘法群G2和一個可接受的雙線映射，在G2中選擇一個生成元P;

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

現假設節點B是節點A的鄰居節點，則A與B完成雙向認證的過程如下:

(1)A→＊:IDA

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

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

認證協議開始時協議發起方A先向其射頻范圍內廣播一個認證請求消息，包含A的ID，A的位置信息以及一個A產生的隨機數;鄰居節點B在收到認證請求后，向A返回一條響應消息，包含B的ID，B的位置信息，B產生的隨機數以及利用B的私鑰和A的公鑰計算得到的消息認證碼;A收到B發送的響應消息后再回復一個利用A的私鑰和B的公鑰計算得到的消息認證碼，從而完成雙向認證。

上述消息認證碼使用的密鑰滿足:

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

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

3 安全協議的形式化驗證

3．1 節點位置固定的安全驗證

3．1．1 協議誠信實體建模

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

圖2 認證協議發起方A的狀態轉換圖

圖3 認證協議響應方B的狀態轉換圖

值得注意的是，協議發起方A在執行認證協議過程中可能會移動節點位置，同樣B在認證協議執行過程中也可能會移動節點位置。

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

通過自定義函數cal_distance計算兩個節點間的歐拉距離。

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

同時定義三個全局消息通道實現協議描述中的三輪消息的傳輸:

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

節點的公鑰和私鑰都基于節點的ID及其位置信息，私鑰僅為對應的節點所私有，公鑰則可被其他節點通過其位置信息和ID計算得到。

3．1．2 入侵者節點建模

根據Dolev-Yao模型[16]，入侵者節點具有如下攻擊能力:

(1)能夠截獲協議發起方A與協議響應方B之間通信的所有消息。

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

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

(4)入侵者可冒充A或B的ID發送消息，例如可冒充A發起認證協議。

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

入侵者的Promela描述較誠實實體A與B復雜得多，下面給出抽象的Promela關鍵代碼:

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

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

3．1．3 協議性質描述

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

文獻[17]給出了對認證協議執行模型檢測的一般方法。鑒于無線傳感器網絡的特殊性，本文對Promela擴展定義如下變量:

bool req_a=0，當協議發起者(A)開始廣播認證請求時置1;

bool req_b=0，當協議響應者(B)收到A發出的廣播請求時置1;

bool ack_1_b=0，當B向A發送消息2時置1;

bool ack_1_a=0，當A收到B發送的消息2并認證通過時置1;

bool ack_2_a=0，當A向B發送消息3時置1;

bool ack_2_b=0，當B收到消息3并驗證通過時置1;

bool authenticated=0，當以上六個值都為1時置1，即表示A與B完成雙向認證。

bool not_neighbor=0，當A與B兩節點距離超過射頻范圍時置1。

利用以上變量構造LTL公式如下:

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

3．1．4 協議分析結果

將協議實體的Promela模型與上述LTL性質描述公式導入到SPIN中執行模型檢測。結果顯示G1，G2，G4都滿足，在檢驗G3時發現一條反例，反例路徑如圖4所示。

圖4 SPIN驗證性質G3時產生的反例路徑

反例路徑表明當節點A在發送消息1后若移動了位置，再發送認證請求時就會導致消息2始終無法通過認證，從而使A的合法鄰居節點B始終無法與A完成雙向認證。結合SPIN反例分析原始協議，容易找出導致認證失敗的原因。因為若節點A移動位置，即假設lA改變為lA，但執行認證協議時節點A擁有的依然是基于lA的ID私鑰ldA，即沒有基于lA的ID私鑰ldA，因此即使A節點移動后仍處在B節點的鄰居位置范圍內，也將無法通過B的安全認證。

3．2 節點位置移動的安全驗證

為使節點能在一定范圍內移動而不影響協議的認證性，需將節點私鑰和公鑰的計算與節點固定的具體位置信息無關，為此可提出如下改進方案:

假設某個數據網關管轄的簇中心位置為L0，簇內節點的合法活動范圍半徑為R0，則簇L0內節點i的標識可由L0‖IDi唯一確定，在對節點i的密鑰管理過程中我們可通過L0‖IDi計算節點的私鑰和公鑰，從而使節點私鑰和公鑰計算不依賴于節點的固定位置，以便使節點i可在簇L0的合法活動范圍內自由移動。

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

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

圖5 SPIN驗證性質G4時的反例路徑

根據SPIN產生的反例圖，不難給出協議可能面臨的一個具體過程描述如下:

(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)

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

4 基于位置的WSN安全協議改進

4．1 方案描述

為克服中間人攻擊，可采用時間戳代替原協議中的隨機數。當然，這里假設WSN擁有一種穩定可靠的時間同步機制，作為時間戳方案的基本保障。改進后的鄰居節點安全認證協議描述如下:

(1)A→＊:IDA

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

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

4．2 安全驗證

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

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

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

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

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

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

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

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

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

5 結論

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

[1]陳鐵明，白素剛，蔡家楣．TinyIBE:面向無線傳感器網絡的身份公鑰加密系統[J]．傳感技術學報，2009，22(8):1193－1197．

[2]陳鐵明，葛亮，蔡家楣，等．TinyTCSec:一種新的輕量級無線傳感器網絡鏈路加密協議[J]．傳感技術學報，2011，24(2):275－282．

[3]陳鐵明，江頡，王小號，等．一種改進的基于位置的攻擊容忍WSN 安全方案[J]．傳感技術學報，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，Fernando 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，Fruth 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的無線傳感網絡安全協議建模與分析[J]．計算機科學，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]林惠民，張文輝．模型檢測:理論、方法與應用[J]．電子學報，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/．