Completeness of the Authentication Tests
March 2007
Shaddin F. Doghmi, The MITRE Corporation
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
The shapes of a cryptographic protocol are its minimal, essentially
different executions. In previous work, we have described a search algorithm
to discover the shapes of a protocol, and implemented the algorithm in a
Cryptographic Protocol Shape Analyzer cpsa.
In this paper, we show its completeness, i.e. that every shape can in fact
be found in a finite number of steps. The steps in question are applications
of two authentication tests, fundamental protocol patterns for analysis and
heuristics for protocol design. We formulate the authentication tests in a new,
stronger form, for which completeness is true.
We also introduce skeletons, as partial descriptions of executions. The
information-preserving maps between skeletons are a kind of homomorphism.
The completeness result shows that any homomorphism from a skeleton to a
full execution may be digested into a sequence of atomic steps leading to a
shape.
Additional Search Keywords
N/A
|
