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

Helmut Seidl; Kumar Neeraj Verma

doi:10.1145/1380572.1380577

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

Helmut Seidl, Kumar Neeraj Verma

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

1 Scopus citations

Abstract

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class 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.

Original language	English
Article number	28
Journal	ACM Transactions on Computational Logic
Volume	9
Issue number	4
DOIs	https://doi.org/10.1145/1380572.1380577
State	Published - 1 Aug 2008

Keywords

Cryptographic protocols
First-order logic
Horn clauses
Instantiation-based theorem proving
Resolution

Access to Document

10.1145/1380572.1380577

Cite this

@article{8fed652884184bebaec66cb283806700,

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

abstract = "Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class 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.",

keywords = "Cryptographic protocols, First-order logic, Horn clauses, Instantiation-based theorem proving, Resolution",

author = "Helmut Seidl and Verma, {Kumar Neeraj}",

note = "Funding Information: This work has partly been supported by the Council of the European Community through the EJOB-program and partly by the Deutsche Forschungsgemeinschaft through the Sonderforschungs-bereich Frankfurt/Darmstadt.",

year = "2008",

month = aug,

day = "1",

doi = "10.1145/1380572.1380577",

language = "English",

volume = "9",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery (ACM)",

number = "4",

}

TY - JOUR

T1 - Flat and one-variable clauses

T2 - Complexity of verifying cryptographic protocols with single blind copying

AU - Seidl, Helmut

AU - Verma, Kumar Neeraj

N1 - Funding Information: This work has partly been supported by the Council of the European Community through the EJOB-program and partly by the Deutsche Forschungsgemeinschaft through the Sonderforschungs-bereich Frankfurt/Darmstadt.

PY - 2008/8/1

Y1 - 2008/8/1

N2 - Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class 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.

AB - Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class 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.

KW - Cryptographic protocols

KW - First-order logic

KW - Horn clauses

KW - Instantiation-based theorem proving

KW - Resolution

UR - http://www.scopus.com/inward/record.url?scp=51149113525&partnerID=8YFLogxK

U2 - 10.1145/1380572.1380577

DO - 10.1145/1380572.1380577

M3 - Article

AN - SCOPUS:51149113525

SN - 1529-3785

VL - 9

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 4

M1 - 28

ER -

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

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this