@inproceedings{080e1118219b4acab655e3268c55bd4a,
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, 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.",
author = "Helmut Seidl and Verma, \{Kumar Neeraj\}",
year = "2005",
doi = "10.1007/978-3-540-32275-7\_6",
language = "English",
isbn = "3540252363",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "79--94",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 11th International Conference, LPAR 2004, Proceedings",
note = "11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004 ; Conference date: 14-03-2005 Through 18-03-2005",
}