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

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.

Abstract licence: CC0

A person counts once a day per paper. We keep no cookie and no address: a reader is a hash that changes every day. Any month under five reads shows no number.