Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
<|reference_start|>Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying: 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.<|reference_end|>
@article{seidl2005flat,
    title={Flat and One-Variable Clauses: Complexity of Verifying Cryptographic
  Protocols with Single Blind Copying},
    author={Helmut Seidl, Kumar Neeraj Verma},
    journal={arXiv preprint arXiv:cs/0511014},
    year={2005},
    archivePrefix={arXiv},
    eprint={cs/0511014},
    primaryClass={cs.LO cs.CR}
}