|
Authentication Tests and
the Structure of Bundles 2002 Award Winner
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
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 be concluded 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.
»
Download Paper at the Science Direct Web site
Publication
Theoretical Computer Science, Vol. 283, Issue 2, pp. 333–380,
Copyright © 2002 Elsevier Scienc B.V. All rights reserved.
Additional Search Keywords
cryptographic protocols, authentication, secrecy, strand spaces, bundles, cryptographic protocol design
|
