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

该论文研究端到端加密（E2EE）通信场景下有害媒体（如儿童性虐待材料 CSAM、恐怖主义内容等）的识别问题。由于 E2EE 保护用户隐私，服务提供商无法直接查看消息内容，因此需要在不破坏加密和隐私的前提下检测已知有害媒体。论文提出一种高效的私有成员计算方法，允许客户端或服务端在不泄露查询内容的前提下，判断某个媒体对象（如图片/视频的哈希值）是否存在于已知有害内容数据库中。核心贡献包括：设计轻量级密码学协议，将通信双方的计算与通信开销控制在可接受范围；给出与现有 E2EE 系统（如 Signal、WhatsApp 类架构）集成的接口方案；探讨误报（false positive）对用户隐私的影响，并分析抵御恶意客户端/服务端对抗行为的隐私保证。实验表明该方法在真实规模数据集上具有可行性，显著降低带宽与延迟开销。论文适合安全协议设计者、隐私保护技术研究员、以及负责内容审核策略的工程师阅读。

端到端加密 (E2EE) 消息应用常被视为安全通信的黄金标准，被广泛用于敏感场景下的群组协调，例如政治决策或企业机密讨论。随着 Threema、WhatsApp、Signal 和 iMessage 等主流应用相继引入群组投票功能，用户自然期望所有参与者能够看到一致的对话内容和相同的结果，这一属性被称为“记录本一致性”（Transcript Consistency, TC）。然而，本研究针对恶意参与者威胁模型，系统性地证明了当前主流 E2EE 应用在群聊场景中并不提供任何形式的 TC 保证。作者指出，恶意群成员可以不触发任何 UI 警告，就能对不同接收者选择性省略、重排或篡改消息内容，甚至影响跨设备同步的一致性。他们识别出多种“多义性”向量（equivocation vectors），涵盖协议回退路径以及群内故意使用的点对点传递通道。利用这些向量，攻击者可实施社会工程、绕过群组审核，并重点演示了操纵投票结果的场景。此外，研究还发现了若干实现相关的隐私问题，例如可通过群组行为进行设备操作系统指纹识别。论文在先前 TC 研究的基础上，将跨服务设计缺陷系统化，并提出了低开销的缓解措施，包括协议层面的完整性校验和 UI 中的信号提示策略，以帮助用户识别不一致状态。这项工作对依赖 E2EE 保证决策一致性的用户和产品设计者具有重要参考价值。