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

王麗丹　楊紅麗

摘 要：在目前協(xié)議安全問題日益突出的情況下，針對無線傳感器網(wǎng)絡中典型的分簇協(xié)議LEACH進行安全性改進的版本也越來越多，但這些版本是否真正安全并不確定?；谛问交５乃枷耄訪EACH的安全協(xié)議版本ORLEACH協(xié)議為例，分別建立簇頭節(jié)點、簇成員節(jié)點、監(jiān)控節(jié)點以及攻擊節(jié)點的CSP模型，并使用模型檢查工具PAT對其進行驗證，分析在攻擊節(jié)點存在的情況下，協(xié)議是否能夠滿足網(wǎng)絡的安全需求。驗證結果表明，盡管ORLEACH協(xié)議中加入了安全機制，但是協(xié)議仍然不能抵擋某些攻擊行為的發(fā)生。

關鍵詞：安全協(xié)議；無線傳感器網(wǎng)絡；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 引言

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

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

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

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

1 基于LEACH的安全協(xié)議

1.1 LEACH協(xié)議

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

1.2 ORLEACH協(xié)議

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

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

2 ORLEACH協(xié)議建模

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

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

（1）聲明枚舉參與者相關常量。enum{CH，Node，Mon，BS，I，everyone，K} 其中，CH為簇頭節(jié)點標識，Node為普通節(jié)點標識，Mon為監(jiān)控節(jié)點標識，BS為基站節(jié)點標識，I為攻擊節(jié)點標識，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 簇頭節(jié)點模型

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

2.2 監(jiān)控節(jié)點模型

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

首先為監(jiān)控節(jié)點設立一個標志位nomessage，初始為false。當攻擊節(jié)點實施黑洞攻擊，即收到成員節(jié)點的數(shù)據(jù)但沒有向外發(fā)送時，將該標志位變?yōu)閠rue，然后更新黑名單，并且發(fā)送警報。建立的監(jiān)控節(jié)點模型如下：

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

2.cb！join.mon.clu ->

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

4.{

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

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

7.[BL_Monitor.Length（）

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

9.-> Skip

10.}；

2.3 攻擊節(jié)點建模

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

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

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.……

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

2.4 驗證

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

協(xié)議的安全性包括：

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

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

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

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

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

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

#define iniCommitCN （IniCommitCN==true）；當簇頭完成收到成員節(jié)點的數(shù)據(jù)后，InitCommit置為true；

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

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

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

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

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

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

在驗證時，出現(xiàn)問題，反例路徑描述如下：

（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作為簇頭節(jié)點CH與成員節(jié)點Node的中間人，攻擊者可以在網(wǎng)絡中隨意重放建簇及其它消息，迫使雙方進行無限制的通信，達到快速消耗節(jié)點能源的目的。由于ORLEACH協(xié)議中加入監(jiān)控機制，當監(jiān)控節(jié)點監(jiān)控到簇頭不正常行為時，廣播警報消息，使該簇頭節(jié)點被孤立。

3 結語

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

參考文獻：

[1] 孫利民，李建中，陳渝，等.無線傳感器網(wǎng)絡[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的使用控制模型的形式化規(guī)約與安全性分析[J].網(wǎng)絡與信息安全學報，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