Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif

Abstract : After giving general context on the verification of security protocols, we focus on the automatic symbolic protocol verifier ProVerif. This verifier can prove secrecy, authentication, and observational equivalence properties of security protocols, for an unbounded number of sessions of the protocol. It supports a wide range of cryptographic primitives defined by rewrite rules or by equations. The tool takes as input a description of the protocol to verify in a process calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol into an abstract representation of the protocol by Horn clauses, and determines whether the desired security properties hold by resolution on these clauses.
Type de document :
Chapitre d'ouvrage
Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.54-87, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. 〈10.1007/978-3-319-10082-1_3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01102136
Contributeur : Bruno Blanchet <>
Soumis le : lundi 12 janvier 2015 - 10:38:02
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

Collections

Citation

Bruno Blanchet. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.54-87, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. 〈10.1007/978-3-319-10082-1_3〉. 〈hal-01102136〉

Partager

Métriques

Consultations de la notice

135