The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm
Bruno Blanchet (Inria, Paris, France)
TL;DR
ProVerif is a widely used security protocol verifier that employs Horn clause resolution to analyze protocols, with this paper providing an overview and insights into its resolution algorithm and domain-specific features.
Contribution
This paper offers a concise overview of ProVerif and discusses the specifics of its Horn clause resolution algorithm tailored for security protocol analysis.
Findings
ProVerif effectively verifies security properties of protocols.
Horn clause resolution is central to ProVerif's analysis.
The paper highlights domain-specific adaptations of the algorithm.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.