Download:
Abstract: In two prior papers, Millen-Lynch-Meadows proved that, under some restrictions on messages, including identities for canceling an encryption and a decryption within the same term during analysis will be redundant. i.e., they will not lead to any new attacks that were not found without them. In this paper, we prove that slightly modified restrictions are sufficient to safely remove those identities, even when protocols contain operators such as the Exclusive-OR operator that break the free algebra assumption with their own identities, in addition to the identities considered by Millen-Lynch-Meadows.
Keywords: Cryptographic protocol analysis, Free algebras,
Equational theories, Constraint solving, Exclusive-OR.
Acknowledgments: We are greatly indebted to Chris Lynch (Clarkson University) for many helpful comments and clarifications. This work was funded in part by IIIT, Hyderabad, India during Summer 2010.