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

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-)