安全协议验证器 ProVerif 及其 Horn 子句消解算法
密码学与安全
2022-11-23 v1
摘要
ProVerif 是一种广泛使用的安全协议验证器。在内部，ProVerif 使用 Horn 子句对协议进行抽象表示，并对这些子句使用消解算法，以证明协议的安全属性或发现攻击。在本文中，我们概述 ProVerif 并讨论其消解算法的一些特性，这些特性与 ProVerif 所生成的特定应用领域和特定子句相关。本文是一篇简短的综述，为读者提供关于 ProVerif 的出版物索引，其中可找到更多细节。
引用
@article{arxiv.2211.12227,
title = {The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm},
author = {Bruno Blanchet},
journal= {arXiv preprint arXiv:2211.12227},
year = {2022}
}
备注
In Proceedings HCVS/VPT 2022, arXiv:2211.10675