基于模型检测的无线体域网安全协议形式化验证

摘要：

在研究无线体域网(WBAN)安全属性的基础上,为了对无线体域网安全协议进行安全分析,保证协议设计之初的安全性,提出并实现了一种基于模型检测的无线体域网安全协议形式化分析和验证方法.基于模型检测工具PAT研究建模语言CSP#及其扩展方法,提出一种支持网络节点可移动的抽象建模数据结构,便于对WBAN协议的形式化建模;根据Dolev-Yao模型,结合WBAN节点位置的可移动性,建立攻击者抽象模型.以Chitra等提出的基于双天线的WBAN安全协议为例,在PAT工具中应用笔者提出的方法对其进行建模并加以分析验证,体现了方法的实用性.

关键词：无线体域网、模型检测、安全协议、PAT、CSP#、线性时序逻辑

所属期刊栏目：43

分类号：TP309.7(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61103044

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

页数：共6页

页码：497-502