Sciweavers

Share
IFIP
2010
Springer

Secrecy and Authenticity Types for Secure Distributed Messaging

8 years 9 months ago
Secrecy and Authenticity Types for Secure Distributed Messaging
Abstract. We introduce a calculus with mobile names, distributed principals and primitives for secure remote communication, without any reference to explicit cryptography. The calculus is equipped with a system of types and effects providing static guarantees of secrecy and authenticity in the presence of a Dolev-Yao intruder. The novelty with respect to existing type systems for security is in the structure of our secrecy and authenticity types, which are inspired by the formulas of BAN Logic, and retain much of the simplicity and intuitive reading of such formulas. Drawing on these types, the type system makes it possible to characterize authenticity directly as a property of the data exchanged during a protocol rather than indirectly by extracting and interpreting the effects the protocol has on that data.
Michele Bugliesi, Stefano Calzavara, Damiano Maced
Added 18 May 2011
Updated 18 May 2011
Type Journal
Year 2010
Where IFIP
Authors Michele Bugliesi, Stefano Calzavara, Damiano Macedonio
Comments (0)
books