无线传感网络安全协议的形式化建模与分析

本项目研究一套面向无线传感网络安全协议抽象规约的形式化统一建模与分析的系统应用框架，主要包括三方面：（1）无线传感网安全协议的通用形式化描述；（2）无线传感网安全协议的安全属性统一建模；（3）基于模型检测的传感网安全协议形式化分析。研究建立基于进程代数的无线传感网安全协议通用形式化描述规范，实现传感安全协议的高层抽象模型，为不同的协议分析方法提供统一的、完善的协议规约描述，支持对无线传感网络环境特性及恶意节点攻击行为的刻画，避免对协议规约理想化操作可能引起的偏差；建立基于线性时序逻辑的无线传感网安全协议性质统一建模方法，实现安全协议的分析目标形式化，支持对无线传感网特殊安全性质的刻画，为自动推理演算方法提供统一的验证逻辑；建立基于模型检测的无线传感网安全协议形式化分析方法，实现对无线传感网协议攻击和安全性质线性时序逻辑公式的模型检测，实现一种分析协议规约模型的具体可操作方法。

本项目研究提出一套面向无线传感网络安全协议抽象规约的形式化统一建模与分析的系统应用框架，主要包括三方面：（1）无线传感网安全协议的通用形式化描述；（2）无线传感网安全协议的安全属性统一建模；（3）基于模型检测的传感网安全协议形式化分析。. 建立了基于进程代数的无线传感网安全协议通用形式化描述规范，实现传感安全协议的高层抽象模型，为不同的协议分析方法提供统一的、完善的协议规约描述，支持对无线传感网络环境特性及恶意节点攻击行为的刻画，避免对协议规约理想化操作可能引起的偏差，通用的形式化建模方法还应具备对无线传感网络环境特性及恶意节点攻击行为的细致刻画能力，研究提出的形式化规范主要能描述如下模型：可配置的传感节点及其数据感知行为，包括节点动态数据感知、激活等；事件驱动的传感节点间并行交互行为，包括节点消息异步收发、广播等；数据为中心的安全协议网络环境特征，包括端到端数据安全操作等；恶意传感节点的攻击行为，包括节点资源耗尽、信号或供电中断等。. 建立了基于线性时序逻辑的无线传感网络安全协议性质统一建模方法，实现安全协议的正确性分析目标形式化，为基于进程代数的自动推理演算方法提供统一的验证逻辑描述。除了传统安全协议所具有的安全属性，安全性质逻辑还应具备对无线传感网络安全协议特殊安全目标刻画，主要包括：传感节点密钥安全属性，即连通性、自愈性、容侵性等安全特征；传感节点硬件安全属性，基于位置、通信、能耗、时间等安全性质。. 建立了基于模型检测的无线传感网络安全协议形式化分析方法，实现对无线传感网络协议攻击和安全性质线性时序逻辑表达式的模型检测，给出一种分析协议规约的形式化模型可操作的具体方法。主要完成如下工作：实现基于PROMELA进程和模型检测工具SPIN的安全协议分析过程，主要需将传感协议规约的形式化模型转换成PROMELA模型检测代码；无线传感网络安全协议的安全缺陷实例分析，主要包括SPINS、TinySec、LEAP、TinyPK等网络各层代表性协议。. 本项目研究获得了超预期成果，共计发表论文10篇，其中SCI检索3篇，出版学术专著1部，授权国家发明专利3项，获得软件著作权1项；研究成果获得中国电子学会科学技术奖技术发明类三等奖，并通过企事业单位的应用推广取得了良好的社会经济效益。