Primitives for Authentication in Process Algebras

We extend the pi-calculus and the spi-calculus with two primitives that guarantee authentication. They enable us to abstract from various implementations/specifications of authentication, and to obtain idealized protocols which are “secure by construction”. The main underlying idea, originally proposed in Focardi (Proc. Sixth Italian Conf. on Theoretical Computer Science, November 1998) for entity authentication, is to use the locations of processes in order to check who is sending a message (authentication of a party) and who originated a message (message authentication). The theory of local names, developed in Bodei et al. (Theoret. Comput. Sci. 253(2) (2001) 155) for the View the MathML source-calculus, gives us almost for free both the partner authentication and the message authentication primitives.