What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication

Abstract

The latest Wi-Fi security standard, IEEE 802.11, includes a secure authentication protocol called SAE, whose use is mandatory for WPA3-Personal networks. The protocol is specified at two separate but linked levels: a traditional cryptographic description of the communication logic between network devices, and a state machine description that realises the former in each single device. Current formal verification efforts focus mainly on communication logic. We present detailed formal models of the protocol at both levels, provide precise specifications of its security properties, and analyse machine-checked proofs in ProVerif and ASMETA. The integrated analysis of the above two models is particularly novel, enabling us to identify and address several issues in the current IEEE 802.11 specification more thoroughly than would have been possible otherwise, leading to several official revisions of the standard.

Figures (6)

• Figure 1: SAE protocol in WPA3 ieee802.11:2020 as specified in the standard. $A$ and $B$ share the secret password $w$ and computed $\mathrm{PE}$ in private; $\mathrm{PE} \in \mathbb{G}$ and $\mathbb{G}$ is a subgroup of $\mathbb{Z}^{\star}_p$ of order $q$; $i$ is a counter. $B$ is symmetric to $A$ and thus omitted for brevity.
• Figure 2: State machine instantiating the SAE protocol in WPA3 ieee802.11:2020.
• Figure 3: The vanilla description of the SAE protocol.
• Figure 4: Scenario-based testing of the COM event when PI is in ACCEPTED state (simplified, showing first step of three).
• Figure 5: Replay attack at the design level specification of the WPA3-SAE protocol in IEEE 802.11:2020, the variant that uses finite field cryptography.