An Interactive Prover for Protocol Verification in the Computational Model.

这篇 arXiv 论文提出了一套用于在计算模型下对安全协议进行机械化验证的框架和交互式证明器。研究背景是：安全协议设计的正确性至关重要，需要坚实的数学基础和计算机辅助方法。此前 Bana 和 Comon 提出的形式化方法只能分析固定会话数目

历史摘要 · 未重新核验 · IEEE S&P