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