Bounded ACh Unification

Authors: Ajay Kumar Eeralla and Christopher Lynch

Paper Information

Title:Bounded ACh Unification
Authors:Ajay Kumar Eeralla and Christopher Lynch
Proceedings:UNIF Extended abstracts
Editors: Mauricio Ayala-Rincon and Philippe Balbiani
Keywords:Homomorphism, Unification, Bounded, Splitting

ABSTRACT. We consider the problem of unification modulo an equational theory ACh, which consists of a function h which is homomorphic over an associative-commutative operator +. Unification modulo ACh is undecidable, so we define a bounded ACh unification problem. In this bounded version of ACh unification we essentially bound the number of times h can be recursively applied to a term, and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving bounded ACh unification, and we prove that the rules are sound, complete and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

Talk:Jul 07 11:30 (Session 26R: Unification, protocol analysis, and logics)