该论文聚焦于一个长期存在的安全工程问题：即时通信协议的「形式化规范保证」与「实际运行实现行为」之间存在落差。Signal 协议为数以十亿计的用户提供加密通信，是 WhatsApp（全球用户量最大的消息应用）与 Signal 官方客户端的底层协议；学界已在计算模型与 Dolev-Yao 符号模型下对该协议给出大量强安全证明，但这些证明只覆盖协议规范本身，无法说明真实客户端在运行时是否严格按模型执行。作者的工作是填补这一差距：采用新近提出的运行时监控器 SpecMon，对实际观测到的执行轨迹进行一致性检查，判断其是否符合形式化协议模型。为此，作者对两个真实应用（WhatsApp Web 与 Signal Desktop）进行插桩，捕获它们与网络层及密码学组件之间的交互事件；在可信事件抽取的前提上，把运行时行为抽象为符号层，再据此构建两个与 Tamarin 兼容的多重集重写（multiset-rewrite）模型以便形式化验证。论文给出了首个 WhatsApp Web 上 Signal 协议实现的模型，以及迄今为止最详细的 Signal 原始协议模型。监控结果显示，在给定的抽取与符号抽象假设下，观测到的执行符合这些模型，并对 Signal 协议的核心组件验证了认证性与机密性属性。值得注意的是，监控还暴露出原始 libsignal 库与 WhatsApp 分支之间此前未被文档记录的行为差异。作者同时评估了方法的可复现性与实用性：完成 WhatsApp Web 建模、应用插桩、加入模糊测试并运行实验共耗时三个人周；实验表明可对真实应用进行高效监控，并能检测人为注入的安全故障，在其实测环境中开销较低。

本文针对 WhatsApp 的握手协议（Prekey 机制）进行了安全与隐私分析。研究背景是端到端加密通信中密钥协商的安全重要性。论文核心问题包括：Prekey 交换是否存在信息泄露、是否可被中间人攻击利用、以及隐私保护是否充分。方法上，作者对 WhatsApp 实际部署的握手流程进行了逆向工程和形式化建模，结合密码学分析工具评估其安全属性。主要贡献包括：发现了 Prekey 签名验证中的遗留问题、揭示了服务器侧 Prekey 管理可能导致的用户身份绑定弱点，并提出了改进方案。实验在模拟环境中验证了攻击场景，证明这些漏洞可被远程利用。该研究适合密码学和安全协议研究人员、即时通讯开发者和隐私倡导者阅读。

本论文研究了全球最大即时通讯平台 WhatsApp 的电话号码枚举漏洞。WhatsApp 拥有超过 35 亿活跃用户（截至 2025 年初），其通讯录同步机制允许用户通过手机号查询联系人是否注册。该机制虽为合法功能，但本质上为攻击者提供了枚举有效手机号的能力。作者通过大规模实验证明，WhatsApp 的速率限制措施存在严重不足，能够以每小时超过 1 亿次的速率进行探测而不被阻止。研究发现，2021 年 Facebook 数据泄露中披露的近一半电话号码在 WhatsApp 上仍处于活跃状态，凸显了数据泄露的长期风险。此外，作者还进行了用户普查，揭示了即使消息内容经过端到端加密，元数据（如用户活跃状态和关联设备）仍可能被大规模收集。更关键的是，发现了不同设备或电话号码之间重复使用 X25519 公钥的现象，这可能是由于不安全的自定义实现或欺诈活动导致。论文最后描述了与 WhatsApp 团队的协作修复过程，确认了速率限制问题已得到解决。该研究适合安全研究人员、隐私倡导者及即时通讯平台开发者阅读。