Authenticity by Tagging and Typing.
Matteo Maffei
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.