The ρ-spi Calculus at Work: Authentication Case Studies

In [10], we introduce a process calculus for describing security protocols and we propose a static and compo-sitional analysis of entity authentication. In this paper we apply such a technique on well-known shared key authentication protocols. The analysis helps clarifying the protocol logics, suggests simplifications and reveals some attacks. Moreover we discuss how our analysis scales up to multi-protocol systems