AI 中文总结
本文形式化研究无线通信中基于配对的隐私攻击的根本原因，通过对Wi-Fi P2P和蓝牙低功耗的建模提出解决方案，获相关组织认可，为隐私保护无线协议发展铺路。
AI 中文摘要
随着来自社交媒体、物联网设备等隐私敏感数据的激增，迫切需要形式化的自动化方法来评估这些复杂系统内的隐私风险。本文形式化研究了无线通信中利用重放/中继技术的基于配对的隐私威胁的根本来源。我们的研究利用了条件无关响应、重放抗性和距离边界措施，这些对于使用共享密钥和允许列表进行认证重连接的协议至关重要。特别是，本文对著名无线网络进行了形式化建模，如Wi-Fi P2P持久组形成和蓝牙低功耗重连接过程，以说明根本原因和对策。我们的模型针对关联推理攻击以及现有的良好认证、帧不透明和无失步的形式化方法严格验证了所提出的解决方案。随后的分析不仅揭示了无线通信中未知的隐私领域，还识别了新旧漏洞。我们提出的设计变更已得到Wi-Fi联盟和蓝牙技术联盟（Bluetooth SIG）的认可，为未来弹性、隐私保护的无线协议的进步铺平了道路。
英文摘要
With the surge in privacy-sensitive data from sources such as social media and IoT devices, there is a pressing need for formal, automated methods to assess privacy risks within these intricate systems. This paper formally investigates root sources of pairing-based privacy threats exploited using replay/relay techniques in wireless communication. Our research harnesses condition-oblivious responses, replay-resistance, and distance bounding measures vital for protocols utilizing shared keys in allowlists for authenticated reconnections. Particularly, the paper uses formal modeling of notable wireless networks, like the Wi-Fi P2P persistent group formation and the Bluetooth Low Energy reconnection procedure, to illustrate the root causes and countermeasures. Our model rigorously validates the proposed solution against association inference attacks, along with existing formalizations of well-authentication, frame opacity, and no-desynchronization. The ensuing analysis reveals not only uncharted privacy realms in wireless communication but also identifies old and new vulnerabilities. Our proposed design changes are acknowledged by Wi-Fi Alliance and Bluetooth SIG, paving the way for future advancements in resilient, privacy-preserving wireless protocols.
