Authenticity by Tagging and Typing.

Matteo Maffei

MyThS/MIKADO/DART Meeting, Venice, June 14-16 2004


Slides

Abstract

Authentication is one of the most interesting security properties, so required by the real-life applications as difficult to analyze. Informally, authentication protocols enable one entity to prove its presence and claimed identity to a remote party, possibly authenticating a message. Messages used in authentication protocols are often ambigous: they can have different interpretations according to the context. This ambiguity often causes attacks in an isolated environment, where many principals run the same protocol. But the situation is even worse in a multi-protocol system, where principals run different protocols. As discussed by Syverson and Meadows, ``problems can arise when a protocol is interacting with another protocol that does not use a tagging scheme, or tags data in a different way''. We propose a uniform tagging scheme for authentication protocols, allowing to disambiguate the meaning of each ciphertext exchanged in the authentication task. Based on that, we propose a type and effect system for authentication protocols, based on the p-spi calculus. Our analysis validates the honest protocol participants against static (hence decidable) conditions that provide formal guarantees of authentication. The main result is that the validation of each component is provably sound and fully compositional: if all the protocol participants are successfully validated, then the protocol as a whole guarantees authentication in the presence of Dolev-Yao intruders. The compositional nature of the analysis makes it suitable for analyzing multi-protocol systems, where different protocols are concurrently executed.