Paper
What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication
Authors
Roberto Metere, Mario Lilli, Luca Arnaboldi, Elvinia Riccobene
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2603.23352v1</id>\n <title>What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication</title>\n <updated>2026-03-24T15:54:05Z</updated>\n <link href='https://arxiv.org/abs/2603.23352v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2603.23352v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.CR'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.NI'/>\n <published>2026-03-24T15:54:05Z</published>\n <arxiv:comment>16 pages, 6 figures, 2 tables</arxiv:comment>\n <arxiv:primary_category term='cs.CR'/>\n <author>\n <name>Roberto Metere</name>\n </author>\n <author>\n <name>Mario Lilli</name>\n </author>\n <author>\n <name>Luca Arnaboldi</name>\n </author>\n <author>\n <name>Elvinia Riccobene</name>\n </author>\n </entry>"
}