Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying

TL;DR

This paper improves the complexity classification of the satisfiability problem for a class of clauses modeling cryptographic protocols with blind copying, showing it is NEXPTIME-complete and DEXPTIME-complete for Horn clauses.

Contribution

It establishes tighter complexity bounds for satisfiability and secrecy problems in cryptographic protocol modeling using first order clauses.

Findings

Satisfiability for class $ ext{C}$ is NEXPTIME-complete.

Satisfiability for Horn clauses in this class is DEXPTIME-complete.

Secrecy problem is DEXPTIME-complete.

Abstract

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class $\mathcal C$ 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.