Suppose a principal in a cryptographic protocol creates and transmits a message containing a new value v, later receiving v back in a different cryptographic context. It can conclude that some principal possessing the relevant key has received and transformed the message in which v was emitted. In some circumstances, this principal must be a regular participant of the protocol, not the penetrator.
An inference of this kind is an authentication test. We introduce two main kinds of
authentication test. An outgoing test is one in which the new value v is transmitted
in encrypted form, and only a regular participant can extract it from that form.
An incoming test is one in which v is received back in encrypted form, and only
a regular participant can put it in that form. We combine these two tests with a
supplementary idea, the unsolicited test, and a related method for checking that keys
remain secret. Together, these techniques determine what authentication properties
are achieved by a wide range of cryptographic protocols.
In this paper we introduce authentication tests and prove their soundness. We illustrate their power by giving new and straightforward proofs of security goals for several protocols. We also illustrate how to use the authentication tests as a heuristic for finding attacks against incorrect protocols. Finally, we suggest a protocol design
process.
We express these ideas in the strand space formalism, which provides a convenient context to prove them correct.
Published in Theoretical Computer Science, 2001.
cryptographic protocols, authentication, secrecy, strand spaces, bundles, cryptographic protocol design
