Compositional Analysis of Authentication Protocols

ESOP 2004, LNCS 2986, pages 140–154, 2004. c Springer–Verlag, Berlin Heildelberg 2003. We propose a new method for the static analysis of entity authentication protocols. We develop our approach based on a dialect of the spi-calculus as the underlying formalism for expressing protocol narrations. Our analysis validates the honest protocol participants against static (hence decidable) conditions that provide formal guarantees of entity 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 entity authentication in the presence of Dolev-Yao intruders.

• Type: Conference
• Year: 2004
• Where: ESOP
• Authors: Michele Bugliesi, Riccardo Focardi, Matteo Maffei
• Keywords: Entity Authentication, Entity Authentication Protocols, ESOP 2004, Programming Languages, Protocol Participants