MSR 2.0: Language Definition and Programming Environment
Abstract
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].
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 2011
- Accession Number
- ADA556716
Entities
People
- Iliano Cervesato
Organizations
- Carnegie Mellon University