Bruno Blanchet Back to publications
Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002), pages 33-44, Portland, Oregon, January 2002. ACM Press.


Copyright© 2002 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 permissions@acm.org.

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

Get the paper

.ps.gz, 151 Kb


Slides of the talk.


We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.


  AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet},
  TITLE = {Analyzing {S}ecurity {P}rotocols with {S}ecrecy {T}ypes and {L}ogic {P}rograms},
  BOOKTITLE = {29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002)},
  PAGES = {33--44},
  YEAR = {2002},
  ADDRESS = {Portland, Oregon},

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)