MSR 2.0: Language Definition and Programming Environment

摘要

This report defines the syntax and semantics of the specification language MSR 2.0, and gives requirements for a run-time environment for it. Specifically, it defines the concrete syntax of the language and formalizes its typing and execution semantics at an abstract level. It also describes programming environment functionalities such as type reconstruction and facilities for controlling execution. MSR 2.0 is a specification language based on first-order multiset rewriting modulo equations, dependent types, and subsorting. This report is meant to act as its 'official' definition, as various subsets have appeared in previous publications, for example (6, 7). It has been used extensively for studying cryptographic protocols (5, 8, 9, 10, 12, 13, 15) and especially Kerberos (5, 1, 2, 3, 4, 16, 17). It was also used experimentally for modeling bio-molecular systems (11). MSR 1.0, the precursor of this version, was also used in foundational studies for cryptoprotocols (14, 19). An implementation of MSR 2.0 which adheres to the definition presented in this report has been written in Maude (18, 21).