Analysis of the 802.11i 4-way handshake

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.