Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

By Bruno Blanchet. Found. Trends Priv. Secur., 2016

401 citations recorded by the source corpus.

ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses. This survey presents an overview of the research on ProVerif.

Subfields: Artificial Intelligence, Computer Networks and Communications, Information Systems

View Paper: https://www.semanticscholar.org/paper/27e1b5062cd36e9bfefb94e109784d698b964479

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Information Systems

Citations in the corpus

A Formal Analysis of 5G Authentication (2018, methodology): “However, in addition to using the same aforementioned abstractions and simplifications, they only used ProVerif to check if specific trace executions correspond to attack traces.”