Primitives for Authentication in Process Algebras

We extend the P­­-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 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 for the P­calculus, gives us almost for free both the partner authentication and the message authentication primitives.