Suppose a principal in a cryptographic protocol creates and transmits
a message containing a new value v, which it later receives back in
cryptographically altered form. It can conclude that some principal
possessing the relevant key has transformed the message containing v.
Insome circumstances, this 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 certain
values remain secret. Together, they determine what authentication properties
are achieved by a wide range of cryptographic protocols.
In this paper we introduce authentication tests and illustrate their
power, 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 [21], and prove
them correct elsewhere [8].
» Download Paper [PDF,
249KB]
