有限变体性质自动验证：超越收敛等式理论
密码学与安全
2024-10-22 v1
摘要
计算机辅助安全协议分析深植于等式理论之中，用以建模密码学原语。大多数针对满足有限变体性质 (FVP) 的等式理论的自动化验证工具，要求证明 FVP 或至少提供作为 E-收敛重写系统的表示，其中 E 最多为单参数的关联交换 (AC) 函数符号的等式理论。其中，ProVerif 因能在无需表示的情况下自动证明 FVP 而可能为唯一例外，但仅适用于小类等式理论。在本工作中，我们提出一种新型半决策程序，用于在无需特定表示的情况下证明 FVP，适用于超越由 E-收敛重写系统表达的等式理论类。我们实现了原型系统并成功应用于多个文献中的理论。
引用
@article{arxiv.2410.15289,
title = {Automatic verification of Finite Variant Property beyond convergent equational theories},
author = {Vincent Cheval and Caroline Fontaine},
journal= {arXiv preprint arXiv:2410.15289},
year = {2024}
}
备注
Extended version of the conference paper accepted at CSF 2025