r-spi calculus at work:Authentication Case Studies Riccardo Focardi a,1,2 Matteo Maffei a,1,3

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