| Bruno Blanchet |  |
 |
Date de l'exposé : 6 janvier 2006
An Automatic Security Protocol Verifier based on ResolutionTheorem Proving
We present a technique for the verification of cryptographic protocols, based on an abstract representation of the protocol by a set of Horn clauses, and on a resolution algorithm on these clauses. This technique allows a flexible encoding of many cryptographic primitives. It can verify a wide range of security properties of the protocols, such as secrecy, authenticity, and limited cases of process equivalences, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol, in parallel or not.
