本文针对无线通信协议中基于配对（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官方认可，为未来构建更具韧性的隐私保护无线协议铺平了道路。本文适合无线安全研究者、协议设计人员以及物联网隐私工程师阅读，以了解如何运用形式化方法从根源上消除配对过程中的隐私泄露风险。

本论文针对 EMV 非接触式支付系统中存在的中继攻击（relay attack）问题展开研究。中继攻击允许攻击者在持卡人与读卡器之间转发消息，从而在用户不知情的情况下完成支付，例如通过无线方式窃取资金。论文首先评估了现有的防护措施：Apple Pay 要求用户指纹或 Face ID 授权；Mastercard 和 Visa 则提出了基于时间或加密的协议来阻止中继。作者发现，在交通支付模式下，可以利用中继绕过 Apple Pay 的锁屏，从已锁定的 iPhone 向任意 EMV 读卡器非法支付任意金额，无需用户授权。此外，Visa 提出的中继对抗措施可被 root 后的智能手机绕过。对于 Mastercard 的防护，作者指出其时间限制在 ISO 14443 协议层实施比在 EMV 协议层更可靠。基于这些发现，论文提出了一种新的中继抵抗协议 L1RP（Layer 1 Relay Protection），并利用 Tamarin 证明器对手机支付（含或不含用户认证）的不同模式进行建模，形式化验证了 Apple 和 Visa 建议（Samsung 采用）的解决方案，并证明 L1RP 能够有效抵御中继攻击。该研究为改进非接触式支付安全提供了重要理论和实践依据。