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

TL;DR

This paper provides a comprehensive formal security analysis of the WPA3 SAE wireless authentication protocol, combining models of communication logic and state machines to identify issues and improve the standard.

Contribution

It introduces detailed formal models at two levels and integrates their analysis, leading to the discovery of security issues and influencing official standard revisions.

Findings

Identification of security issues in the IEEE 802.11 SAE protocol

Formal verification of protocol properties using ProVerif and ASMETA

Contributions to standard revisions based on analysis results

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.