Normalization of Linear Horn Clauses - Formal Methods: Foundations and Applications - page 243

selection . Later, Goubault-Larrecq and Parrennes [8] applied H 1 Horn clauses for ana-

lyzing implementations of cryptographic protocols in C.
In order to extend the class

H 1 , Nielsen et al. [11] introduced the Iterative Special-
ization Schema . The idea is to approximate a finite set of arbitrary Horn clauses by
means of H 1 Horn clauses to detect components of predicates which are finite .This

information then is exploited to obtain an equivalent, but hopefully syntactically sim-
pler set of Horn clauses via instantiation . Using these techniques, Nielsen et al. [11]
successfully validated the non-trivial Yahalom protocol for key-distribution.
In the present paper, we extend H 1 into another direction. We consider arbitrary

linear Horn clauses and present a normalization semi-procedure for computing least
models of finite sets of linear Horn clauses. Our normalization semi-procedure is a
simplification of the procedure of Nielson et al. [12], since no pre-computations are
necessary. It destructs complex heads on the fly. Moreover, it is a direct and strict ex-
tension: It always terminates on finite sets of H 1 Horn clauses in at most exponentially

many steps. Although satisfiability for finite sets of linear Horn clauses is undecid-
able [6], our semi-procedure at least terminates for certain meaningful subclasses of
the class of all finite sets of linear Horn clauses. One meaningful example, where the
semi-procedure terminates after at most exponentially many steps, are the finite sets of
linear Horn clauses that can be used for encoding a backward reachability analysis for
constrained dynamic pushdown networks (see Bouajjani et al. [3]). This application in
particular demonstrates that potential applications are not restricted to the analysis of
cryptographic protocols.

Outline. The present paper is organized as follows: We present our technical contri-
bution — the normalization semi-procedure for finite sets of linear Horn clauses — in
section 2. In section 3, we introduce an application which is not related to the analy-
sis of cryptographic protocols, namely, backward reachability for constrained dynamic
pushdown networks. We conclude in section 4. Omitted proofs can be found in the
corresponding technical report.

2 Normalization of Finite Sets of Linear Horn Clauses

2.1 Basics

For a set Σ of ranked function symbols and a set of variables, T ( Σ,X ) denotes the

set of terms built up from symbols in Σ and variables in

X

X . We assume that there are

k -ary function symbols k for all k ∅ ) is also denoted by

T ( Σ ) and contains all ground terms, i.e. all terms without variables. We denote function
symbols in the following by f , g and h , nullary function symbols (also called constants )
by a , b and c , variables by x , y and z , and finally terms by s , t and u . Positions in terms
are defined as usual as sequences of strictly positive integers. For a term t , t

∈ N \{ 1 } in Σ .Theset T ( Σ,

| l is the
subterm of t at position l ,and t [ s ] l the result of replacing that subterm by s .Given
aset

P of unary predicate symbols we are able to build atoms . For a unary predicate

P X ), P ( t ) is called an atom . In order to simplify nota-

tions, we also denote the atom P ( k ( t 1 ,...,t k )) by P ( t 1 ,...,t k ) for all k

∈ P and a term t ∈ T ( Σ,

.
We identify the pair ( P, k ) with the k -ary predicate P . Substitutions are functions

∈ N \{ 1 }