基于SPIN的无线传感器网络安全协议建模与分析  

Using SPIN to Model and Analyze Security Protocol in Wireless Sensor Network

作　　者：敬超[1] 常亮[1] 古天龙[1] 

机构地区：[1]桂林电子科技大学计算机控制学院,桂林541004

出　　处：《计算机科学》2009年第10期132-136,共5页Computer Science

基　　金：广西研究生教育创新项目(2007105950812M16)资助

摘　　要：模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功。无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战。提出了一种适用于无线传感器网络的安全协议形式化建模分析方法。它充分借鉴了传统有线网络安全协议的建模方法,在其基础上充分考察了无线传感器网络的通信环境以及网络节点,建立起一个全面并且直观的安全协议运行模型。以A.Perrig等人提出的SPINS安全协议为例,应用模型检验工具SPIN对其认证性和机密性等安全需求进行了分析验证,发现了该协议存在的漏洞。实例分析证实了模型检验方法在分析无线传感器网络安全协议时的有效性,从而推进了其在安全协议分析方面的应用范围。Model checking has been successfully applied to design and analyze wired network security protocol. Compared with the wired network,wireless sensor network（WSN） also has the strict requirement on its security protocol. The vulnerabilities of WSN exist in communication environment and network node; those are great challenges for designing and analyzing a security protocol in WSN. This paper proposed an appropriate method to model and analyze security protocol in the WSN. Based on the method of wired network security protocol, with the thorough consideration of sensor network environmental factors and feature of sensor nodes, a general model was established and analyzed by our method. The paper took WSN SPINS security protocol as an example to model and analyze viaSPIN tool Through verifying the authentication and confidentiality of SPINS, we found flaws in the SPINS protocol. The work demonstrates the feasibility of using model checking to model and analyze security protocol in WSN, and expands the usage of model checking.

关 键 词：无线传感器网络 模型检验 SPINS协议 SPIN工具 PROMELA 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]