Dynamic types for authentication

We propose a type and effect system for authentication protocols built upon a tagging scheme that formalizes the intended semantics of ciphertexts. The main result is that the validation of each component in isolation is provably sound and fully compositional: if all the protocol participants are independently validated, then the protocol as a whole guarantees authentication in the presence of Dolev-Yao intruders possibly sharing long term keys with honest principals. Protocol are thus validated in the presence of both malicious outsiders and compromised insiders. The highly compositional nature of the analysis makes it suitable for multi-protocol systems, where different protocols might be executed concurrently.