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.
翻译：ProVerif是一个广泛使用的安全协议核查员。 在内部,ProVerif使用Horn条款和这些条款的解析算法对协议进行抽象的表述,以证明协议的安全性质或发现攻击。在本文件中,我们概述了ProVerif,并讨论了其解析算法中与特定应用领域和ProVerif产生的特定条款有关的一些具体特点。本文是一份简短的摘要,为关于ProVerif的出版物提供了提示,读者将在其中找到更多细节。
相关内容
微信扫码咨询专知VIP会员