Computing Knowledge in Equational Extensions of Subterm Convergent Theories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2020

Computing Knowledge in Equational Extensions of Subterm Convergent Theories

Résumé

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 work we extend this to consider a subterm convergent term rewrite system defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.
Fichier principal
Vignette du fichier
permut-subterm-know.pdf (468.65 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02966957 , version 1 (14-10-2020)

Identifiants

Citer

Serdar Erbatur, Andrew M Marshall, Christophe Ringeissen. Computing Knowledge in Equational Extensions of Subterm Convergent Theories. Mathematical Structures in Computer Science, 2020, 30 (6), pp.683-709. ⟨10.1017/S0960129520000031⟩. ⟨hal-02966957⟩
49 Consultations
105 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More