Computer Science Qatar
School of Computer Science, Carnegie Mellon University
Also appears as Computer Science Department
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 .
*Carnegie Mellon University Qatar Campus