  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.
