Tags:Deducibility, Graph-minors, Static equivalence and Term rewrite systems

Abstract:

In this preliminary paper we report on the development of a new form of term rewrite system, the graph-embedded term rewrite system. These systems are inspired by the graph minor relation and are more flexible extensions of the well known homeomorphic embedded term rewrite systems. As a motivating application area for the new systems, we consider the symbolic analysis of security protocols. In this field, restricted term rewrite systems, such as subterm-convergent, have proven useful since many of the decision procedures are sound and complete for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm-convergent". Interestingly, the applicability of the decision procedure to these examples must typically be proven on an individual basis since they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that most of these systems are examples of graph-embedded term rewrite systems.

Graph-Embedded Term Rewrite Systems and Applications (a Preliminary Report)