Searching for Shapes in Cryptographic
Protocols
March 2007
Shaddin F. Doghmi, The MITRE Corporation
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
A shape describes the behavior of the honest participants in
some minimal protocol execution. These shapes are informative, because
typically protocols have very few of them. Authentication and secrecy
properties are easy to determine from the set of shapes, as are attacks,
and other protocol characteristics.
A skeleton gives partial information about some possible executions,
and a homomorphism from one skeleton to another is an informationpreserving
map. We describe a procedure that searches through skeletons
using homomorphisms. The search procedure has been implemented in
a Cryptographic Protocol Shape Analyzer (CPSA).
Additional Search Keywords
N/A
|
