Cryptographic protocols are extremely hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Using the symbolic model of cryptography, protocols are proven correct against an idealized cryptographic model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. On the other hand, existing computational models of cryptography only support interactive proofs and/or are limited to stateless protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA) model, formalized in the BC logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic protocol analysis. While machine-checked security proofs are provided in this domain, such efforts require expert knowledge both in the cryptographic space as well as on the reasoning side. In this paper, we present the CryptoVampire framework, providing the first fully automated setting for deriving proofs of trace properties in the BC logic. CryptoVampire brings a first-order formalization of protocol properties, by proposing tailored handling of subterm relations. In addition, CryptoVampire implements specialized reasoning techniques, saturation algorithms, and heuristics, allowing the direct integration of CryptoVampire within the landscape of automated theorem proving. Our experimental results showcase the effectiveness of CryptoVampire, providing also automation support for existing approaches in the area.

翻译：密码协议的设计与正确性证明极为困难，即便是协议标准也面临日益增长的攻击案例。利用符号密码学模型，协议可在理想化密码模型中得到正确性证明，但该模型抽象了密码方案的代数性质，从而遗漏了部分攻击。另一方面，现有的计算密码学模型仅支持交互式证明和/或局限于无状态协议。BC逻辑形式化的计算完备符号攻击者（CCSA）模型为这一难题提供了创新方案，旨在融合并汲取两类模型的优势，通过符号协议分析获得密码学安全保障。尽管该领域已实现机器验证的安全证明，但此类尝试同时需要密码学与推理领域的专家知识。本文提出CryptoVampire框架，首次实现了BC逻辑中迹属性的全自动化推导证明。通过提出子项关系的定制化处理方法，CryptoVampire实现了协议属性的一阶形式化。此外，该框架集成了专门推理技术、饱和算法与启发式策略，可无缝融入自动化定理证明生态系统。实验结果表明，CryptoVampire在提升现有方法自动化支持能力的同时，展现出卓越的有效性。