WCDCAnalyzer: Scalable Security Analysis of Wi-Fi Certified Device Connectivity Protocols

are designed to interact with Wi-Fi Protected Access (WPA) protocols and play a crucial role in enabling devices to connect and communicate with each other and with applications across the Internet. Although the Wi-Fi Alliance designs both WPA and WCDC protocols, they differ significantly in their pairing processes. Some WCDC protocols, such as WI-FI DIRECT [2] , have been widely adopted and are included in Android and Linux systems [3], [4] and have been deployed in over 3 billion devices [3] . For such a widely deployed protocol, it is crucial to ensure the security and privacy of the protocol design. Prior works and problem. In terms of prior research on the security and privacy of WCDC protocols, there is a notable lack of preliminary efforts to analyze the security and privacy of these protocols. This gap can be attributed to several factors. First, the complexity of protocols like WI-FI DIRECT poses significant challenges for analysis. Second, these protocols are relatively newer compared to WPA, leading to less scrutiny in academic research. In a broader context, previous work [5] adopts formal analysis of WPA2 four-way and group-key handshakes. Therefore, in this paper, we pose the following research question: Is it possible to develop a formal analysis framework to investigate the security and privacy properties of WCDC protocols comprehensively? To resolve this question, we design and develop WCDCAnalyzer, the first comprehensive formal analysis framework focusing on WI-FI DIRECT [2], WI-FI EASYCONNECT [6], and WI-FI EASYMESH [7]. These protocols serve different purposes, such as initial pairing or efficient data transfer. Since the initial pairing step plays a key role in the overall security, we choose these three protocols because they incorporate such processes. Challenges. The formal analysis of the WCDC protocols, especially WI-FI DIRECT, with state-of-the-art verification tools such as Tamarin [8], presents one critical roadblock: scalability. This is due to the large size and complexity of the WI-FI DIRECT protocol. In formal analysis, the complexity of computation typically scales quickly with the size of the protocol and the model, particularly for cryptographic protocols operating in adversarial environments [9] . Scalability poses a significant challenge in analyzing and verifying systems as they grow in size. The primary reason is the state explosion problem [10] , where the number of possible system states increases exponentially, resulting in a large state space and excessive memory consumption. An approach to addressing Abstract-The Wi-Fi Alliance has developed several device connectivity protocols-such as WI-FI DIRECT, WI-FI EASY-CONNECT, and WI-FI EASYMESH-that are integral to billions of devices worldwide. Given their widespread adoption, ensuring the security and privacy of these protocols is critical. However, existing research has not comprehensively examined the security and privacy aspects of these protocols' designs. To address this gap, we introduce WCDCAnalyzer (Wi-Fi Certified Device Connectivity Analyzer), a formal analysis framework designed to evaluate the security and privacy of these widely used Wi-Fi Certified Device Connectivity Protocols. One of the significant challenges in formally verifying the WI-FI DIRECT protocol is the scalability problem caused by the state explosion resulting from the protocol's large scale and complexity, which leads to an exponential increase in memory usage. To address this challenge, we develop a systematic decomposition method following the compositional reasoning paradigm and integrate it into WCDCAnalyzer. This allows WCDCAnalyzer to automatically decompose a given protocol into several sub-protocols, verify each sub-protocol separately, and combine the results. Our design is a practical application of compositional reasoning based on rigorous foundations, and we provide detailed algorithms showing how thisreasoning approach can be applied to cryptographic protocol verification. Using WCDCAnalyzer, we analyze these protocols and newly discover 10 vulnerabilities, including authentication bypass, privacy leakage, and DoS attacks. The vulnerabilities and associated practical attacks have been validated on commercial devices and acknowledged by the Wi-Fi Alliance. 1 "WCDC" is a collective term used to denote protocols developed by the Wi-Fi Alliance for various connection environments.