Helmut Seidl and Kumar Neeraj Verma. Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 79-94, Montevideo, Uruguay, March 2004. Springer.

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class of first order clauses, which extends the Skolem class. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com