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

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

2005-11-03

arxiv.org/abs/cs/0511014v1

Computer Science

Logic in Computer Science

Long version of paper presented at LPAR 2004

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-482688