CADE 2013 - LNAI 7898

Tractable Inference Systems: An Extension with a Deducibility Predicate

Hubert Comon-Lundh¹, Véronique Cortier², and Guillaume Scerri^{1, 2}

¹LSV, CNRS & ENS Cachan, France

²LORIA, CNRS, France

Abstract. The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses. Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects. For instance, our clauses may contain atomic formulas S t where is a predicate symbol and S is a finite set of terms instead of a term. is used to represent any possible computation of an attacker, given a set of messages S. The class of clauses that we consider encompasses the clauses designed by Bana & Comon-Lundh for security proofs of protocols in a computational model.

Because of the (variadic) predicate symbol, we cannot use ordered resolution strategies only, as in Basin & Ganzinger: given S t, we must avoid computing S′ t for all subsets S′ of S. Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment.

Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin & Ganzinger), together with a particular class of (non saturated) Horn clauses with the predicate and constraints (which are necessary to cover the application).

LNAI 7898, p. 91 ff.

Full article in PDF | BibTeX