The framework called MSR is based on multiset rewriting
systems defined over first-order atomic formulas and it has been
introduced by Cervesato et al. [11] for the formal
specification of cryptographic protocols. In [14],
the basic formalism (i.e., without existential quantification) has
been extended to allow for the specification of relations over
data variable using constraints, i.e. a logic language
interpreted over a fixed domain. Multiset rewriting rules allow
one to locally model rendez-vous and internal
actions of processes, and constraints to symbolically represent
the relation between the data of different processes, thus
achieving a clear separation between process structure and data
paths. This formalism can be viewed as a first-order extension of
Petri Nets in which tokens carry along structured data. We will
call the resulting formalism
. First of all, we introduce
the notion of constraint system.
Subsections