The Security Protocol Specification Language MSR
[ Papers
| Examples
| Implementation
| Related pages
]
MSR (not to be confused with MicroSoft Research) is ...
There have been 3 versions of MSR so far:
- MSR 1: This was a simple first-order multiset rewriting language
augmented with existential quantifiers on the right-hand side of
rewrite rules. Typing was 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.
- MSR 2: Turns
- MSR 3:
Examples
Currently, all examples can be found only in the papers in mathematical
notation:
They will soon be available in the concrete syntax.
Implementation
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 will be the basis for experimentation with reasoning and
verification for MSR.
Related Pages
...
Last Modified: 30 August 2004