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.

Download Full Presentation