Helmut Seidl and Kumar Neeraj Verma. Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case. In Ralf Treinen, editor, Rewriting Techniques and Applications, volume 5595 of Lecture Notes in Computer Science, pages 118-132, Brasília, Brazil, June 2009. Springer.
In cryptographic protocols with the single blind copying restriction, at most one piece of unknown data is allowed to be copied in each step of the protocol. The secrecy problem for such protocols can be modeled as the satisfiability problem for the class of first-order Horn clauses called flat and one-variable Horn clauses, and is known to be DEXPTIME-complete. We show that when an XOR operator is additionally present, then the secrecy problem is decidable in 3-EXPTIME. We also note that replacing XOR by the theory of associativity-commutativity or by the theory of Abelian groups, or removing some of the syntactic restrictions on the clauses, leads to undecidability.
Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com