Secrecy and Authenticity Types for Secure Distributed Messaging

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.