FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Knowledge Problems in Equational Extensions of Subterm Convergent Theories

Authors: Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen

Paper Information

Title:Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Authors:Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen
Proceedings:UNIF Extended abstracts
Editors: Mauricio Ayala-Rincon and Philippe Balbiani
Keywords:intruder deduction problem, static equivalence problem, subterm convergent theories, equational rewriting
Abstract:

ABSTRACT. We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In this note we extend this to consider a subterm convergent equational term rewrite system defined modulo an equational theory, like Commutativity or Associativity-Commutativity. We show that for certain classes of such equational theories, namely the shallow classes, the two knowledge problems remain decidable.

Pages:7
Talk:Jul 07 11:00 (Session 26R: Unification, protocol analysis, and logics)
Paper: