王丽丹　杨红丽

摘 要：在目前协议安全问题日益突出的情况下，针对无线传感器网络中典型的分簇协议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