基于模型检测的无线传感网安全协议形式化分析与改进*

陈铁明，何卡特，江 颉

(浙江工业大学计算机科学与技术学院，杭州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/．