MSR 2.0: Language Definition and Programming Environment
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Programming and Software