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  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 pi-calculus, gives us almost for free both the partner authentication and the message authentication primitives.
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.