Back to ProVerif
Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102-146, January 2005. Tool feature


Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

Get the paper

.ps.gz, 178 Kb, .pdf, 450 Kb


Official ACM version (you can download the full text from there):

ACM DL Author-ize serviceAnalyzing security protocols with secrecy types and logic programs
Martín Abadi, Bruno Blanchet
Journal of the ACM (JACM), 2005


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},
  JOURNAL = {Journal of the ACM},
  YEAR = 2005,
  VOLUME = 52,
  NUMBER = 1,
  PAGES = {102--146},