The Sizes of Skeletons: Security Goals are Decidable
February 2005
Joshua D. Guttman, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
We show how to collapse executions of a cryptographic protocol, when they contain behaviors that we regard as redundant. Moreover, executions containing sufficiently many local runs necessarily contain redundant behaviors, if they have limited numbers of fresh values. Since precise authentication and secrecy assertions are explicit about which values must be assumed to be fresh, it follows that these assertions are decidable.
We formalize these notions within the strand space framework, introducing the notion of a skeleton, a collection of behaviors of the regular (non-penetrator) participants. Homomorphisms between skeletons express natural relations relevant to protocol analysis.
Additional Search Keywords
n/a
|
