BlanchetBook09

Back to ProVerif

Bruno Blanchet. Using Horn Clauses for Analyzing Security Protocols. In Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 86-111. IOS Press, March 2011. Survey

Get the paper

.pdf, 261 Kb

Links

The book at IOS Press

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.

Bibtex


@INCOLLECTION{BlanchetBook09,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Using {H}orn Clauses for Analyzing Security Protocols},
  BOOKTITLE = {Formal Models and Techniques for Analyzing Security Protocols},
  PUBLISHER = {IOS Press},
  PAGES = {86--111},
  VOLUME = 5,
  SERIES = {Cryptology and Information Security Series},
  MONTH = MAR,
  YEAR = 2011,
  EDITOR = {V{\'e}ronique Cortier and Steve Kremer},
  ISBN = {978-1-60750-713-0}
}