We show how to collapse executions of a cryptographic protocol, when they contain behaviors that we regard as redundant.
The Sizes of Skeletons: Security Goals are Decidable
Download Resources
PDF Accessibility
One or more of the PDF files on this page fall under E202.2 Legacy Exceptions and may not be completely accessible. You may request an accessible version of a PDF using the form on the Contact Us page.
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.