基于PAT的WSNs分簇安全协议研究

作     者：王丽丹 

作者单位：北京工业大学 

学位级别：硕士

导师姓名：杨红丽

授予年度：2017年

学科分类：0810[工学-信息与通信工程] 08[工学] 080202[工学-机械电子工程] 0802[工学-机械工程] 

主      题：WSNs 模型检测 分簇安全协议 ORLEACH PAT 

摘      要：随着无线传感器网络(Wireless Sensor Networks,简称WSNs)应用越来越普及,其安全问题日益突出,WSNs安全协议研究成为热点。由于协议在开发过程中,复杂的协议流程和应用场景可能会导致协议设计漏洞,给攻击者提供攻击的可能性。为了对协议的安全性进行分析,降低网络或节点被攻击的风险,将模型检测技术应用到WSNs安全协议的建模与验证中,已成为当前的研究热点。WSNs分簇协议由于网络中节点角色地位的不同以及复杂的通信流程,使得防御节点的攻击比较困难。ORLEACH协议是以LEACH(Low energy adaptive clustering Hierachy)分簇路由协议为基础,加入了入侵检测机制及其他安全机制的协议。为了验证ORLEACH协议的安全性,本文采用模型检测工具PAT(Process Analysis Toolkit)进行建模与验证。首先对PAT的函数库进行扩展,添加了新的数据结构及函数,然后验证了LTL公式表示的安全属性,如机密性、完整性、认证性等,最后根据ORLEACH协议的不足之处,给出了改进方案。本文主要贡献如下:(1)对PAT函数库进行扩展,加入新的数据结构与函数。WSNode函数库是节点所有属性的抽象;Key密钥函数库包括一系列的加密操作和解密操作;ORLEACHLIB函数库包括协议预分布阶段密钥池的生成,密钥环的分配等操作。WSNode函数库和Key密钥函数库是分簇安全协议建模通用的函数库,可以用于建模其他WSNs分簇安全协议。(2)对ORLEACH分簇协议建立节点行为模型和攻击模型。使用扩展后的PAT函数库,分别对协议中的簇头节点、监控节点、成员节点、基站建立了CSP#语言描述的输入模型,然后对协议的建簇和数据传输阶段建立了黑洞攻击和篡改攻击模型,以及对协议邻居节点认证阶段建立综合攻击模型。(3)利用PAT验证ORLEACH协议。在协议建模的基础上,利用PAT工具对消息机密性和完整性进行验证,结果发现,ORLEACH协议实现了数据的机密性,保证外部攻击节点即使窃取了数据包也不能破解其中的内容;ORLEACH协议能够检测出实施黑洞攻击的节点,并将其隔离;但是对实施了篡改攻击的节点不能识别,即不能保证消息的完整性;除此外,当对共享密钥发现阶段邻居节点认证过程进行验证时,发现攻击节点的介入能够使非邻居节点完成认证。(4)改进ORLEACH协议。根据PAT验证结果中给出的反例,提出的改进方案包括:采用消息认证码的方式,在节点发送数据时,同时发送一个使用与接收节点共享的密钥K对数据包进行MAC操作后得到的消息认证码,保证了消息的完整性;采用时间戳的方式,在节点进行广播认证时,同时发送一个当前时间的时间戳,实现了邻居节点间的双向认证。