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

Abstract : 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.
Type de document :
Article dans une revue
Foundations and Trends® in Privacy and Security , Now publishers inc, 2016, 1 (1-2), pp.1 - 135. 〈10.1561/3300000004〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01423760
Contributeur : Bruno Blanchet <>
Soumis le : samedi 31 décembre 2016 - 13:56:49
Dernière modification le : mercredi 2 mai 2018 - 08:46:07
Document(s) archivé(s) le : samedi 1 avril 2017 - 12:06:17

Fichier

proverif.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends® in Privacy and Security , Now publishers inc, 2016, 1 (1-2), pp.1 - 135. 〈10.1561/3300000004〉. 〈hal-01423760〉

Partager

Métriques

Consultations de la notice

91

Téléchargements de fichiers

242