本文针对无线通信协议中基于配对（pairing）的隐私攻击进行形式化建模与缓解研究。随着社交媒体和物联网设备产生大量隐私敏感数据，亟需形式化、自动化的方法来评估复杂系统中的隐私风险。作者首先指出，利用重放/中继（replay/relay）技术实现的关联推断（association inference）攻击，其根源在于协议设计中对条件无关响应（condition-oblivious responses）、重放抵抗（replay-resistance）和距离边界（distance bounding）等安全属性的缺失。文章以Wi-Fi P2P持久组建立过程和蓝牙低功耗（BLE）重连流程为例，形式化建模了这两类典型无线网络协议，并系统分析了协议中共享密钥允许列表（allowlist）用于认证重连时的隐私弱点。作者提出了针对关联推断攻击的协议设计改进方案，并通过模型验证证明了该方案满足已有的认证（well-authentication）、帧不可见性（frame opacity）和无失步（no-desynchronization）等安全属性。分析结果不仅揭示了无线通信中尚未被充分探索的隐私问题，还发现了新旧多种漏洞。所提出的设计变更已被Wi-Fi联盟和蓝牙SIG官方认可，为未来构建更具韧性的隐私保护无线协议铺平了道路。本文适合无线安全研究者、协议设计人员以及物联网隐私工程师阅读，以了解如何运用形式化方法从根源上消除配对过程中的隐私泄露风险。