Search

Nielson et al. [12] exhibit a rich class of Horn clauses which they call H1. Least models of finite sets of H1 Horn clauses are regular tree languages. Nielson et al. [12] describe a normalization procedure for computing least models of finite sets of H1 Horn clauses in the form of tree automata. In the present paper, we simplify and extend this normalization procedure to a semi-procedure that deals with finite sets of linear Horn clauses. The extended semi-procedure does not terminate in general but does so on useful subclasses of finite sets of linear Horn clauses. The extension in particular coincides with the normalization procedure of Nielson et al. [12] for sets of H1 Horn clauses. In order to demonstrate the usefulness of the extension, we show how backward reachability analysis for constrained dynamic pushdown networks (see Bouajjani et al. [3]) can be encoded into a class of finite sets of linear Horn clauses for which our normalization procedure terminates after at most exponentially many steps.

In cryptographic protocols with the single blind copying restriction, at most one piece of unknown data is allowed to be copied in each step of the protocol. The secrecy problem for such protocols can be modeled as the satisfiability problem for the class of first-order Horn clauses called flat and one-variable Horn clauses, and is known to be DEXPTIME-complete. We show that when an XOR operator is additionally present, then the secrecy problem is decidable in 3-EXPTIME. We also note that replacing XOR by the theory of associativity-commutativity or by the theory of Abelian groups, or removing some of the syntactic restrictions on the clauses, leads to undecidability.

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class \(\mathcal 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.

Security protocols employing cryptographic primitives with algebraic properties are conveniently modeled using Horn clauses modulo equational theories. We consider clauses corresponding to the class $\mathcal{H}3$ of Nielson, Nielson and Seidl. We show that modulo the theory ACU of an associative-commutative symbol with unit, as well as its variants like the theory XOR and the theory AG of Abelian groups, unsatisfiability is NP-complete. Also membership and intersection-non-emptiness problems for the closely related class of one-way as well as two-way tree automata modulo these equational theories are NP-complete. A key technical tool is a linear time construction of an existential Presburger formula corresponding to the Parikh image of a context-free language. Our algorithms require deterministic polynomial time using an oracle for existential Presburger formulas, suggesting efficient implementations are possible.

We study two-way tree automata modulo equational theories. We deal with the theories of Abelian groups (ACUM), idempotent commutative monoids (ACUI), and the theory of exclusive-or (ACUX), as well as some variants including the theory of commutative monoids (ACU). We show that the one-way automata for all these theories are closed under union and intersection, and emptiness is decidable. For two-way automata the situation is more complex. In all these theories except ACUI, we show that two-way automata can be effectively reduced to one-way automata, provided some care is taken in the definition of the so-called push clauses. (The ACUI case is open.) In particular, the two-way automata modulo these theories are closed under union and intersection, and emptiness is decidable. We also note that alternating variants have undecidable emptiness problem for most theories, contrarily to the non-equational case where alternation is essentially harmless.