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

摘要：

模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功.无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战.提出了一种适用于无线传感器网络的安全协议形式化建模分析方法.它充分借鉴了传统有线网络安全协议的建模方法,在其基础上充分考察了无线传感器网络的通信环境以及网络节点,建立起一个全面并且直观的安全协议运行模型.以A.Perrig等人提出的SPINS安全协议为例,应用模型检验工具SPIN对其认证性和机密性等安全需求进行了分析验证,发现了该协议存在的漏洞.实例分析证实了模型检验方法在分析无线传感器网络安全协议时的有效性,从而推进了其在安全协议分析方面的应用范围.

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

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2009-12-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：132-136