Helmut Seidl, Vesal Vojdani and Varmo Vene. A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis. In Ana Cavalcanti and Dennis Dams, editors, Formal Methods, volume 5850 of Lecture Notes in Computer Science, Eindhoven, The Netherlands, November 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