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