Authenticity by tagging and typing

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. The highly compositional nature of the analysis makes it suitable for multi-protocol systems, where different protocols might be executed concurrently. Categories and Subject Descriptors C.2.2 [Computer-Communication Networks]: Network Protocols—Protocol Verification; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Program Analysis; K.6.5 [Management of Computing and Information Systems]: Security and Protection—Authentication General Terms Security, Verification Keywords Static Analysis, Authentication, Process Calculi

• Type: Conference
• Year: 2004
• Where: CCS
• Authors: Michele Bugliesi, Riccardo Focardi, Matteo Maffei
• Keywords: Authentication Protocols, CCS 2004, Guarantees Authentication, Intended Semantics, Security Privacy