基于PAT的WSNs安全分簇協議建模與驗證

王麗丹　楊紅麗

摘 要：在目前協議安全問題日益突出的情況下，針對無線傳感器網絡中典型的分簇協議LEACH進行安全性改進的版本也越來越多，但這些版本是否真正安全并不確定。基于形式化建模的思想，以LEACH的安全協議版本ORLEACH協議為例，分別建立簇頭節點、簇成員節點、監控節點以及攻擊節點的CSP模型，并使用模型檢查工具PAT對其進行驗證，分析在攻擊節點存在的情況下，協議是否能夠滿足網絡的安全需求。驗證結果表明，盡管ORLEACH協議中加入了安全機制，但是協議仍然不能抵擋某些攻擊行為的發生。

關鍵詞：安全協議；無線傳感器網絡；CSP；模型檢查；PAT

DOI：10.11907/rjdk.171438

中圖分類號：TP309 文獻標識碼：A 文章編號：1672-7800（2017）009-0177-04

Abstract：Under the condition of the protocol security problem increasingly， aiming at the typical cluster-based protocols in WSNs security improvement in the LEACH is also more and more， but these agreements whether safety is uncertain. In this paper， based on the idea of formal modeling， to the safety of the LEACH protocol version ORLEACH as an example， respectively set up the cluster-head nodes， the cluster member nodes， and attack nodes and the monitoring node of CSP model， and using the model checking tool PAT for its verification， analysis of the presence of node， the attack protocol can satisfy the security requirements of the network. Verification results show that although ORLEACH protocol to join the security mechanism， but the agreement still not strong enough to resist some attacks from happening.

Key Words：cluster； security protocol； CSP； model checking； PAT

0 引言

無線傳感器網絡（WSNs，Wireless Sensor Networks）由大量廉價的微型傳感器節點組成，這些傳感器節點自主分布，隨機部署，用來檢測一些物理信息，如溫度、濕度、壓力等[1]。由于WSNs無線、自組織等特性，其應用十分廣泛。但是在軍事戰場或小區安防等應用場景中，WSNs涉及的數據必須具有極高的機密性。因此，如何保障通信安全已成為近年來的研究熱點之一。其要解決的主要問題是重新設計安全的通信協議，安全協議是指在通信協議中加入必要的加密原語，通過使用適當的密鑰、隨機數、散列函數等機制將消息進行加密。

針對安全需求，現階段已提出許多經典的適用于WSNs 的安全協議，如Tiny Sec[2]、LEAP[3]（Loca-lized Encryption and Authentication Protocol）、SPINS（Security Protocols for Sensor Networks）[4]等。安全協議投入實際應用場景之前，都必須進行分析驗證以保障其安全性。模型檢查在對協議的安全性分析上已取得巨大成就，其基本思想是使用有限狀態機描述待驗證的系統，使用線性時態邏輯公式描述待驗證的性質。模型檢查工具通過遍歷有限狀態機的狀態空間，來檢驗系統是否具有時態邏輯公式描述的性質，如果不滿足，則給出反例。文獻[5]對LEAP協議進行建模和分析，創建了4種場景下的模型：單跳共享密鑰對、多跳共享密鑰對、分組密鑰對以及μTESLA。通過分析該協議下節點的通信過程，發現了不同場景中存在的攻擊。文獻[6]借助PAT[10]對使用控制模型UCON 進行建模驗證，首先建立了UCON核模型和組合進程的TCSP#模型，實現了對復雜并發會話、時間控制與非確定性的形式化規約，從而使組合進程的可達空間即為所求空間。最后，提出了基于可達空間的UCON安全性分析方法，以及基于進程代數等價的控制規則沖突性分析方法。文獻[7]使用PAT工具對智能家居平臺進行特性模擬，包括智能家居平臺的組成部分，根據其功能、結構及通信方法，結合平臺實際應用中的性質，實現對智能家居平臺各模塊及通信的形式化規約。針對智能家居的相關特性，使用形式化語言進行描述與驗證。

近場通信（NFC）是短距離無線通信技術，以支持大范圍的智能設備應用，例如支付和票務。由于中繼攻擊可以很容易地繞過NFC要求的短距離進行通信，文獻[8]提出了一個通用框架，使用形式分析和模型檢查作為驗證手段，防止NFC協議中的中繼攻擊。使用PRISM模型檢查器建立了一個連續時間馬爾可夫鏈（CTMC）模型。然后結合NFC協議規范與攻擊者的特點，生成中繼攻擊模型，通過驗證結果分析了應對方案。

綜上所述，模型檢測技術已經發展多年，檢測工具多種多樣。本文以通信順序進程CSP[9]為輸入模型，線性時態邏輯LTL（Linear Temporal Logic）公式描述協議的安全屬性，首次提出使用模型檢查工具PAT驗證WSNs分簇協議的安全性。以典型的分簇協議LEACH[11]為基礎，針對LEACH安全協議版本中安全性較高的ORLEACH[12]協議為研究對象，分別建立簇頭節點、簇成員節點、監控節點，以及攻擊節點的模型，驗證在攻擊節點存在的情況下，協議是否能夠抵御住攻擊節點的攻擊。endprint

1 基于LEACH的安全協議

1.1 LEACH協議

LEACH協議是一種基于簇的路由協議，是無線傳感器網絡中最早提出的、最經典的層次式路由協議。其基本思想是以循環的方式隨機選擇簇頭，其余節點選擇加入到不同的簇中，然后進行數據收集。LEACH協議拓撲結構如圖1所示，每個簇中選舉出一個簇頭，負責將本簇成員收集的數據進行整合并發送給基站。LEACH協議最大的優勢是自組織形成簇，網絡中的節點輪流做簇頭，且簇內成員節點只負責與本簇簇頭通信，不直接與基站通信，因此節點的能耗非常低，延長了整個網絡的生命周期。

1.2 ORLEACH協議

為了讓協議本身能夠處理來自網絡內部的攻擊，Somia Sahraoui等提出適用于分簇結構的入侵檢測系統，為每個簇設立監控節點。監控節點的選擇基于動態，并且具有隨機性。監控節點除了監控本簇簇頭的行為外，還具有感知數據和通信的能力。每次建簇，選擇的監控節點也隨之不同。

Somia Sahraoui等提出將入侵檢測系統應用于RLEACH協議的ORLEACH協議，與RLEACH協議相比，ORLEACH協議中多了一類監控節點，整個協議的運行過程增加了一個入侵檢測和警報階段。在節點初始化時，每個節點都分配一個黑名單。協議的第一個階段與RLEACH相同，首先是共享密鑰發現階段，所有節點建立安全鏈接。第二個階段是簇建立階段，在此過程中，成員節點會對收到的簇頭身份進行校驗，看其是否在自己的黑名單中，若存在，則孤立該節點，否則就發送加入請求，同樣，簇頭也會對申請加入的節點身份進行識別校驗，若在自己的黑名單中，則孤立該節點。簇建立完成后，在每個簇內的所有非簇頭節點中隨機選擇若干監控節點，每一輪的建簇過程都將重新進行一次監控節點的選擇。第三個階段是數據收集和入侵檢測階段，監控節點監聽簇頭行為，若簇頭在一段時間內沒有發送任何消息，則視該簇頭為攻擊節點，并將其加入自己的黑名單，并廣播出去，被檢測出的攻擊節點在以后的建簇過程中，就會被孤立，從而提高網絡安全，增加傳輸效率；若監控的簇頭節點無異常，則簇頭節點將收集到的數據進行融合并發送給基站。

2 ORLEACH協議建模

由于ORLEACH協議共享密鑰階段建立在節點部署之前，為了簡化模型，只模擬節點已部署在特定環境，且簇頭已經選出的情況下，協議中節點之間發生的信息交換過程。由于篇幅所限，本文只對簇頭節點、監控節點和攻擊節點模型進行詳細描述。

首先需要聲明的全局信息包括：協議參與者實體及相關常量、信道及節點其它相關信息。

（1）聲明枚舉參與者相關常量。enum{CH，Node，Mon，BS，I，everyone，K} 其中，CH為簇頭節點標識，Node為普通節點標識，Mon為監控節點標識，BS為基站節點標識，I為攻擊節點標識，everyone為廣播通信時接收者標識，K為密鑰表示。

（2）聲明信道。

channel ca 0；

channel cb 0；

channel cc 0；

其中，信道ca用于傳送消息1，消息類型為x1、x2；cb用于傳送消息2、消息3，消息類型為x1、x2、x3；信道cd用于傳送消息4和消息5，消息類型為x1、x2、x3、{x4}K。

2.1 簇頭節點模型

簇頭節點狀態轉化過程如圖2所示。首先簇頭節點自動從Idle狀態遷移到Init狀態，然后廣播發送建簇消息adv，其中包括自己的身份CHid等其它信息，隨后遷移到Wait狀態等待響應；收到其余節點發送的申請入簇消息join_req后，遷移到Check狀態，檢測該節點是否在自己的黑名單中，若該節點在自己的黑名單中，則不理會該節點，檢測其余節點，若此節點符合要求，則接受其請求，并向其分配時間片，通知成員節點發送收集的數據（這些數據使用成員節點與簇頭節點共享的密鑰加密），進入Wait狀態等待接收數據消息；最后簇頭節點將這些數據加以整合，并且使用與基站共享的初始密鑰將此消息進行加密，發送給基站，進入Commit狀態完成一次協議的執行。

2.2 監控節點模型

監控節點既執行普通成員節點收集數據并傳遞數據的工作，又執行監控簇頭行為的功能。當簇建立完成后，每個簇中隨機安全地選出若干各簇頭節點，在與簇頭通信過程中，同時監控簇頭行為，若一段時間內，簇頭沒有任何消息發送出來，則視該簇頭節點為惡意節點，并更新自己的黑名單，然后生成警報信息。若黑名單的長度未達到事先設定好的閾值，則監控節點只廣播此節點的id；若黑名單長度達到閾值，則監控節點將整個黑名單直接發送給基站。當監控節點廣播警報信息時，通信范圍內的節點收到后，首先查看自己的黑名單內是否有此節點，若沒有，則更新。在以后的建簇過程中，若發現簇頭是自己黑名單中的節點時，便不予理會，從而孤立這些惡意節點，提高網絡安全。

首先為監控節點設立一個標志位nomessage，初始為false。當攻擊節點實施黑洞攻擊，即收到成員節點的數據但沒有向外發送時，將該標志位變為true，然后更新黑名單，并且發送警報。建立的監控節點模型如下：

1.Monitor（） = ca？mv.clu->

2.cb！join.mon.clu ->

3.if （nomessage） // 如果nomessage值為真，簇頭節點clu實施了黑洞攻擊

4.{

5.mn{BL_Monitor.Add（clu）} -> //加入自己的黑名單

6.//黑名單長度小于閾值，廣播此節點；黑名單長度達到閾值，將黑名單發送給基站

7.[BL_Monitor.Length（）

8.[BL_Monitor.Length（）==Threshold] ca！attack.BL_Monitor.BSendprint

9.-> Skip

10.}；

2.3 攻擊節點建模

由于RLEACH和ORLEACH協議都采用了隨機密鑰對機制，每個節點在部署之前都隨機分配了若干個密鑰，并且在建簇時，成員節點首先根據是否與簇頭節點有共享密鑰選擇加入某一簇中。因此，外部攻擊節點若想加入到網絡中，須破解多個節點獲取密鑰信息，從而會大大消耗自身的資源，因而能夠有效防止外部攻擊。但是對于來自網絡內部的攻擊，即節點此時已在網絡內部，被攻擊者捕獲變為損壞節點，這些節點了解自身與其余節點的密鑰信息，從而可以實施更嚴重的攻擊行為。加入入侵檢測系統后的ORLEACH協議，能夠及時檢測出損壞節點并進行及時隔離處理，減小損失。該協議能夠有效抵御黑洞攻擊、選擇性轉發攻擊以及Sinkhole攻擊。

對于分簇協議而言，因其功能、地位的不平等性，簇頭節點無疑是整個網絡中最為關鍵的一環。攻擊者一旦成為簇頭，將對網絡造成危害，諸如，破壞消息的機密性、完整性，可以向基站發送偽造、篡改的消息，毀壞基站；可以連續廣播建簇消息，促使周圍節點持續向其發送數據，快速消耗周圍節點的能量，降低整個網絡的數據傳輸效率；等等一系列惡意行為。因此，對于分簇協議，保證其簇頭的安全性是重中之重。本文針對損壞的簇頭節點（惡意節點），建立黑洞攻擊及選擇性轉發攻擊兩種行為模型，驗證ORLEACH協議對兩種攻擊的抵御能力。建立模型如下：

1.PI（）=ca？x1.from.to_everyone ->

2.InterceptCa{

3.m1=x1；

4.m2=from；

5.NodeI.addKnow（……）；

6.NodeI.addKnow（……）；

7.}->PI（）[]

8.cb？x2.from.to ->

9.InterceptCb{

10. ……

11.NodeI.addKnow（……）；

12.}->PI（）[]

13.cc？x3.from.to ->

14.InterceptCc{

15.……

16.NodeI.addKnow（……）；

17.}->PI（）[]

18.……

19.ca！x1.from.to ->PI（） []

20.cb！x2.from.to ->PI（） []

21.……

如數據塊InterceptCa、InterceptCb等為攻擊者的行為，通過竊聽信道中的消息，并使用addKnow（）函數存儲到自己的知識集中，然后從知識集中隨意組合消息內容發送到信道中，如19、20行，攻擊者將隨意組合收集到的信息，然后重放到信道中。

2.4 驗證

完整性和黑洞攻擊的檢測均可用可達性進行分析，即在模型的所有路徑中，存在一條路徑的某個狀態滿足要驗證的條件。

協議的安全性包括：

（1）黑洞攻擊檢測。G1：#define goal1（checked==true）；checked初始狀態為false，當實行黑洞攻擊的簇頭節點被檢測出，再參與建簇的行為后，可被隔離。

（2）完整性檢測。G2：#define goal2 tempered==true）；tempered初始狀態為false，當攻擊節點實行選擇性轉發時，值為true。

如果G1斷言通過，系統狀態可以到達goal1，表示本次的簇頭節點是惡意節點，該節點在之前的建簇過程中成為簇頭，并實施了黑洞攻擊，卻被監控節點檢測出來，并將此警報信息廣播給周圍鄰居節點。成員節點接收到此消息，更新自己的黑名單，在本輪建簇過程中，識別出聲明建簇的節點為惡意節點。反之，若不能到達goal1，表示該系統能夠抵御黑洞攻擊。PAT驗證通過，能夠檢測出實施黑洞攻擊的節點，并將其加入黑名單中孤立。

若第G2條斷言語句通過，系統狀態可以到達goal2，表示損壞節點成為簇頭，并實施了選擇性轉發攻擊，將篡改的數據發送給了基站。這條性質說明對于損壞節點實施的選擇性轉發攻擊，監控節點不能檢測出。因此，該系統不能抵御內部節點實施的選擇性轉發攻擊。PAT工具給出一條見證跡時序圖（見圖1），粗線表示攻擊者的行為，在網絡正常通信過程中，攻擊者通過竊聽信道中的信息，獲取成員節點發送給簇頭節點的加密數據，并進行篡改（tamper），然后將這些篡改的數據發送到信道中，簇頭節點接收后無法分辨消息的完整性，在進行數據融合時，便將這些篡改后的消息一同融合并發送到基站。

（3）認證性。首先定義如下變量：

#define iniRunningCN （IniRunningCN==true）； 當簇頭開始廣播建簇時，IniRunningCN置為true；

#define iniCommitCN （IniCommitCN==true）；當簇頭完成收到成員節點的數據后，InitCommit置為true；

#define resRunningCN （ResRunningCN==true）；當成員節點收到簇頭節點的廣播消息時，ResCommit置為true；

#define resCommitCN （ResCommitCN==true）；當成員節點收到簇頭節點的時間片標志時，ResCommit置為true。

認證性。保證接收者接收到的消息是聲明的節點發送的。使用LTL描述性質：

G3：[]（（[]！iniCommitCN）‖（！iniCommitCN U resRunningCN））；endprint

G4：[]（（[]！resCommitCN）‖（！resCommitCN U iniRunningCN））；

若G3不滿足，說明有攻擊者竊取簇頭發送的消息，并冒充成員節點Nid與簇頭節點CHid通信；若G4不滿足，說明有攻擊者冒充簇頭CHid與成員節點Nid通信。

在驗證時，出現問題，反例路徑描述如下：

（1）CH→*：IDCH，adv

（2）I →*：IDCH，adv

（3）Node →I（CH）：IDNode，IDCH，join_req

（4）I（Node）→CH：IDNode，IDCH，join_req

（5）I（CH）→*：TDMA

（6）Node→I（CH）：IDNode，Ekcn（data）

（7）Mon→*：alert_mess，IDCH

結果表明，攻擊者I作為簇頭節點CH與成員節點Node的中間人，攻擊者可以在網絡中隨意重放建簇及其它消息，迫使雙方進行無限制的通信，達到快速消耗節點能源的目的。由于ORLEACH協議中加入監控機制，當監控節點監控到簇頭不正常行為時，廣播警報消息，使該簇頭節點被孤立。

3 結語

本文對加入監控機制和密鑰管理機制的分簇安全協議ORLEACH使用模型檢測工具PAT建立簡易的CSP模型，并進行了安全性驗證，發現對于來自網絡內部的攻擊，該協議能夠及時檢測出實施黑洞攻擊的損壞節點，并將其孤立，提高了整個網絡的數據傳輸率。然而對于攻擊節點實行的篡改攻擊數據完整性的問題，該協議不能保證檢測出。對于不能加入到網絡中的外部攻擊節點也可以竊聽到簇頭的建簇消息（廣播的建簇消息沒有加密），從而獲取簇頭的身份id，并可以在網絡中無限制地重放此消息，從而消耗內部節點的能量。因此，將針對該協議的這兩個缺點作深入研究，并對協議模型進行繼續細化，同時對PAT工具建立適應于分簇協議的建模框架。

參考文獻：

[1] 孫利民，李建中，陳渝，等.無線傳感器網絡[M].北京：清華大學出版社，2005.

[2] KARLOF C， SASTRY N， WAGNER D. TinySec：a link layer security architecture for wireless sensor networks[C]. International Conference on Embedded Networked Sensor Systems， SENSYS 2004， Baltimore， Md， USA，2004：162-175.

[3] ZHU S， SETIA S， JAJODIA S. LEAP+： efficient security mechanisms for large-scale distributed sensor networks[J]. Acm Transactions on Sensor Networks，2004（4）：500-528.

[4] PERRIG A. SPINS：security protocols for sensor networks[J]. Wireless Networks，2002，8（5）：521-534.

[5] VERMA R M， BASILE B E. Modeling and analysis of LEAP， a key management protocol for wireless sensor networks[C]. IEEE Communications Society Conference on Sensing and Communication in Wireless Networks，2013：23-25.

[6] 周從華，陳偉鶴，劉志鋒.基于PAT的使用控制模型的形式化規約與安全性分析[J].網絡與信息安全學報，2016，2（3）：52-67.

[7] 馬俊偉.基于PAT工具的智能家居平臺形式化分析與檢驗[D].太原：太原理工大學，2016.

[8] ALEXIOU N， BASAGIANNIS S， PETRIDOU S. Security analysis of NFC relay attacks using probabilistic model checking[C]. Wireless Communications and Mobile Computing Conference （IWCMC），2014 International. IEEE，2014：524-529.

[9] 霍爾.通信順序進程[M].北京：北京大學出版社，1990.

[10] PAT：process analysis toolkit[EB/OL].http：//pat.comp.nus.edu.sg/.

[11] HEINZELMAN W R， CHANDRAKASAN A， BALAKRISHNAN H. Energy-efficient communication protocol for wireless microsensor networks[C]. Hawaii International Conference on System Sciences，2000.

[12] SAHRAOUI S， BOUAM S. Secure routing optimization in hierarchical cluster-based wireless sensor networks[J]. International Journal of Communication Networks & Information Security，2013，5（3）：178-185.

（責任編輯：孫 娟）endprint