CryptoVampire:面向完全符号攻击者密码学模型的自动推理
密码学与安全
2024-04-08 v2 计算机科学中的逻辑
摘要
密码协议难以设计和证明正确,不断增长的(甚至针对协议标准的)攻击列表即为佐证。密码学的符号模型支持对此类协议针对理想化模型的自动化形式化安全证明,该模型抽象掉了密码方案的代数性质从而遗漏攻击。计算模型给出严格保证,但目前仅支持交互式证明和/或受限的协议类。一个有前景的方法由计算上完全符号攻击者(CCSA)给出,其在 BC Logic 中形式化,旨在桥接并兼取两者之长,通过符号分析获得密码学保证。BC Logic 由最近开发的交互式定理证明器 Squirrel 支持,它支持机器检验的交互式安全证明,而非自动化证明,因此需要专家知识。我们引入了 CryptoVampire 密码协议验证器,首次完全自动化了 BC Logic 中迹属性的证明。关键技术贡献是具有子项关系定制处理的一阶(FO)协议属性形式化。我们克服了高阶(HO)逻辑中交互式证明的负担,仅使用 FO 推理自动确立密码协议的正确性。在理论方面,我们限制带有密码学公理的完整 FO 逻辑,以确保在失去 HO BC Logic 表达力的同时不失去正确性。在实践方面,CryptoVampire 集成了使用 FO 饱和算法和启发式的专用证明技术,从而能够利用最先进的 Vampire FO 定理证明器作为底层证明引擎。我们的实验结果显示了 CryptoVampire 作为独立验证器的有效性,以及在为 Squirrel 提供自动化支持方面的表现。
引用
@article{arxiv.2305.12173,
title = {CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model},
author = {Simon Jeanteur and Laura Kovács and Matteo Maffei and Michael Rawson},
journal= {arXiv preprint arXiv:2305.12173},
year = {2024}
}