[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:
- 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.
Implementations
MSR 2
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
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.
MSR 3
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.
Examples
Related Pages
...
Last modified: Fri Dec 31, 10
[an error occurred while processing this directive]