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