利用CSP方法对IEEE 802.11w形式化分析  

Using CSP for formal analysis of IEEE 802.11w protocol

作　　者：吴名欢[1] 程小辉[1] 李雄伟 

机构地区：[1]桂林理工大学信息科学与工程学院,广西桂林541004 [2]中国石油集团测井有限公司信息管理部,西安710077

出　　处：《计算机应用研究》2015年第5期1489-1492,1502,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(61262075);广西高等学校资助项目(KY2015YB120);广西高等学校重大科研基金资助项目(201201ZD012)

摘　　要：运行在IEEE 802.11i基础上的IEEE 802.11w增加了对无线网络管理帧的保护,针对IEEE 802.11w协议的安全性问题,利用了通信顺序进程(CSP)对其进行形式化分析。对协议运行在恶意环境中,存在攻击者的情况下,利用CSP方法建立了攻击者和协议主体的CSP进程模型。使用模型检测工具故障发散改进器(FDR)进行仿真实验,对协议的认证和安全属性进行了校验,发现该协议存在中间人攻击情况,为提高IEEE 802.11w的安全性提供了帮助。IEEE 802. 11 w authentication protocol based on the IEEE 802. 11 i enhances the IEEE 802. 11 i security for management frames. In order to study the safety of the protocol,this paper modeled the protocol by formal analysis using communicating sequential processes（ CSP）. This paper chosed the role of protocol and the attacker for modelling and verification. It used CSP for modelling and performed the verification using FDR. In the experiments,it found an attack in this protocol. It checked authentication and security attributes and discovered the middleman attack case. It can provide a reference to improve the safety of IEEE 802. 11 w help.

关 键 词：无线网络 形式化分析 故障发散改进器 通信顺序进程 

分 类 号：TP393.04[自动化与计算机技术—计算机应用技术]