Helmut Seidl and Kumar Neeraj Verma. Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. , volume abs/cs/0511014 of Forschungsbericht, 2005. Universität Trier, Mathematik/Informatik.

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class of first order clauses. 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