Date Added: May 2010
This paper 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 the authors focus on secrecy in this paper, this method can also prove other security properties, including authentication and process equivalences.