Bruno Blanchet Back to publications
Bruno Blanchet. Automatic Verification of Cryptographic Protocols: A Logic Programming Approach (invited talk). In 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pages 1-3, Uppsala, Sweden, August 2003. ACM.


Copyright© 2003 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page or intial screen of the document. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept., ACM Inc., fax +1 (212) 869-0481, or

If you agree with this copyright notice, you can get the paper:

Get the paper

.ps.gz, 74 Kb, .pdf, 69 Kb


Official ACM version:

ACM DL Author-ize serviceAutomatic verification of cryptographic protocols: a logic programming approach
Bruno Blanchet
PPDP '03 Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, 2003

Slides of the talk.


We present a technique for cryptographic protocol verification, based on an intermediate representation of the protocol by a set of Horn clauses (a logic program). This technique makes it possible to verify security properties of the protocols, such as secrecy and authenticity, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol.


  AUTHOR = {Bruno Blanchet},
  TITLE = {Automatic {V}erification of {C}ryptographic {P}rotocols:
{A} {L}ogic {P}rogramming {A}pproach (invited talk)},
  BOOKTITLE = {5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03)},
  PAGES = {1--3},
  YEAR = {2003},
  ADDRESS = {Uppsala, Sweden},

E-mail/Courrier électronique : (remove trap-)