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.


© Springer-Verlag.

Get the paper

.ps.gz, 95 Kb


LNCS series home page. LNCS Volume 2694 at Springer.

Slides of the talk.


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.


  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},
  PUBLISHER = {Springer}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)