桥接理论与实践：面向 ProVerif 和 Tamarin 的可执行安全属性分类学
密码学与安全
2026-05-29 v1
摘要
安全性对依赖现代数字系统的方方面面至关重要。由于几乎所有数字交互都受互联网和密码协议的支配，这些协议必须作为可靠机制，确保诸如保密性和完整性等核心安全属性。对这些协议的形式化验证是 securing interconnected systems 的关键步骤。诸如 ProVerif 和 Tamarin 之类的工具被广泛用于执行自动化验证。然而，其有效使用需要专业的领域知识，这为 security protocol 设计者（他们通常拥有安全背景而非形式化验证背景）的学习曲线带来了挑战。因此，我们需要结构化、可及的资源来帮助协议设计者以形式化验证工具的语言表达其设计和要求。为此，我们引入了一个系统且基于证据的安全属性分类学。该分类学源于对 2022-2025 年间使用 ProVerif 和 Tamarin 的 53 项研究的文献综述，提供了最新验证属性的视角。我们系统性地对这些属性进行分类和定义，提供既适用于直观理解的非形式化定义，也适用于清晰性和一致性的严格形式定义（以一阶逻辑表达）。我们进一步详细阐述了建模模式并在 ProVerif 和 Tamarin 中实现可执行示例，收集于开放仓库中。本工作通过桥接理论安全属性定义与其实际可执行验证模型之间的差距，推动了技术前沿。
引用
@article{arxiv.2605.29465,
title = {Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin},
author = {Leonard Tudorache and Ivan Kurtev and Mark van den Brand},
journal= {arXiv preprint arXiv:2605.29465},
year = {2026}
}
备注
Under review at International Journal on Software and Systems Modeling (SoSyM)