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.

翻译：最新Wi-Fi安全标准IEEE 802.11包含名为SAE的安全认证协议，该协议在WPA3个人网络中被强制使用。该协议在两个独立但又相互关联的层面上进行规范：网络设备间通信逻辑的传统密码学描述，以及在各设备中实现前述逻辑的状态机描述。当前形式化验证工作主要聚焦于通信逻辑层面。我们提出了两个层面的协议详细形式化模型，给出了其安全属性的精确规范，并在ProVerif与ASMETA中完成了机器验证证明。上述两个模型的集成分析具有特别的新颖性，使我们能够比以往更全面地识别并解决当前IEEE 802.11标准中的若干问题，最终推动该标准完成多次官方修订。