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

Helmut Seidl, Kumar Neeraj Verma

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 satisfiabil…