Knowledge Problems in Equational Extensions of Subterm Convergent Theories

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01878567
Contributor : Christophe Ringeissen <>
Submitted on : Friday, September 21, 2018 - 11:18:14 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Saturday, December 22, 2018 - 3:05:27 PM

File

subterm-know.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01878567, version 1

Collections

Citation

Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Knowledge Problems in Equational Extensions of Subterm Convergent Theories. UNIF 2018 - 32nd International Workshop on Unification, Mauricio Ayala-Rincon; Philippe Balbiani, Jul 2018, Oxford, United Kingdom. ⟨hal-01878567⟩

Share

Metrics

Record views

160

Files downloads

30