Security is a serious concern in wireless networks. In order to eliminate the vulnerabilities in previous Standards, the IEEE 802.11i Standard is designed to provide security enhancements in MAC layer. The authentication process consists of several components, including an 802.1X authentication phase using TLS over EAP, a 4-Way Handshake to establish a fresh session key, and an optional Group Key Handshake for group communications. The objective of this work is to analyze IEEE 802.11i with respect to data confidentiality, integrity, mutual authentication, and availability.
Under our threat model, 802.11i appears to provide effective data confidentiality and integrity when CCMP is used. 802.11i may also provide satisfactory mutual authentication and key management, although there are some potential implementation oversights that may cause severe problems. On the other hand, we identified several Denial of Service attacks. Different solutions are proposed for these vulnerabilities, which result in an improved variant of 802.11i with a more effecient failure recovery mechanism. Some of the resulting improvements have been adopted by the IEEE 802.11 TGi in their final deliberation.
We used a finite-state verification tool, called Mur$\phi$, to analyze the 4-Way Handshake component. Our result shows that finite-state verification is quite effective for analyzing security protocols. Furthermore, we adopted Protocol Composition Logic to conduct a correctness proof of 802.11i, including SSL/TLS as a component. The proof is modular, comprising a separate proof for each protocol component and providing insight into the networking environment in which each component can be reliably used. Finally, we showed that 802.11i can significantly reduce the complexity of designing a secure routing protocol when it is deployed in wireless ad hoc networks.
Abstract: The IEEE 802.11i wireless networking protocol provides mutual authentication between a network access point and user devices prior to user connectivity. The protocol consists of several parts, including an 802.1X authentication phase using TLS over EAP, the 4-Way Handshake to establish a fresh session key, and an optional Group Key Handshake for group communications. Motivated by previous vulnerabilities in related wireless protocols and changes in 802.11i to provide better security, we carry out a formal proof of correctness using a Protocol Composition Logic previously used for other protocols. The proof is modular, comprising a separate proof for each protocol section and providing insight into the networking environment in which each section can be reliably used. Further, the proof holds for a variety of failure recovery strategies and other implementation and configuration options. Since SSL/TLS is widely used apart from 802.11i, the security proof for SSL/TLS has independent interest.
Abstract: This paper analyzes the IEEE 802.11i wireless networking standard with respect to data confidentiality, integrity, mutual authentication, and availability. Under our threat model, 802.11i appears to provide effective data confidentiality and integrity when CCMP is used. Furthermore, 802.11i may provide satisfactory mutual authentication and key management, although there are some potential implementation oversights that may cause severe problems. Since the 802.11i design does not emphasize availability, several DoS attacks are possible. We review the known DoS attacks on unprotected management frames and EAP frames, and discuss ways of mitigating them in 802.11i. The practicality of a DoS attack against Michael MIC Failure countermeasure is discussed and improvements are proposed. Two new DoS attacks and possible repairs are identified: RSN IE Poisoning and 4-Way Handshake Blocking. Finally some tradeoffs in failure-recovery strategies are discussed and an improved variant of 802.11i is proposed to address all the discussed vulnerabilities.
Abstract: 802.11i is an IEEE standard designed to provide enhanced MAC security in wireless networks. The authentication process involves three entities: the supplicant (wireless device), the authenticator (access point), and the authentication server (e.g., a backend RADIUS server). A 4-Way Handshake must be executed between the supplicant and the authenticator to derive a fresh pairwise key and/or group key for subsequent data transmissions. We analyze the 4-Way Handshake protocol using a finite-state verification tool and find a Denial-of-Service attack. The attack involves forging initial messages from the authenticator to the supplicant to produce inconsistent keys in peers. Three repairs are proposed; based on various considerations, the third one appears to be the best. The resulting improvement to the standard, adopted by the 802.11 TGi in their final deliberation, involves only a minor change in the algorithm used by the supplicant.