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

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