基于模型检测的无线体域网安全协议形式化验证
2016-01-22陈铁明,虞震波,王婷等
基于模型检测的无线体域网安全协议形式化验证
陈铁明，虞震波，王婷，方赵林
(浙江工业大学 计算机科学与技术学院，浙江 杭州 310023)
摘要：在研究无线体域网(WBAN)安全属性的基础上，为了对无线体域网安全协议进行安全分析，保证协议设计之初的安全性，提出并实现了一种基于模型检测的无线体域网安全协议形式化分析和验证方法.基于模型检测工具PAT研究建模语言CSP#及其扩展方法，提出一种支持网络节点可移动的抽象建模数据结构，便于对WBAN协议的形式化建模；根据Dolev-Yao模型，结合WBAN节点位置的可移动性，建立攻击者抽象模型.以Chitra等提出的基于双天线的WBAN安全协议为例，在PAT工具中应用笔者提出的方法对其进行建模并加以分析验证，体现了方法的实用性. 2) CU与待认证传感器节点的建模如下：
关键词：无线体域网；模型检测；安全协议；PAT；CSP#；线性时序逻辑
收稿日期：2015-04-17
基金项目：国家自然科学基金资助项目(61103044)
作者简介：陈铁明(1978—)，男，浙江诸暨人，副教授，博士，研究方向为网络信息安全，E-mail:tmchen@zjut.edu.cn.
中图分类号：TP309.7
文献标志码：A
文章编号：1006-4303(2015)05-0497-06
Abstract:Based on the research of wireless body area network (WBAN) security attributes, a formal analysis and verification method for WBAN security protocols is proposed and implemented in this paper. The method can ensure the security of WBAN protocols in the early stage of protocol design. First, the modeling language CSP# which is supported by the model checker PAT is extended with an abstract modeling data structure supporting the node mobility, which could simplify the modeling of WBAN protocols. Then, an abstract attacker model is established through the combination of Dolev-Yao model and WBAN node mobility. Finally, the WBAN security protocol proposed by Chitra et al. is modeled and verified using our method embedded in PAT, which reflects the usability and efficiency of this method.
Keywords:wireless body area networks; model checking; security protocols; PAT; CSP#; linear temporal logic
Formal verification of wireless body area network security
protocols based on model checking
CHEN Tieming, YU Zhenbo, WANG Ting, FANG Zhaolin
(College of Computer Science and Technology, Zhejiang University of Technology, Hangzhou 310023, China)
随着无线通信技术和无线传感技术的不断发展，无线传感器网络的研究和应用获得了巨大成功[1-4].无线体域网(Wireless body area network, WBAN)是无线传感网在智能定位、医学领域的分支，主要应用于人体区域,负责采集人体机能数据以供医疗分析[5].安全协议作为构成无线传感网络的关键部分，其数据的安全性、认证的可靠性是制约WBAN正常通信的最重要因素.自从Dolev和Yao提出将模型检测技术应用于安全协议分析和验证[6]，模型检测技术以其简洁明了的建模过程和高度自动化的分析验证成为了当前主流的形式化分析技术[7].Aladdin等通过时序Petri网对网络协议进行建模，确保了协议的正确可靠[8].Kashif等使用SPIN模型[9]检测工具对WSN路由协议进行形式化分析，发现了攻击漏洞[10].Lowe利用进程代数使用CSP(Communicating sequential process)方法[11]对NSPK协议进行了形式化分析，发现了一个十几年来未知的攻击.2015年Wang等使用模型检测技术对WBAN的MAC层安全协议做了形式化分析[12].然而目前对WBAN安全协议的形式化分析工作仍比较少，因此对WBAN安全协议进行形式化分析验证的重要性不言而喻.
上述方法均采用某种形式化建模语言实现对安全协议的形式化描述，进而被相应支持该形式化语言的工具接受并实现自动化模型检测过程.虽然模型检测工具的自动化验证程度高，分析过程严谨，但是系统建模的过程仍比较复杂，需要具有专业知识经验的人工支持，建模过程的好坏直接影响到验证结果的正确性.因此面向不同应用领域定制开发专用的建模语言也是一种发展趋势.利用新型模型检测工具PAT(Process analysis toolkit)框架[13]的高度可扩展性，提出一个基于数据结构的CSP#语言扩展模块，提高WBAN安全协议的形式化建模和分析效率，实现了一种面向WBAN位置相关安全协议的专用建模与验证方法.
1PAT模型检测工具
PAT是由新加坡国立大学PAT研究小组自主开发的一套模型检测工具，支持并发、实时系统、UML状态机等系统的建模验证，能够对CSP#，RTS，LTS等多种语言进行模拟验证和反例生成.
PAT是一个可扩展、模块化的通用架构，其系统框架[14]如图1所示，整个框架分为4层，这种分层架构方便了模块的扩展，并将建模验证过程分为3步：编译、抽象和验证.从图1中可以看出：最上层的建模层(Modeling layer)，包含了多个不同领域、不同目标系统的建模模块，可以使用某种建模语言(如CSP#)对不同的系统进行建模；第二层是抽象层(Abstraction layer)，能够对上层已经建模完成的系统进行抽象分析，包括对不同系统的数据、环境等的抽象；第三层是中间呈现层(Intermediate representation layer)，负责将输入的系统模型转化为一种中间状态(如标签迁移系统LTS)，以对应底层不同的模型检测算法；底层是分析层(Analysis layer)，包含模型检测技术的关键算法，如死锁检测算法、LTL性质检测算法等.
PAT工具具有如此良好的扩展性，因此可以利用建模层的抽象功能对建模层语言模块进行抽象，扩展PAT的CSP#模块(即并行模块)，方便WBAN领域安全协议的建模验证.抽象后的语言模块能够自动转化为PAT已经支持的语言，从而简化系统描述和实现过程，使得建模过程更人性化、更易使用.借助PAT工具良好的扩展性，可方便对WBAN安全协议的建模.
图1 模型检测工具PAT的系统框架图 Fig.1 The system framework of PAT
2无线体域网节点位置建模
2.1基于双天线的无线体域网协议
无线体域网节点位置随着人的移动而变化，且传感器节点体积小、容量和能源有限，很容易受到外界的攻击，导致WBAN安全问题层出不穷.为此，Javali等首次提出了基于双天线的无线体域网安全认证方案[15]，该方案基于接受信号强度(Received signal strength, RSS)，利用双天线本身位置的分离性，能够有效的将攻击手段排除在其射频范围外.
该方案模型假设有一个双天线的可信任实体节点CU和若干个单天线的待认证节点，图2给出了CU和传感器节点布置图.图中节点E为攻击者节点，B为诚实实体节点，A1和A2分别代表CU的两条天线.从图2中可以看出：节点E到A1,A2的距离分别为e1,e2，节点B到A1,A2距离为d1,d2.
图2 无线体域网安全认证协议模型节点布置图 Fig.2 The node layout of WBAN security authentication protocol model
节点E与可信任节点CU之间的通信过程如下：
1) CU→E:Probe={IDcu}
2) E→CU:Resp[0]={IDE,P0,L0,K0}
…
i) E→CU:Resp[i]={IDE,Pi,Li,Ki}
…
n) E→CU:Resp[n]={IDE,Pn,Ln,Kn}
其中：Pi为发送方发送消息时的能量；Ki为随机数；Li为发送方的位置信息.
首先CU给传感器节点向其射频范围内广播一个探测包Probe用以发现未认证节点，传感器节点收到探测包后发送一个响应包Resp[i]，包含节点此时的发送能量，位置信息以及随机数，CU收到响应包后，计算包的RSSI(Receivedsignalstrengthindication)值为
其中：di为此时传感器节点与CU的距离；α为节点间的距离能量指数.
计算A1和A2的RSSI平均值RDavg，计算公式为
其中：j={1,2,…,n}，n为p和q之间的较小值.
4) CU将RDavg和RSSI门槛值RDth进行比较，将小于RDth的传感器节点视为攻击者节点，大于RDth的传感器节点则为诚实节点.最后CU给诚实节点发送AssocResp[ACCEPT]消息.
2.2支持节点可移动的抽象方法
由于人的日常行为使WBAN节点位置经常发生移动，要求在建模过程中考虑节点可能移动到的位置，加大了建模的复杂度.利用CSP#语言的扩展性对节点的移动进行抽象，可以有效提高建模的准确率，下面采用二维坐标对传感节点的位置信息进行抽象：
public class Location: ExpressionValue {
public intx; //节点位置x坐标
public inty; //节点位置y坐标
public int CalculateDistance(Location){…}
…
};
类Location中包含节点的二维坐标，并通过自定义函数CalculateDistance()计算两个节点间的欧氏距离，从而判断节点位置是否移动或超出射频范围.例如，假设节点A和B的位置信息分别为(xa,ya)，(xb,yb)，R表示节点传输距离，当((xa-xb)(xa-xb)+(ya-yb)(ya-yb))>R·R时，说明节点A和B间的距离超出了节点的射频范围.
知识集类KnowledgeSet用于存储协议执行过程中的数据信息，如：ID，随机数等会直接影响协议能否正常执行的变量.其中内置SortedList
public class KnowledgeSet : ExpressionValue {
public SortedList
public bool Add(UnitType, Object); //增加知识集
public Object Get(UnitType); //提取知识集
…
};
在上述抽象的基础上，封装成WSNNode结构，扩展PAT建模层的CSP#语言模块，加入新的函数库和语义，WSNNode类图如图3所示.
图3 面向WBAN传感节点建模的WSNNode类图 Fig.3 The class diagram of WBAN sensor model
WSNNode结构代表传感器节点，其中包含了协议正常执行的所有信息，包括节点ID、传输半径、位置信息、知识集信息、随机数等内容.WSNNode结构和新函数库的设计极大地简化了WBAN安全协议的建模与验证.
3形式化建模与验证
3.1WBAN协议形式化建模及性质描述
3.1.1协议诚实实体节点建模
采用有穷状态机描述协议中信任节点CU在协议执行过程中的状态迁移情况，如图4所示.
图4 协议信任节点CU的状态转换图 Fig.4 The State transition diagram of trusted sensor CU
图4中idle为CU的初始状态；当CU广播一个探测包后自动跳转到State1状态，并等待有未认证的传感器节点回送ACK确认消息；收到ACK确认消息后跳转到State2状态，判断响应节点是否在其射频范围内；若在其射频范围内，则与响应节点重复交互n次消息，这n次消息由CU的两条天线A1和A2随机接收，结束交互后跳转到State3状态；State3状态将计算着n次消息RSSI值的平均值RDavg，并跳转到State4状态；State4状态将RSSI平均值与门槛RDth进行比较，若RDavg>RDth则该传感器节点为合法节点，认证结束，跳转到idle状态；否则，认证失败，重新跳转到idle状态.
需要注意的是，在认证过程中，响应节点可能会移动节点位置，同样信任节点CU在认证过程中也会移动节点位置.
下面介绍如何利用基于CSP#扩展的利用抽象节点可移动的建模方法对协议信任节点CU进行建模.先对接下来需要涉及的CSP#语言语法进行简单说明：P()=Exp代表一个进程或某主体的行为，其中()内可带参数，Exp代表过程描述，例如P()=e→P()代表进程P循环执行事件e；事件e可带参数，例如e.exp1.exp2，其中exp1和exp2为变量；符号?和!代表输入输出通道，其中?为接受消息，!为发送消息；[]代表选择，例如公式P[]Q表示可能执行P，也可能执行Q.
1) 定义两个全局消息通道，作为协议中实体间消息传递的载体：
channel ca 0;
channel cb 0;
其中：通道ca用于承载CU广播探测包的消息；通道cb用于传递CU与待认证传感器节点的n条重复消息，由于这n条消息的格式相同，故用同一通道代替.
PInitPre(NodeCU, Loc) =//初始化CU节点信息
IntruderInitial {
Node_A1.addItem(NodeCU, Loc, LCU_A1);
Node_A2.addItem(NodeCU, Loc, LCU_A2);
} -> PInit ();
PInit()=//开始执行协议
ca! Node_A1. everyone -> PInit() []
ca! Node_A2. everyone -> PInit() []
ca? Node_A1. to1 -> PInit() []
ca? Node_A2. to1 -> PInit() []
cb! Node_A1. tox. Power. Loc. Nonce -> PInit()[]
cb! Node_A2. tox. Power. Loc. Nonce -> PInit();
变量LCU_A1与LCU_A2分别代表了CU的两条天线，其位置坐标距离相差1 cm.LE代表攻击节点的位置信息.用一个枚举类型来初始化各个节点的ID信息，以避免重复ID的现象.
3.1.2节点可移动的攻击者建模
对攻击者E的建模最为复杂.结合攻击者位置的可移动性以及攻击者可以利用改变发送功率的方式伪造信号强度，对Dolev-Yao模型[16]进行扩展，攻击者节点应具有以下能力：
1) 可以窃听并截获协议执行过程中节点传输的消息，以窃取CU的正常通信范围.
2) 可以冒充协议诚实节点发送消息.
3) 根据截获的消息，动态增长自己的知识集(KnowledgeSet对象)，从而产生新的攻击消息.
4) 利用节点可移动性，在诚实节点射频范围外利用功率大、收发能力强的收发器向周围节点发送信息，诱使周围节点认为攻击节点在其射频范围内.
使用基于CSP#扩展抽象节点可移动的建模方法对攻击者E建模，主要分为两大部分：一、对网络中的消息进行截获，破坏诚实节点与CU的正常通信，以及窃取正常节点的信息；二、攻击者移动位置，伪装成诚实节点与CU通信.关键代码如下：
PIntruderPre(NodeE, Loc) =
IntruderInitial {
NodeE.addItem(NodeE, Loc);
} -> PIntruder();
PIntruder() =
cA?ID_X . to1 ->//截获并存储消息
InterceptChanA {
…//截获通道ca中的探测包并保存.
NodeE.addItem(…) ;
}-> PIntruder() []
cA?ID_X . to1. PowerX. LocX. NonceX ->
InterceptChanA {
…//截获通道cb中的认证消息并保存.
NodeE.addItem(…) ;
}-> PIntruder() []
//重放截获的消息或根据获取知识产生新消息
cA! NodeE. tox -> PIntruder() []
cB! NodeE. tox. Power. Loc. Nonce -> PIntruder() ;
攻击者节点通过NodeE.addItem()函数将截获的消息存入知识集KnowledgeSet对象中，随后从知识集KnowledgeSet中任意选取ID、能量值、位置信息、随机数组合成一个节点Node发送到通道中，攻击者将枚举所有可能的组合.
为了抽象节点的射频范围内的所有移动可能性，在初始阶段定义了信任节点CU和攻击者E的传输距离RadiusCU和RadiusE，给出如下PAT模型用于自动生成所有可能的节点位置：
[]x1:{0…RadiusCU};y1:{0…RadiusCU};x2:{0…RadiusE};y2:{0…RadiusE}
@(PInitPre(NodeCU,newLocation(x1,y1))|||PIntruderPre(NodeE,newLocation(x2,y2)))
其中：符号[]表示x,y每次在其取值范围内任取一个值；|||表示协议发起方与接收方并发执行.
针对位置可移动的情况，攻击者节点对位置的选择不局限于其自身的可移动范围RadiusE.在最后的实验结果中我们可以看到，若RadiusE与CU的射频范围RadiusCU有重叠则攻击者可冒充诚实节点与CU通信，所以攻击者的行为是不确定的，它的执行是无限循环上述代码，枚举所有可能的状态，从而能够搜索整个状态空间.
3.1.3LTL性质描述
采用线性时序逻辑[17](Linear temporal logic, LTL)对协议属性进行规范描述.为了更方便的描述协议性质，对CSP#扩展定义如下变量：
#defineiniRunningEU(req_CU==true)；//当攻击者节点伪装成诚实节点给信任节点CU回送ACK确认消息时置true.
#defineresCommitEU(ack_2_E==true)；//当CU与节点E完成n次消息交互，并完成认证时置true.
#defineMoveInRadius(OutRadius==true)；//当攻击者节点移入CU的射频范围时置true.
协议的认证性是指确认对方的真实身份，并保证其真实身份与消息中所声称的身份相一致.分析Chitra等提出的WBAN安全协议时，采用文[15]的方法进行检测：当攻击者E收到信任节点CU广播的探测包，则待认证的响应方E必须回送一个确认消息，同时开始认证过程，此时攻击者E的位置必定在CU的射频范围内.因此可用LTL公式G:[](MoveInRadius→<>!(iniRunningEU→resCommitEU))表示协议的认证性.其中<>表示最终(eventually)，[]表示一直(always)，!表示否定.若公式G不满足，则表示有攻击者闯入CU的射频范围内，并认证成功.
3.2实验结果与分析
将WBAN安全认证协议的抽象CSP#模型和上一小节描述的LTL性质导入PAT工具中进行模拟验证.结果显示公式G验证失败，其反例路径如图5所示.
图5 反例路径图 Fig.5 The path diagram of counter-example
反例路径中间栏是被攻击者截获或篡改的消息，节点CU的两条天线初始位置分别为(0,0)和(0,1)，节点E的初始位置为(0,6)，在与CU进行认证的过程中位置移动到(0,4)，此时节点E已移入CU的射频范围，并在射频范围内停留足够长的时间，从而满足文[15]对认证性的描述并完成认证.说明此种基于双天线的WBAN安全协议存在缺陷：无法抵御可移动攻击者的入侵.结合原始协议可以得出验证失败的原因：当节点E移入CU的射频范围内时，CU计算出的RSSI值大于RSSI门槛值RDth，若节点E在CU的射频范围内的时间足够长，则n次消息认证的RSSI平均值RDavg将大于RDth，最终认证成功.
4结论
在PAT工具的基础上，提出了一种支持节点可移动的抽象建模数据结构，扩展了CSP#语言模块.对Chitra等提出的安全认证方案进行建模和分析，发现若可移动攻击者的移动范围与信任节点CU的射频范围有交集，则有被攻击的可能.研究发现：对建模过程进行抽象能够有效降低建模的复杂性，更直观地发现协议存在的问题，体现了抽象方法的实用性.因此下一步的研究将在更高层次抽象建模语言和模块，针对无线体域网领域开发专用建模语言，并研究抽象描述语言和CSP#的自动转换，实现模型检测真正的自动化.
参考文献：
[1]陈铁明,江颉,王小号,等.一种改进的基于位置的攻击容忍WSN安全方案[J].传感技术学报,2012,25(4):545-551.
[2]陈庆章,张海洋,陈辰,等.基于WSN的人体姿态辨识系统设计[J].浙江工业大学学报,2014,42(6):591-593.
[3]周晓,李杰,边裕挺.基于无线传感网络的环境温度检测系统设计[J].浙江工业大学学报,2013,41(4):440-443.
[4]陆欢佳,俞立,董齐芬,等.基于无线传感网的楼宇环境检测系统设计[J].浙江工业大学学报,2011,39(6):683-687.
[5]JURIK A, WEAVER A. Remote medical monitoring[J]. Computer,2008,41(4):96-99.
[6]NOVOTNY M. Formal analysis of security protocols for wireless sensor networks[J]. Tatra Mountains Mathematical Publications,2010,47(1):81-97.
[7]林惠民,张文辉.模型检测：理论、方法与应用[J].电子学报,2002,30(12A):1907-1912.
[8]ALADDIN M, THOMAS B, ARMAND T. Network protocol modeling: a time Petri net modular approach[C]//16th International Conference on Software, Telecommunications and Computer Networks. Split: IEEE Press,2008:273-277.
[9]HOLZMANN G J. The spin model checker primer and reference manual[M]. New Jersey: Addison Wesley,2003.
[10]JAVED K, KASHIF A, TROUBITSYNA E. Implementation of spin model checker for formal verification of distance vector routing protocol[J]. International Journal of Computer Science and Information Security,2010,8(3):1-6.
[11]LOWE G, ROSCOE B. Using CSP to detect errors in the TMN protocol[J]. IEEE Transactions on Software Engineering,1997,23(10):659-669.
[12]WANG Y Y, DONG H L, YU Y T, et al. Analyzing IEEE802.15.6 protocol with stochastic model checking[J]. Journal of Computational Information Systems,2015,11(3):935-947.
[13]SUN J, LIU Y AND DONG J S. Model checking CSP revisited: introducing a process analysis toolkit[J]. Communications in Computer and Information Science,2009,17(7):307-322.
[14]LIU Y, SUN J, DONG J S. Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney: Springer Press,2010:371-377.
[15]JAVALI C, REVADIGAR G, LIBMAN L, et al. SeAK: secure authentication and key generation protocol based on dual antennas for wireless body area networks[C]//10th International Workshop. Oxford: Springer Press,2014:74-89.
[16]DOLEV D, YAO A C. On the security of public key protocols[J]. IEEE Transactions on Information Theory,1981,29(2):350-357.
[17]BAIER C, KATOEN J P, LARSEN K G. Principles of model checking[M]. Cambridge: The MIT Press, 2008.
(责任编辑：刘岩)
