基于PAT的WSNs安全分簇协议建模与验证  

WSNs Security Cluster-based Protocol Modeling and Validation Based on the PAT

作　　者：王丽丹[1] 杨红丽[1] 

机构地区：[1]北京工业大学信息学部,北京100124

出　　处：《软件导刊》2017年第9期177-180,184,共5页Software Guide

摘　　要：在目前协议安全问题日益突出的情况下,针对无线传感器网络中典型的分簇协议LEACH进行安全性改进的版本也越来越多,但这些版本是否真正安全并不确定。基于形式化建模的思想,以LEACH的安全协议版本ORLEACH协议为例,分别建立簇头节点、簇成员节点、监控节点以及攻击节点的CSP模型,并使用模型检查工具PAT对其进行验证,分析在攻击节点存在的情况下,协议是否能够满足网络的安全需求。验证结果表明,尽管ORLEACH协议中加入了安全机制,但是协议仍然不能抵挡某些攻击行为的发生。Under the condition of the protocol security problem increasingly, aiming at the typical cluster-based protocols in WSNs security improvement in the LEACH is also more and more, but these agreements whether safety is uncertain. In this pa- per, based on the idea of formal modeling, to the safety of the LEACH protocol version ORLEACH as an example, respectively set up the cluster-head nodes, the cluster member nodes, and attack nodes and the monitoring node of CSP model, and using the model checking tool PAT for its verification, analysis of the presence of node, the attack protocol can satisfy the security re- quirements o{ the network. Verification results show that although ORLEACH protocol to join the security mechanism, but the agreement still not strong enough to resist some attacks from happening.

关 键 词：安全协议 无线传感器网络 CSP 模型检查 PAT 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]