An Execution Environment for the MSR Cryptoprotocol Specification Language
Mark-Oliver Stehr,
Iliano Cervesato, and
Stefan Reich.
This work is supported by
the ONR MURI Project CONTESSA.
Keywords: MSR, Multiset Rewriting, Linear Logic, Rewriting Logic,
Dependent Types, Cryptoprotocol Specification
MSR is a specification language for cryptographic protocols that is
based on multiset-rewriting and evolved from ideas on combining linear
logic with the Logical Framework (LF). The goal of this project is to
develop an execution environment for specifications in the MSR
language. We plan to achieve this by defining a mapping from MSR into
rewriting logic with (dependent) types (RWLDT). The latter can be seen
as an instance of the open calculus of constructions (OCC), which
integrates key concepts from equational logic, rewriting logic and
type theory. Since RWLDT is a sublanguage of OCC, the mapping from
MSR into RWDT can then be composed with an existing mapping from a
sufficiently rich sublanguage of OCC into RWL, which has been already
implemented in the OCC/Maude prototype.
Relevant References:
- Iliano Cervesato,
Nancy Durgin,
Patrick D. Lincoln,
John C. Mitchell
and
Andre Scedrov:
A Meta-Notation for Protocol Analysis,
12th Computer Security Foundations Workshop -
CSFW-12,
pp. 55-69,
IEEE Computer Society Press,
Mordano, Italy,
28-30 June 1999.
Abstract,
Bibtex,
Full paper
(ps,
pdf,
dvi),
Research Index
- Iliano Cervesato:
Typed Multiset Rewriting Specifications of Security Protocols,
First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology -
MFCSIT'00
(A. Seda, editor),
pp. 1-43,
Elsevier
ENTCS 40,
Cork, Ireland,
19-21 July 2000.
Abstract,
Bibtex,
Full paper
(ps,
pdf,
dvi),
Electronic version,
Slides
- Iliano Cervesato:
A Specification Language for Crypto-Protocols based on Multiset Rewriting, Dependent Types and Subsorting,
Workshop on Specification, Analysis and Validation for Emerging Technologies -
SAVE'01
(G. Delzanno, S. Etalle and M. Gabbrielli, editors),
pp. 1-22,
Paphos, Cyprus,
1 December 2001.
Abstract,
Bibtex,
Full paper
(ps,
dvi),
Slides
- Iliano Cervesato:
Typed MSR: Syntax and Examples,
First International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security -
MMM'01
(V.I. Gorodetski, V.A. Skormin and L.J. Popyack, editors),
pp. 159-177,
Springer-Verlag
LNCS 2052,
St. Petersburg, Russia,
21-23 May 2001.
Abstract,
Bibtex,
Full paper
(ps,
dvi),
Slides
- Iliano Cervesato:
Data Access Specification and the Most Powerful Symbolic Attacker in MSR,
Software Security - Theories and Systems -
ISSS 2002,
(Revised Papers of the 2002 Mext-NSF-JSPS International Symposium)
(M. Okada, B. Pierce, Andre Scedrov,
H. Tokuda and A. Yonezawa, editors),
pp. 384-416,
Springer-Verlag
LNCS 2609,
Tokyo, Japan,
8-10 November 2003.
Abstract,
Bibtex,
Full paper
(ps,
pdf,
dvi)
-
Frederic Butler,
Iliano Cervesato,
Aaron D. Jaggard
and
Andre Scedrov:
A Formal Analysis of Some Properties of Kerberos 5 Using MSR,
Fifteenth Computer Security Foundations Workshop -
CSFW-15,
pp. 175-190,
IEEE Computer Society Press,
Cape Breton, NS, Canada,
24-26 June 2002.
Abstract,
Bibtex,
Full paper
(ps,
pdf,
dvi),
Slides
- Mark-Oliver Stehr: Programming, Specification, and Interactive
Theorem Proving - Towards a Unified Language based on Equational
Logic, Rewriting Logic, and Type Theory , Doctoral Thesis,
Fachbereich Informatik, Universität Hamburg, 2002. Published as
E-Dissertation
here by SUB Hamburg.
Abstract available in
html and
ps. Thesis available in ps
and pdf.
- M.-O. Stehr: The Open Calculus of Constructions: An Equational
Type Theory with Dependent Types for Programming, Specification, and
Interactive Theorem Proving, 2003. Draft available here.
- I. Cervesato, M.-O. Stehr: Representing the MSR Cryptoprotocol
Specification Language in an Extension of Rewriting Logic with
Dependent Types. Fifth International Workshop on Rewriting Logic and
its Applications (WRLA'2004), Barcelona, Spain, March 27 - 28, 2004,
Electronic Notes in Theoretical Computer Science, Elsevier,
2004. Paper available here.
- Iliano Cervesato. MSR 2.0: Language Definition and Programming Environment.
ITT Industries, August 26, 2004. Manuscript. Preliminary Version.
Presentations
- Relating the MSR Crypto-Protocol Specification Language to
Rewriting Logic with Dependent Types. UMBC Protocol Analysis
Meeting, June 10-11, 2003, Baltimore. Slides available here.
- Towards an Execution Environment for the MSR Cryptoprotocol
Specification Language (joint work with Iliano Cervesato, ITT
Industries). Contessa Review Meeting 2003, December 5, 2003,
University of Pennsylvania. Slides available here.
To explore the suitability of our translation we have conducted two case studies and analyzed
them in the MSR implementation:
Implementation
An MSR implementation is available for all platforms that the rewriting engine
Maude supports. The tool allows parsing,
executing and analyzing MSR specifications.
It is built on top of Maude 2.0, but requires a special version of
the Maude engine which we provide on this page (see links below). So in addition to
msr.tgz, you need to install a binary version of the Maude interpreter
(we have built versions for
Linux, Windows and MacOS X) or download the sources and compile Maude yourself.
Further installation instructions can be found in the
user's guide.
A documentation for developers interested in understanding and modifying the MSR
implementation is underway and will be released here shortly.
The MSR distribution contains the following files and directories: