AbadiBlanchetJACM7037
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
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
Links
Official ACM version (you can download the full text from there):
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
}
Analyzing security protocols with secrecy types and logic programs