Completeness of the Authentication Tests

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.