Sciweavers

TOCL
2008

Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying

14 years 10 days ago
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.
Helmut Seidl, Kumar Neeraj Verma
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TOCL
Authors Helmut Seidl, Kumar Neeraj Verma
Comments (0)