[an error occurred while processing this directive] The Security Protocol Specification Language MSR

The Security Protocol Specification Language MSR

[ Papers | Implementation | Examples | Related pages ]

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:


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:

It is being extended to additinally provide: This implementation has been used to specify a number of examples . It will be the basis for experimentation with reasoning and verification for MSR.


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.


Related Pages


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