BlanchetDagstuhl00

Bruno Blanchet Back to publications
Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In Dagstuhl seminar Security through Analysis and Verification, December 2000.

Links

Seminar homepage: http://www.dagstuhl.de/00501/

Abstract

We develop a typed process calculus for security protocols in which types convey secrecy properties. We prove a secrecy theorem that shows that well-typed processes do not reveal their secrets. We focus on asymmetric communication primitives, especially on public-key encryption. These present special difficulties, partly because they rely on related capabilities (e.g., public and private keys) with different levels of secrecy and scopes. Their treatment constitutes the main novelty of this work.

Our type system can be applied to some small but subtle security protocols. For example, in the Needham-Shroeder public-key protocol (a standard test case), one might expect a certain nonce to be secret; however, the protocol fails to typecheck under the assumption that this nonce is secret. This failure is not a shortcoming of the type system: it manifests Lowe's attack on the protocol. On the other hans, a corrected version of the protocol does typecheck under the assumption. Our secrecy theorem yields the expected property in this case.

Bibtex


@INPROCEEDINGS{BlanchetDagstuhl00,
  AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet},
  TITLE = {Secrecy {T}ypes for {A}symmetric {C}ommunication},
  BOOKTITLE = {Dagstuhl seminar "Security through Analysis and Verification"},
  YEAR = 2000,
  MONTH = DEC
}


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