**MSR** (not to be confused with *MicroSoft Research*) comprises a
family of specification languages and environments for distributed and
concurrent systems. It originated as an extension of multiset rewriting
(hence the acronym) and has its foundations in linear logic and type theory.
It has been mostly applied to the investigation of cryptographic security
protocols, both to study their fundamental properties and to represent and
reason about actual protocols.

There have been 3 versions of MSR so far:

**MSR 1:**This is a simple first-order multiset rewriting language augmented with existential quantifiers on the right-hand side of rewrite rules. Typing is kept to a minimum and at most one network predicate could occur in a rule. It has been used mainly to obtain early decidability and complexity results for cryptographic protocol verification and as a bridge to compare some early protocol specification formalisms.**MSR 2:**This language has the objective of carrying out actual protocol verifications. It extends**MSR 1**with a powerful type system based on dependent types with subsorting, with guards and constraints, and with a module system. The major case study as a formalism to analyze real protocols was through a multi-year project focusing on the Kerberos V authentication protocol, which le to some interesting findings.**MSR 2**also played a role in furthering our theoretical understanding of security protocols: it underlies the first proof of completeness of the Dolev-Yao intruder, and was used in a study of user-defined notions of type-flaw vulnerabilities. An MSR 2 prototype comprising a type checker and an evaluator has been implemented and used to specify the protocols in the Clark-Jacob library.**MSR 3:**This more recent project reexamines the logical foundations of multiset rewriting and generalizes them into a formalism that combines the inherent state-transition semantics found in multiset rewriting for example, and the reactive nature of process algebra. It is the first language to support both computational paradigms, and it has a simple interpretation in linear logic. It has been implemented in a very early prototype.

Follow this link for an annotated bibliography of papers related to MSR.

An implementation of MSR 2 is now available here. It is written in Maude and was developed at the University of Illinois - Urbana-Champaign by Mark-Oliver Stehr and Stefan Reich as part of the MURI CONTESSA project. The implementation currently provides:

- Parsing
- Type reconstruction
- Type checking
- Forward simulation

- AS checker

A very early prototype of MSR 3 was developed by Lawrence Tan. It contains a type-checker and a preliminary evaluator. It will be made public once it is more robust.

- The Clark-Jacob Library in MSR 2.0
- Examples in mathematical notation from early papers:

Last modified: Fri Dec 31, 10 [an error occurred while processing this directive]