On the complexity of equational Horn clauses

Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

96 Scopus citations

Abstract

Security protocols employing cryptographic primitives with algebraic properties are conveniently modeled using Horn clauses modulo equational theories. We consider clauses corresponding to the class H3 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.

Original languageEnglish
Title of host publicationAutomated Deduction - CADE-20 - 20th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages337-352
Number of pages16
ISBN (Print)3540280057, 9783540280057
DOIs
StatePublished - 2005
Event20th International Conference on Automated Deduction, CADE-20 - Tallinn, Estonia
Duration: 22 Jul 200527 Jul 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3632 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Automated Deduction, CADE-20
Country/TerritoryEstonia
CityTallinn
Period22/07/0527/07/05

Fingerprint

Dive into the research topics of 'On the complexity of equational Horn clauses'. Together they form a unique fingerprint.

Cite this