Dynamic types for authentication^*

Issue title: Formal Methods in Security Engineering Workshop (FMSE 04)

Article type: Research Article

Authors: Bugliesi, Michele | Focardi, Riccardo | Maffei, Matteo

Affiliations: Dipartimento di Informatica, Università Ca' Foscari di Venezia, Via Torino 155, I-30172 Mestre (Ve), Italy. E-mail: [email protected], [email protected], [email protected]

Note: [*] Extended and revised version of [13].

Abstract: 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. Protocols 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.

DOI: 10.3233/JCS-2007-15602

Journal: Journal of Computer Security, vol. 15, no. 6, pp. 563-617, 2007