Accession Number : ADA556716


Title :   MSR 2.0: Language Definition and Programming Environment


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : Cervesato, Iliano


Full Text : http://www.dtic.mil/get-tr-doc/pdf?AD=ADA556716


Report Date : Nov 2011


Pagination or Media Count : 34


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].


Descriptors :   *PROGRAMMING LANGUAGES , ABSTRACTS , CRYPTOGRAPHY , SEMANTICS , SPECIFICATIONS , SYNTAX , WRITING


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE