Dynamic types for authentication*

• DOI: 10.3233/jcs-2007-15602
• Publication Date: 2016-05-18T07:37:28Z
• Authors: Michele Bugliesi; Riccardo Focardi; Matteo Maffei
• Keywords: Component (thermodynamics); Isolation

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