Using Horn Clauses for Analyzing Security Protocols

Bruno Blanchet 1
1 CASCADE - Construction and Analysis of Systems for Confidentiality and Authenticity of Data and Entities
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : This chapter presents a method for verifying security protocols based on an abstract representation of protocols by Horn clauses. This method is the foundation of the protocol verifier ProVerif. It is fully automatic, efficient, and can handle an unbounded number of sessions and an unbounded message space. It supports various cryptographic primitives defined by rewrite rules or equations. Even if we focus on secrecy in this chapter, this method can also prove other security properties, including authentication and process equivalences.
Type de document :
Chapitre d'ouvrage
Véronique Cortier; Steve Kremer. Formal Models and Techniques for Analyzing Security Protocols, 5, IOS Press, pp.86 - 111, 2011, Cryptology and Information Security Series, 978-1-60750-713-0. 〈10.3233/978-1-60750-714-7-86〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01110425
Contributeur : Brigitte Briot <>
Soumis le : mercredi 28 janvier 2015 - 10:45:04
Dernière modification le : jeudi 11 janvier 2018 - 01:49:23

Identifiants

Collections

Citation

Bruno Blanchet. Using Horn Clauses for Analyzing Security Protocols. Véronique Cortier; Steve Kremer. Formal Models and Techniques for Analyzing Security Protocols, 5, IOS Press, pp.86 - 111, 2011, Cryptology and Information Security Series, 978-1-60750-713-0. 〈10.3233/978-1-60750-714-7-86〉. 〈hal-01110425〉

Partager

Métriques

Consultations de la notice

71