In [Mil03, LM05], 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 notorious Exclusive-OR operator that break the free algebra assumption with their own identities, in addition to the identities considered by Millen-Lynch-Meadows.
CITATION STYLE
Malladi, S. (2015). Soundness of removing cancellation identities in protocol analysis under exclusive-or. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6993, pp. 205–224). Springer Verlag. https://doi.org/10.1007/978-3-642-27375-9_12
Mendeley helps you to discover research relevant for your work.