论文标题
安全协议验证者proverif及其号角分辨率算法
The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm
论文作者
论文摘要
Proverif是一种广泛使用的安全协议验证者。在内部，Proverif使用Horn子句对协议的抽象表示以及在这些子句上的分辨率算法，以证明协议的安全属性或找到攻击。 在本文中，我们介绍了鄙视的概述，并讨论了其分辨率算法的一些特殊性，该算法与特定的应用程序域以及Proverif生成的特定条款有关。本文是一个简短的摘要，可以使关于Proverif的出版物提供指示，其中读者将找到更多细节。
ProVerif is a widely used security protocol verifier. Internally, ProVerif uses an abstract representation of the protocol by Horn clauses and a resolution algorithm on these clauses, in order to prove security properties of the protocol or to find attacks. In this paper, we present an overview of ProVerif and discuss some specificities of its resolution algorithm, related to the particular application domain and the particular clauses that ProVerif generates. This paper is a short summary that gives pointers to publications on ProVerif in which the reader will find more details.
