BlanchetPPDP03
Back to ProVerif
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. Survey
Copyright
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 permissions@acm.org.
If you agree with this copyright notice, you can get the paper:
Get the paper
.ps.gz, 74 Kb, .pdf, 69 Kb
Links
Official ACM version (you can download the full text from there):
Slides of the talk.
Abstract
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.
Bibtex
@INPROCEEDINGS{BlanchetPPDP03,
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},
MONTH = AUG,
PUBLISHER = {ACM}
}
Automatic verification of cryptographic protocols: a logic programming approach