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 C 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.

• Type: Journal
• Year: 2008
• Where: TOCL
• Authors: Helmut Seidl, Kumar Neeraj Verma
• Keywords: Cryptographic Protocols, Satisfiability, Single Blind, TOCL 2008