WPA3 SAE 无线认证的形式化安全分析
密码学与安全
2026-03-25 v1 网络与互联网体系结构
摘要
最新 Wi-Fi 安全标准 IEEE 802.11 包含一种称为 SAE 的安全认证协议，其在 WPA3-Personal 网络中使用为强制性。该协议在两个相互关联但独立的层级上被规定：网络设备间通信逻辑的传统密码学描述，以及在每个单一设备中实现前者的状态机描述。当前形式化验证工作主要关注通信逻辑。我们提供了这两个层级的详细形式化模型，对其安全属性给出了精确定义，并在 ProVerif 和 ASMETA 中分析了机器验证证明。对上述两个模型的综合分析尤为新颖，使我们能够比仅分析单一模型更彻底地识别并解决当前 IEEE 802.11 规范中的若干问题，从而导致了该标准的若干官方修订。
引用
@article{arxiv.2603.23352,
title = {What a Mesh: Formal Security Analysis of WPA3 SAE Wireless Authentication},
author = {Roberto Metere and Mario Lilli and Luca Arnaboldi and Elvinia Riccobene},
journal= {arXiv preprint arXiv:2603.23352},
year = {2026}
}
备注
16 pages, 6 figures, 2 tables