Formal Verification of IEEE 802.11w Authentication Protocol

IEEE 802.11 is the standard designed to provide secured communication in wireless LAN. IEEE 802.11w authentication protocol enhances the IEEE802.11i security for selected management frames. These protocols allow a wireless station to gain access to a protected wireless network managed by an access point. In this paper, a section of the protocol is chosen for modelling and verification. Communicating Sequential Process (CSP) is used for modelling and the verification is performed using CasperFDR. CasperFDR can verify most of the communication protocols. It can perform an exhaustive verification that can establish with mathematical certainty whether or not a given behaviour is error-free. CasperFDR is used to specify system behaviour in a formal validation model that defines interactions between the processes. This paper models IEEE802.11w authentication protocol by formal verification using CasperFDR and analyzes the output. A few attacks are found in this protocol. The specifications through which these attacks were found are presented.