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

摘要

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