Tractable inference systems: an extension with a deducibility predicate

Hubert Comon-Lundh 1 Véronique Cortier 2 Guillaume Scerri 2
1 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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).
Type de document :
Communication dans un congrès
Bonacina, Maria Paola. CADE'24 - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, United States. Springer, 7898, pp.91-108, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_6〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00881068
Contributeur : Véronique Cortier <>
Soumis le : jeudi 7 novembre 2013 - 14:13:49
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri. Tractable inference systems: an extension with a deducibility predicate. Bonacina, Maria Paola. CADE'24 - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, United States. Springer, 7898, pp.91-108, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_6〉. 〈hal-00881068〉

Partager

Métriques

Consultations de la notice

430