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

该论文针对证书透明化（Certificate Transparency, CT）这一已被所有主流浏览器支持的 TLS 证书生态机制，重新梳理其安全目标并给出严格的形式化分析。CT 的设计初衷是降低对证书颁发机构（CA）的信任依赖：所有 CA 必须把签发的证书写入公开日志，并由第三方监控方对日志的合规性与一致性进行检查。整个体系涉及 CA、日志运营方（logger）、监控方（monitor）以及终端用户客户端四个角色，彼此之间存在复杂的校验关系，因此很难精确说明 CT 究竟如何在引入复杂基础设施的代价下消除信任假设。作者指出，此前在 Dolev-Yao 符号模型与计算模型下的分析都只使用了高度简化的模型，并且其安全定义是为 CA 量身定制的，抓取到的其实是设计特性而非真正要保证的目标属性。本文主张把「可问责性（accountability）」确立为 CT 的核心目标，并在 Dolev-Yao 模型中展开系统性分析：先从传统 PKI 出发，逐层过渡到 CT，再进一步分析针对 SCT 审计（SCT Auditing）与 Gossiping 的扩展提案。分析结论表明，朴素 CT 方案在「日志诚实」的假设下才能提供可问责性，即它仍依赖一个诚实日志；SCT 审计扩展可以消除这一假设，而 Gossiping 扩展则无法消除该假设。该工作为理解 CT 及其扩展的真实信任边界提供了更精确的密码协议层面依据。

本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅在攻击收益为正时发起攻击。作者将攻击动作赋予成本、将破坏安全目标赋予奖励，并在加权交替时序逻辑（WATL）中定义“理性安全”属性：不存在能使理性入侵者获得严格正效用的违规策略。针对有限成本标注并发博弈结构上的有界理性入侵者，论文证明该验证问题是可判定的，给出了复杂度特征，并证明其严格细化 DY 安全性：某些协议在 DY 模型下不安全但在理性模型下安全，二者之间存在一个可计算的阈值。作者通过两个对比性用例展示框架：一是在会话不确定下的认证支付协议，理性入侵者需在不可区分的会话间策略性行动，其不完美信息会提高设计者需要定价的防御成本；二是无密码学方案的 ThreeBallot 投票协议，通过计算贿赂与收益的比率，指出低于该比率时理性胁迫者不会发动攻击。该工作为协议安全性评估提供了更贴近真实攻击者动机的决策框架，适合安全协议设计者、形式化验证研究者及博弈论与安全交叉领域学者阅读。

这篇 arXiv 论文提出了一套用于在计算模型下对安全协议进行机械化验证的框架和交互式证明器。研究背景是：安全协议设计的正确性至关重要，需要坚实的数学基础和计算机辅助方法。此前 Bana 和 Comon 提出的形式化方法只能分析固定会话数目的协议，且缺乏对证明机械化的支持。本文的核心贡献是开发了一个元逻辑（meta-logic）及相应的证明系统，用于推导安全性质，能够处理任意会话数目的协议。该证明系统中的证明仅涉及协议执行的高层符号表示，类似于符号模型中的证明，但提供的安全保证位于计算层面（即计算模型中的安全性质）。作者将该方法实现为一个新的交互式证明器 Squirrel，输入是应用 pi-演算（applied pi-calculus）描述的协议，并开展了多个案例研究，覆盖多种密码原语（哈希、加密、签名、Diffie-Hellman 指数运算）和安全性质（认证、强保密、不可关联性）。该工作的主要意义在于弥合了符号模型与计算模型之间的差距，使安全分析者能够在符号层面高效推理，同时获得计算层面的强安全保证。适合对形式化验证、密码协议安全性分析感兴趣的研究人员和安全工程师阅读。

本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和 AlphaProof 启发，作者设计了一个无状态的 API，将 Tamarin 转化为经典 RL 环境，并通过蒙特卡洛树搜索（MCTS）结合神经网络启发式学习已完成子证明的模式。在 16 个案例研究（包括经典协议模型及最新发表中的复杂协议模型）上，该方法比 Tamarin 标准搜索自动找到更多证明，且生成的证明比标准启发式甚至人工编写的启发式更短。该框架可直接用于帮助 Tamarin 用户减少人工努力，同时提供标准化的程序化接口。实验结果表明，RL 方法在协议形式化验证领域具有巨大潜力。