Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories - Department of Formal methods Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories

Résumé

We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems.
Fichier principal
Vignette du fichier
LIPIcs.FSCD.2023.30.pdf (749.84 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-04214220 , version 1 (05-04-2024)

Licence

Paternité

Identifiants

Citer

Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. pp.30:1--30:19, ⟨10.4230/LIPIcs.FSCD.2023.30⟩. ⟨hal-04214220⟩
37 Consultations
3 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More