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

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

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.
Long version of paper presented at LPAR 2004

Keywords

Logic in Computer Science, Cryptography and Security

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/104386

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0511014
 http://arxiv.org/abs/cs/0511014

Collections

arXiv