本文针对安全协议设计中的正确性验证问题，提出了一种在计算模型下对任意会话数进行协议证明的交互式证明框架。作者在Bana和Comon等人先前工作的基础上进行了扩展，原始工作只能分析固定会话数且缺乏证明机械化支持。论文首先定义了一个元逻辑以及相应的证明系统，用于推导安全属性。该证明系统仅处理协议执行的高层符号表示，类似于符号模型中的证明，但能够提供计算级别的安全保证。作者实现了这一方法，构建了名为Squirrel的交互式证明器，其输入是用应用π演算描述的协议。通过多个案例研究，覆盖了哈希、加密、签名、Diffie-Hellman指数运算等原语，以及认证、强机密性、不可链接性等安全属性，验证了该方法的有效性和通用性。该工作弥合了符号模型与计算模型之间的鸿沟，为协议安全性提供了可机械化验证的计算级保证，适用于协议设计者和形式化验证研究人员。