The "authentication tests" are specific challenge-response patterns that occur frequently in cryptographic protocols. Each pattern furnishes a theorem that can be reused across many protocols to establish authentication results. Interestingly, when the authentication tests establish less authentication than one would like, these weaker results frequently suggest an attack.
This is joint work with Javier Thayer and Jonathan Herzog
We use the authentication tests to define a search strategy to enumerate all the minimal scenarios possible for a given protocol. We call such a minimal scenario a "shape". The search strategy is suggested by a notion of homomorphism between skeletons, where a skeleton is part of a potential protocol execution. These homomorphisms give an attractive way to reason about shapes, and to provide a comprehensive way to find them. This is a new aspect of our work on cryptographic protocols, and the approach suggests numerous open questions.
This is joint work with Javier Thayer and Shaddin Doghmi