Abstract
The design of authentication protocols has proven to be surprisingly error prone. We suggest that this is partly due to a language problem. The objectives of entity authentication are usually given in terms of human encounters while we actualy implement message passing prtotocols. We propose various translations of the high level objectives into a language appropriate for communication protocols. In addition, protocols are often specified at too low a level of abstraction. We will argue that encryption should not be used as a general primitive as it does not capture the specific purpose for using a cryptographic function in a particular protocol.
