王麗丹 楊紅麗
摘 要:在目前協(xié)議安全問(wèn)題日益突出的情況下,針對(duì)無(wú)線傳感器網(wǎng)絡(luò)中典型的分簇協(xié)議LEACH進(jìn)行安全性改進(jìn)的版本也越來(lái)越多,但這些版本是否真正安全并不確定?;谛问交5乃枷?,以LEACH的安全協(xié)議版本ORLEACH協(xié)議為例,分別建立簇頭節(jié)點(diǎn)、簇成員節(jié)點(diǎn)、監(jiān)控節(jié)點(diǎn)以及攻擊節(jié)點(diǎn)的CSP模型,并使用模型檢查工具PAT對(duì)其進(jìn)行驗(yàn)證,分析在攻擊節(jié)點(diǎn)存在的情況下,協(xié)議是否能夠滿足網(wǎng)絡(luò)的安全需求。驗(yàn)證結(jié)果表明,盡管ORLEACH協(xié)議中加入了安全機(jī)制,但是協(xié)議仍然不能抵擋某些攻擊行為的發(fā)生。
關(guān)鍵詞:安全協(xié)議;無(wú)線傳感器網(wǎng)絡(luò);CSP;模型檢查;PAT
DOI:10.11907/rjdk.171438
中圖分類(lèi)號(hào):TP309 文獻(xiàn)標(biāo)識(shí)碼:A 文章編號(hào):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ú)線傳感器網(wǎng)絡(luò)(WSNs,Wireless Sensor Networks)由大量廉價(jià)的微型傳感器節(jié)點(diǎn)組成,這些傳感器節(jié)點(diǎn)自主分布,隨機(jī)部署,用來(lái)檢測(cè)一些物理信息,如溫度、濕度、壓力等[1]。由于WSNs無(wú)線、自組織等特性,其應(yīng)用十分廣泛。但是在軍事戰(zhàn)場(chǎng)或小區(qū)安防等應(yīng)用場(chǎng)景中,WSNs涉及的數(shù)據(jù)必須具有極高的機(jī)密性。因此,如何保障通信安全已成為近年來(lái)的研究熱點(diǎn)之一。其要解決的主要問(wèn)題是重新設(shè)計(jì)安全的通信協(xié)議,安全協(xié)議是指在通信協(xié)議中加入必要的加密原語(yǔ),通過(guò)使用適當(dāng)?shù)拿荑€、隨機(jī)數(shù)、散列函數(shù)等機(jī)制將消息進(jìn)行加密。
針對(duì)安全需求,現(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é)議投入實(shí)際應(yīng)用場(chǎng)景之前,都必須進(jìn)行分析驗(yàn)證以保障其安全性。模型檢查在對(duì)協(xié)議的安全性分析上已取得巨大成就,其基本思想是使用有限狀態(tài)機(jī)描述待驗(yàn)證的系統(tǒng),使用線性時(shí)態(tài)邏輯公式描述待驗(yàn)證的性質(zhì)。模型檢查工具通過(guò)遍歷有限狀態(tài)機(jī)的狀態(tài)空間,來(lái)檢驗(yàn)系統(tǒng)是否具有時(shí)態(tài)邏輯公式描述的性質(zhì),如果不滿足,則給出反例。文獻(xiàn)[5]對(duì)LEAP協(xié)議進(jìn)行建模和分析,創(chuàng)建了4種場(chǎng)景下的模型:?jiǎn)翁蚕砻荑€對(duì)、多跳共享密鑰對(duì)、分組密鑰對(duì)以及μTESLA。通過(guò)分析該協(xié)議下節(jié)點(diǎn)的通信過(guò)程,發(fā)現(xiàn)了不同場(chǎng)景中存在的攻擊。文獻(xiàn)[6]借助PAT[10]對(duì)使用控制模型UCON 進(jìn)行建模驗(yàn)證,首先建立了UCON核模型和組合進(jìn)程的TCSP#模型,實(shí)現(xiàn)了對(duì)復(fù)雜并發(fā)會(huì)話、時(shí)間控制與非確定性的形式化規(guī)約,從而使組合進(jìn)程的可達(dá)空間即為所求空間。最后,提出了基于可達(dá)空間的UCON安全性分析方法,以及基于進(jìn)程代數(shù)等價(jià)的控制規(guī)則沖突性分析方法。文獻(xiàn)[7]使用PAT工具對(duì)智能家居平臺(tái)進(jìn)行特性模擬,包括智能家居平臺(tái)的組成部分,根據(jù)其功能、結(jié)構(gòu)及通信方法,結(jié)合平臺(tái)實(shí)際應(yīng)用中的性質(zhì),實(shí)現(xiàn)對(duì)智能家居平臺(tái)各模塊及通信的形式化規(guī)約。針對(duì)智能家居的相關(guān)特性,使用形式化語(yǔ)言進(jìn)行描述與驗(yàn)證。
近場(chǎng)通信(NFC)是短距離無(wú)線通信技術(shù),以支持大范圍的智能設(shè)備應(yīng)用,例如支付和票務(wù)。由于中繼攻擊可以很容易地繞過(guò)NFC要求的短距離進(jìn)行通信,文獻(xiàn)[8]提出了一個(gè)通用框架,使用形式分析和模型檢查作為驗(yàn)證手段,防止NFC協(xié)議中的中繼攻擊。使用PRISM模型檢查器建立了一個(gè)連續(xù)時(shí)間馬爾可夫鏈(CTMC)模型。然后結(jié)合NFC協(xié)議規(guī)范與攻擊者的特點(diǎn),生成中繼攻擊模型,通過(guò)驗(yàn)證結(jié)果分析了應(yīng)對(duì)方案。
綜上所述,模型檢測(cè)技術(shù)已經(jīng)發(fā)展多年,檢測(cè)工具多種多樣。本文以通信順序進(jìn)程CSP[9]為輸入模型,線性時(shí)態(tài)邏輯LTL(Linear Temporal Logic)公式描述協(xié)議的安全屬性,首次提出使用模型檢查工具PAT驗(yàn)證WSNs分簇協(xié)議的安全性。以典型的分簇協(xié)議LEACH[11]為基礎(chǔ),針對(duì)LEACH安全協(xié)議版本中安全性較高的ORLEACH[12]協(xié)議為研究對(duì)象,分別建立簇頭節(jié)點(diǎn)、簇成員節(jié)點(diǎn)、監(jiān)控節(jié)點(diǎn),以及攻擊節(jié)點(diǎn)的模型,驗(yàn)證在攻擊節(jié)點(diǎn)存在的情況下,協(xié)議是否能夠抵御住攻擊節(jié)點(diǎn)的攻擊。endprint
1 基于LEACH的安全協(xié)議
1.1 LEACH協(xié)議
LEACH協(xié)議是一種基于簇的路由協(xié)議,是無(wú)線傳感器網(wǎng)絡(luò)中最早提出的、最經(jīng)典的層次式路由協(xié)議。其基本思想是以循環(huán)的方式隨機(jī)選擇簇頭,其余節(jié)點(diǎn)選擇加入到不同的簇中,然后進(jìn)行數(shù)據(jù)收集。LEACH協(xié)議拓?fù)浣Y(jié)構(gòu)如圖1所示,每個(gè)簇中選舉出一個(gè)簇頭,負(fù)責(zé)將本簇成員收集的數(shù)據(jù)進(jìn)行整合并發(fā)送給基站。LEACH協(xié)議最大的優(yōu)勢(shì)是自組織形成簇,網(wǎng)絡(luò)中的節(jié)點(diǎn)輪流做簇頭,且簇內(nèi)成員節(jié)點(diǎn)只負(fù)責(zé)與本簇簇頭通信,不直接與基站通信,因此節(jié)點(diǎn)的能耗非常低,延長(zhǎng)了整個(gè)網(wǎng)絡(luò)的生命周期。
1.2 ORLEACH協(xié)議
為了讓協(xié)議本身能夠處理來(lái)自網(wǎng)絡(luò)內(nèi)部的攻擊,Somia Sahraoui等提出適用于分簇結(jié)構(gòu)的入侵檢測(cè)系統(tǒng),為每個(gè)簇設(shè)立監(jiān)控節(jié)點(diǎn)。監(jiān)控節(jié)點(diǎn)的選擇基于動(dòng)態(tài),并且具有隨機(jī)性。監(jiān)控節(jié)點(diǎn)除了監(jiān)控本簇簇頭的行為外,還具有感知數(shù)據(jù)和通信的能力。每次建簇,選擇的監(jiān)控節(jié)點(diǎn)也隨之不同。
Somia Sahraoui等提出將入侵檢測(cè)系統(tǒng)應(yīng)用于RLEACH協(xié)議的ORLEACH協(xié)議,與RLEACH協(xié)議相比,ORLEACH協(xié)議中多了一類(lèi)監(jiān)控節(jié)點(diǎn),整個(gè)協(xié)議的運(yùn)行過(guò)程增加了一個(gè)入侵檢測(cè)和警報(bào)階段。在節(jié)點(diǎn)初始化時(shí),每個(gè)節(jié)點(diǎn)都分配一個(gè)黑名單。協(xié)議的第一個(gè)階段與RLEACH相同,首先是共享密鑰發(fā)現(xiàn)階段,所有節(jié)點(diǎn)建立安全鏈接。第二個(gè)階段是簇建立階段,在此過(guò)程中,成員節(jié)點(diǎn)會(huì)對(duì)收到的簇頭身份進(jìn)行校驗(yàn),看其是否在自己的黑名單中,若存在,則孤立該節(jié)點(diǎn),否則就發(fā)送加入請(qǐng)求,同樣,簇頭也會(huì)對(duì)申請(qǐng)加入的節(jié)點(diǎn)身份進(jìn)行識(shí)別校驗(yàn),若在自己的黑名單中,則孤立該節(jié)點(diǎn)。簇建立完成后,在每個(gè)簇內(nèi)的所有非簇頭節(jié)點(diǎn)中隨機(jī)選擇若干監(jiān)控節(jié)點(diǎn),每一輪的建簇過(guò)程都將重新進(jìn)行一次監(jiān)控節(jié)點(diǎn)的選擇。第三個(gè)階段是數(shù)據(jù)收集和入侵檢測(cè)階段,監(jiān)控節(jié)點(diǎn)監(jiān)聽(tīng)簇頭行為,若簇頭在一段時(shí)間內(nèi)沒(méi)有發(fā)送任何消息,則視該簇頭為攻擊節(jié)點(diǎn),并將其加入自己的黑名單,并廣播出去,被檢測(cè)出的攻擊節(jié)點(diǎn)在以后的建簇過(guò)程中,就會(huì)被孤立,從而提高網(wǎng)絡(luò)安全,增加傳輸效率;若監(jiān)控的簇頭節(jié)點(diǎn)無(wú)異常,則簇頭節(jié)點(diǎn)將收集到的數(shù)據(jù)進(jìn)行融合并發(fā)送給基站。
2 ORLEACH協(xié)議建模
由于ORLEACH協(xié)議共享密鑰階段建立在節(jié)點(diǎn)部署之前,為了簡(jiǎn)化模型,只模擬節(jié)點(diǎn)已部署在特定環(huán)境,且簇頭已經(jīng)選出的情況下,協(xié)議中節(jié)點(diǎn)之間發(fā)生的信息交換過(guò)程。由于篇幅所限,本文只對(duì)簇頭節(jié)點(diǎn)、監(jiān)控節(jié)點(diǎn)和攻擊節(jié)點(diǎn)模型進(jìn)行詳細(xì)描述。
首先需要聲明的全局信息包括:協(xié)議參與者實(shí)體及相關(guān)常量、信道及節(jié)點(diǎn)其它相關(guān)信息。
(1)聲明枚舉參與者相關(guān)常量。enum{CH,Node,Mon,BS,I,everyone,K} 其中,CH為簇頭節(jié)點(diǎn)標(biāo)識(shí),Node為普通節(jié)點(diǎn)標(biāo)識(shí),Mon為監(jiān)控節(jié)點(diǎn)標(biāo)識(shí),BS為基站節(jié)點(diǎn)標(biāo)識(shí),I為攻擊節(jié)點(diǎn)標(biāo)識(shí),everyone為廣播通信時(shí)接收者標(biāo)識(shí),K為密鑰表示。
(2)聲明信道。
channel ca 0;
channel cb 0;
channel cc 0;
其中,信道ca用于傳送消息1,消息類(lèi)型為x1、x2;cb用于傳送消息2、消息3,消息類(lèi)型為x1、x2、x3;信道cd用于傳送消息4和消息5,消息類(lèi)型為x1、x2、x3、{x4}K。
2.1 簇頭節(jié)點(diǎn)模型
簇頭節(jié)點(diǎn)狀態(tài)轉(zhuǎn)化過(guò)程如圖2所示。首先簇頭節(jié)點(diǎn)自動(dòng)從Idle狀態(tài)遷移到Init狀態(tài),然后廣播發(fā)送建簇消息adv,其中包括自己的身份CHid等其它信息,隨后遷移到Wait狀態(tài)等待響應(yīng);收到其余節(jié)點(diǎn)發(fā)送的申請(qǐng)入簇消息join_req后,遷移到Check狀態(tài),檢測(cè)該節(jié)點(diǎn)是否在自己的黑名單中,若該節(jié)點(diǎn)在自己的黑名單中,則不理會(huì)該節(jié)點(diǎn),檢測(cè)其余節(jié)點(diǎn),若此節(jié)點(diǎn)符合要求,則接受其請(qǐng)求,并向其分配時(shí)間片,通知成員節(jié)點(diǎn)發(fā)送收集的數(shù)據(jù)(這些數(shù)據(jù)使用成員節(jié)點(diǎn)與簇頭節(jié)點(diǎn)共享的密鑰加密),進(jìn)入Wait狀態(tài)等待接收數(shù)據(jù)消息;最后簇頭節(jié)點(diǎn)將這些數(shù)據(jù)加以整合,并且使用與基站共享的初始密鑰將此消息進(jìn)行加密,發(fā)送給基站,進(jìn)入Commit狀態(tài)完成一次協(xié)議的執(zhí)行。
2.2 監(jiān)控節(jié)點(diǎn)模型
監(jiān)控節(jié)點(diǎn)既執(zhí)行普通成員節(jié)點(diǎn)收集數(shù)據(jù)并傳遞數(shù)據(jù)的工作,又執(zhí)行監(jiān)控簇頭行為的功能。當(dāng)簇建立完成后,每個(gè)簇中隨機(jī)安全地選出若干各簇頭節(jié)點(diǎn),在與簇頭通信過(guò)程中,同時(shí)監(jiān)控簇頭行為,若一段時(shí)間內(nèi),簇頭沒(méi)有任何消息發(fā)送出來(lái),則視該簇頭節(jié)點(diǎn)為惡意節(jié)點(diǎn),并更新自己的黑名單,然后生成警報(bào)信息。若黑名單的長(zhǎng)度未達(dá)到事先設(shè)定好的閾值,則監(jiān)控節(jié)點(diǎn)只廣播此節(jié)點(diǎn)的id;若黑名單長(zhǎng)度達(dá)到閾值,則監(jiān)控節(jié)點(diǎn)將整個(gè)黑名單直接發(fā)送給基站。當(dāng)監(jiān)控節(jié)點(diǎn)廣播警報(bào)信息時(shí),通信范圍內(nèi)的節(jié)點(diǎn)收到后,首先查看自己的黑名單內(nèi)是否有此節(jié)點(diǎn),若沒(méi)有,則更新。在以后的建簇過(guò)程中,若發(fā)現(xiàn)簇頭是自己黑名單中的節(jié)點(diǎn)時(shí),便不予理會(huì),從而孤立這些惡意節(jié)點(diǎn),提高網(wǎng)絡(luò)安全。
首先為監(jiān)控節(jié)點(diǎn)設(shè)立一個(gè)標(biāo)志位nomessage,初始為false。當(dāng)攻擊節(jié)點(diǎn)實(shí)施黑洞攻擊,即收到成員節(jié)點(diǎn)的數(shù)據(jù)但沒(méi)有向外發(fā)送時(shí),將該標(biāo)志位變?yōu)閠rue,然后更新黑名單,并且發(fā)送警報(bào)。建立的監(jiān)控節(jié)點(diǎn)模型如下:
1.Monitor() = ca?mv.clu->
2.cb!join.mon.clu ->
3.if (nomessage) // 如果nomessage值為真,簇頭節(jié)點(diǎn)clu實(shí)施了黑洞攻擊
4.{
5.mn{BL_Monitor.Add(clu)} -> //加入自己的黑名單
6.//黑名單長(zhǎng)度小于閾值,廣播此節(jié)點(diǎn);黑名單長(zhǎng)度達(dá)到閾值,將黑名單發(fā)送給基站
7.[BL_Monitor.Length()
8.[BL_Monitor.Length()==Threshold] ca!attack.BL_Monitor.BSendprint
9.-> Skip
10.};
2.3 攻擊節(jié)點(diǎn)建模
由于RLEACH和ORLEACH協(xié)議都采用了隨機(jī)密鑰對(duì)機(jī)制,每個(gè)節(jié)點(diǎn)在部署之前都隨機(jī)分配了若干個(gè)密鑰,并且在建簇時(shí),成員節(jié)點(diǎn)首先根據(jù)是否與簇頭節(jié)點(diǎn)有共享密鑰選擇加入某一簇中。因此,外部攻擊節(jié)點(diǎn)若想加入到網(wǎng)絡(luò)中,須破解多個(gè)節(jié)點(diǎn)獲取密鑰信息,從而會(huì)大大消耗自身的資源,因而能夠有效防止外部攻擊。但是對(duì)于來(lái)自網(wǎng)絡(luò)內(nèi)部的攻擊,即節(jié)點(diǎn)此時(shí)已在網(wǎng)絡(luò)內(nèi)部,被攻擊者捕獲變?yōu)閾p壞節(jié)點(diǎn),這些節(jié)點(diǎn)了解自身與其余節(jié)點(diǎn)的密鑰信息,從而可以實(shí)施更嚴(yán)重的攻擊行為。加入入侵檢測(cè)系統(tǒng)后的ORLEACH協(xié)議,能夠及時(shí)檢測(cè)出損壞節(jié)點(diǎn)并進(jìn)行及時(shí)隔離處理,減小損失。該協(xié)議能夠有效抵御黑洞攻擊、選擇性轉(zhuǎn)發(fā)攻擊以及Sinkhole攻擊。
對(duì)于分簇協(xié)議而言,因其功能、地位的不平等性,簇頭節(jié)點(diǎn)無(wú)疑是整個(gè)網(wǎng)絡(luò)中最為關(guān)鍵的一環(huán)。攻擊者一旦成為簇頭,將對(duì)網(wǎng)絡(luò)造成危害,諸如,破壞消息的機(jī)密性、完整性,可以向基站發(fā)送偽造、篡改的消息,毀壞基站;可以連續(xù)廣播建簇消息,促使周?chē)?jié)點(diǎn)持續(xù)向其發(fā)送數(shù)據(jù),快速消耗周?chē)?jié)點(diǎn)的能量,降低整個(gè)網(wǎng)絡(luò)的數(shù)據(jù)傳輸效率;等等一系列惡意行為。因此,對(duì)于分簇協(xié)議,保證其簇頭的安全性是重中之重。本文針對(duì)損壞的簇頭節(jié)點(diǎn)(惡意節(jié)點(diǎn)),建立黑洞攻擊及選擇性轉(zhuǎn)發(fā)攻擊兩種行為模型,驗(yàn)證ORLEACH協(xié)議對(duì)兩種攻擊的抵御能力。建立模型如下:
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等為攻擊者的行為,通過(guò)竊聽(tīng)信道中的消息,并使用addKnow()函數(shù)存儲(chǔ)到自己的知識(shí)集中,然后從知識(shí)集中隨意組合消息內(nèi)容發(fā)送到信道中,如19、20行,攻擊者將隨意組合收集到的信息,然后重放到信道中。
2.4 驗(yàn)證
完整性和黑洞攻擊的檢測(cè)均可用可達(dá)性進(jìn)行分析,即在模型的所有路徑中,存在一條路徑的某個(gè)狀態(tài)滿足要驗(yàn)證的條件。
協(xié)議的安全性包括:
(1)黑洞攻擊檢測(cè)。G1:#define goal1(checked==true);checked初始狀態(tài)為false,當(dāng)實(shí)行黑洞攻擊的簇頭節(jié)點(diǎn)被檢測(cè)出,再參與建簇的行為后,可被隔離。
(2)完整性檢測(cè)。G2:#define goal2 tempered==true);tempered初始狀態(tài)為false,當(dāng)攻擊節(jié)點(diǎn)實(shí)行選擇性轉(zhuǎn)發(fā)時(shí),值為true。
如果G1斷言通過(guò),系統(tǒng)狀態(tài)可以到達(dá)goal1,表示本次的簇頭節(jié)點(diǎn)是惡意節(jié)點(diǎn),該節(jié)點(diǎn)在之前的建簇過(guò)程中成為簇頭,并實(shí)施了黑洞攻擊,卻被監(jiān)控節(jié)點(diǎn)檢測(cè)出來(lái),并將此警報(bào)信息廣播給周?chē)従庸?jié)點(diǎn)。成員節(jié)點(diǎn)接收到此消息,更新自己的黑名單,在本輪建簇過(guò)程中,識(shí)別出聲明建簇的節(jié)點(diǎn)為惡意節(jié)點(diǎn)。反之,若不能到達(dá)goal1,表示該系統(tǒng)能夠抵御黑洞攻擊。PAT驗(yàn)證通過(guò),能夠檢測(cè)出實(shí)施黑洞攻擊的節(jié)點(diǎn),并將其加入黑名單中孤立。
若第G2條斷言語(yǔ)句通過(guò),系統(tǒng)狀態(tài)可以到達(dá)goal2,表示損壞節(jié)點(diǎn)成為簇頭,并實(shí)施了選擇性轉(zhuǎn)發(fā)攻擊,將篡改的數(shù)據(jù)發(fā)送給了基站。這條性質(zhì)說(shuō)明對(duì)于損壞節(jié)點(diǎn)實(shí)施的選擇性轉(zhuǎn)發(fā)攻擊,監(jiān)控節(jié)點(diǎn)不能檢測(cè)出。因此,該系統(tǒng)不能抵御內(nèi)部節(jié)點(diǎn)實(shí)施的選擇性轉(zhuǎn)發(fā)攻擊。PAT工具給出一條見(jiàn)證跡時(shí)序圖(見(jiàn)圖1),粗線表示攻擊者的行為,在網(wǎng)絡(luò)正常通信過(guò)程中,攻擊者通過(guò)竊聽(tīng)信道中的信息,獲取成員節(jié)點(diǎn)發(fā)送給簇頭節(jié)點(diǎn)的加密數(shù)據(jù),并進(jìn)行篡改(tamper),然后將這些篡改的數(shù)據(jù)發(fā)送到信道中,簇頭節(jié)點(diǎn)接收后無(wú)法分辨消息的完整性,在進(jìn)行數(shù)據(jù)融合時(shí),便將這些篡改后的消息一同融合并發(fā)送到基站。
(3)認(rèn)證性。首先定義如下變量:
#define iniRunningCN (IniRunningCN==true); 當(dāng)簇頭開(kāi)始廣播建簇時(shí),IniRunningCN置為true;
#define iniCommitCN (IniCommitCN==true);當(dāng)簇頭完成收到成員節(jié)點(diǎn)的數(shù)據(jù)后,InitCommit置為true;
#define resRunningCN (ResRunningCN==true);當(dāng)成員節(jié)點(diǎn)收到簇頭節(jié)點(diǎn)的廣播消息時(shí),ResCommit置為true;
#define resCommitCN (ResCommitCN==true);當(dāng)成員節(jié)點(diǎn)收到簇頭節(jié)點(diǎn)的時(shí)間片標(biāo)志時(shí),ResCommit置為true。
認(rèn)證性。保證接收者接收到的消息是聲明的節(jié)點(diǎn)發(fā)送的。使用LTL描述性質(zhì):
G3:[](([]!iniCommitCN)‖(!iniCommitCN U resRunningCN));endprint
G4:[](([]!resCommitCN)‖(!resCommitCN U iniRunningCN));
若G3不滿足,說(shuō)明有攻擊者竊取簇頭發(fā)送的消息,并冒充成員節(jié)點(diǎn)Nid與簇頭節(jié)點(diǎn)CHid通信;若G4不滿足,說(shuō)明有攻擊者冒充簇頭CHid與成員節(jié)點(diǎn)Nid通信。
在驗(yàn)證時(shí),出現(xiàn)問(wè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
結(jié)果表明,攻擊者I作為簇頭節(jié)點(diǎn)CH與成員節(jié)點(diǎn)Node的中間人,攻擊者可以在網(wǎng)絡(luò)中隨意重放建簇及其它消息,迫使雙方進(jìn)行無(wú)限制的通信,達(dá)到快速消耗節(jié)點(diǎn)能源的目的。由于ORLEACH協(xié)議中加入監(jiān)控機(jī)制,當(dāng)監(jiān)控節(jié)點(diǎn)監(jiān)控到簇頭不正常行為時(shí),廣播警報(bào)消息,使該簇頭節(jié)點(diǎn)被孤立。
3 結(jié)語(yǔ)
本文對(duì)加入監(jiān)控機(jī)制和密鑰管理機(jī)制的分簇安全協(xié)議ORLEACH使用模型檢測(cè)工具PAT建立簡(jiǎn)易的CSP模型,并進(jìn)行了安全性驗(yàn)證,發(fā)現(xiàn)對(duì)于來(lái)自網(wǎng)絡(luò)內(nèi)部的攻擊,該協(xié)議能夠及時(shí)檢測(cè)出實(shí)施黑洞攻擊的損壞節(jié)點(diǎn),并將其孤立,提高了整個(gè)網(wǎng)絡(luò)的數(shù)據(jù)傳輸率。然而對(duì)于攻擊節(jié)點(diǎn)實(shí)行的篡改攻擊數(shù)據(jù)完整性的問(wèn)題,該協(xié)議不能保證檢測(cè)出。對(duì)于不能加入到網(wǎng)絡(luò)中的外部攻擊節(jié)點(diǎn)也可以竊聽(tīng)到簇頭的建簇消息(廣播的建簇消息沒(méi)有加密),從而獲取簇頭的身份id,并可以在網(wǎng)絡(luò)中無(wú)限制地重放此消息,從而消耗內(nèi)部節(jié)點(diǎn)的能量。因此,將針對(duì)該協(xié)議的這兩個(gè)缺點(diǎn)作深入研究,并對(duì)協(xié)議模型進(jìn)行繼續(xù)細(xì)化,同時(shí)對(duì)PAT工具建立適應(yīng)于分簇協(xié)議的建模框架。
參考文獻(xiàn):
[1] 孫利民,李建中,陳渝,等.無(wú)線傳感器網(wǎng)絡(luò)[M].北京:清華大學(xué)出版社,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)絡(luò)與信息安全學(xué)報(bào),2016,2(3):52-67.
[7] 馬俊偉.基于PAT工具的智能家居平臺(tái)形式化分析與檢驗(yàn)[D].太原:太原理工大學(xué),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] 霍爾.通信順序進(jìn)程[M].北京:北京大學(xué)出版社,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.
(責(zé)任編輯:孫 娟)endprint