What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
This work addresses security vulnerabilities in Wi-Fi authentication for WPA3-Personal networks, though it is incremental as it builds on existing verification efforts.
The researchers conducted a formal security analysis of the WPA3 SAE wireless authentication protocol by creating detailed models at both communication logic and state machine levels, which identified several issues in the IEEE 802.11 specification and led to official revisions of the standard.
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.