Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
| dc.creator | Seidl, Helmut | |
| dc.creator | Verma, Kumar Neeraj | |
| dc.date | 2005-11-03 | |
| dc.date.accessioned | 2026-07-07T06:49:33Z | |
| dc.date.available | 2026-07-07T06:49:33Z | |
| dc.description | 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. | |
| dc.description | Long version of paper presented at LPAR 2004 | |
| dc.identifier | https://arxiv.org/abs/cs/0511014 | |
| dc.identifier | http://arxiv.org/abs/cs/0511014 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/104386 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Cryptography and Security | |
| dc.title | Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying | |
| dc.type | text |