AbadiBlanchetSCP04
Bruno Blanchet
Back to publications
Martín Abadi and Bruno Blanchet.
Computer-Assisted Verification of a Protocol for
Certified Email.
Science of Computer Programming, 58(1-2):3-27, October 2005.
Special issue SAS'03.
Copyright
© Elsevier Science B.V.
Get the paper
.ps.gz, 191 Kb
Links
doi:10.1016/j.scico.2005.02.002
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
@ARTICLE{AbadiBlanchetSCP04,
AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet},
TITLE = {Computer-{A}ssisted {V}erification of a {P}rotocol for {C}ertified {E}mail},
JOURNAL = {Science of Computer Programming},
YEAR = 2005,
VOLUME = 58,
NUMBER = {1--2},
PAGES = {3--27},
MONTH = OCT,
NOTE = {Special issue SAS'03.}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)