BlanchetDagstuhl03b
Bruno Blanchet
Back to publications
Bruno Blanchet.
Automatic Proof of Strong Secrecy for Security
Protocols.
In Dagstuhl seminar Language-Based Security, October 2003.
Links
Seminar homepage: http://www.dagstuhl.de/03411/
Abstract
We present a new automatic technique for proving strong secrecy for
security protocols. Strong secrecy means that an adversary cannot see
any difference when the value of the secret changes. Strong secrecy
detects implicit flows and flows of partial information. It is a
particular case of observational equivalence, which gives nice
compositionality properties and makes it easier to combine manual and
automatic proofs. Our technique relies on an automatic translation of
the protocol into Horn clauses, and a resolution algorithm on the
clauses. It requires important extensions with respect to previous
work for (syntactic) secrecy and authenticity. This technique can
handle a wide range of cryptographic primitives, and yields proofs
valid for an unbounded number of sessions and an unbounded message
space; it is also flexible and efficient. We have proved its
correctness, its termination on the large class of tagged protocols,
and implemented it.
Bibtex
@INPROCEEDINGS{BlanchetDagstuhl03b,
AUTHOR = {Bruno Blanchet},
TITLE = {Automatic {P}roof of {S}trong {S}ecrecy for {S}ecurity {P}rotocols},
BOOKTITLE = {Dagstuhl seminar "Language-Based Security"},
YEAR = 2003,
MONTH = OCT
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)