Authentication Primitives for Refining Protocol Specifications *

Abstract We propose a way to abstract from various specifications of authentication and to obtain idealized protocols "secure by construction". This feature enables us to prove that a cryptographic protocol is the correct implementation of the corresponding abstract protocol. Our proposal relies on the combination of two authentication primitives, proposed by the authors in [20, 18] to a simplified version of the spi calculus