AbadiBlanchetJACM7037

Bruno Blanchet Back to publications
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.

Copyright

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

Abstract

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.

Bibtex


@ARTICLE{AbadiBlanchetJACM7037,
  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},
  MONTH = JAN
}


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