AbadiBlanchetSAS03
Bruno Blanchet
Back to publications
Martín Abadi and Bruno Blanchet.
Computer-Assisted Verification of a Protocol for
Certified Email.
In Radhia Cousot, editor, Static Analysis, 10th International
Symposium
(SAS'03),
volume 2694 of Lecture Notes in Computer Science, pages 316-335, San
Diego, California, June 2003. Springer.
Copyright
© Springer-Verlag.
Get the paper
.ps.gz, 95 Kb
Links
LNCS series home page. LNCS Volume 2694 at Springer.
Slides of the talk.
Abstract
We present the formalization and verification of a recent
cryptographic protocol for certified email. Relying on a tool for
automatic protocol analysis, we establish the key security properties
of the protocol. This case study explores the use of general
correspondence assertions in automatic proofs, and aims to demonstrate the
considerable power of the tool and its applicability to non-trivial,
interesting protocols.
Bibtex
@INPROCEEDINGS{AbadiBlanchetSAS03,
AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet},
TITLE = {Computer-{A}ssisted {V}erification of a {P}rotocol for {C}ertified {E}mail},
BOOKTITLE = {Static Analysis, 10th International Symposium (SAS'03)},
PAGES = {316--335},
YEAR = 2003,
EDITOR = {Radhia Cousot},
VOLUME = 2694,
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {San Diego, California},
MONTH = JUN,
PUBLISHER = {Springer}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)