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

Using CSP for formal analysis of IEEE 802.11w protocol

运行在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.