Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types

This paper presents a shallow and hence efficient embedding of the security protocol specification language MSR into rewriting logic with dependent types, an instance of the open calculus of constructions which integrates key concepts from equational logic, rewriting logic, and type theory. MSR is b...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2005-01, Vol.117, p.183-207
Main Authors: Cervesato, Iliano, Stehr, Mark-Oliver
Format: Article
Language:English
Subjects:
dependent types
Maude
MSR
open calculus of constructions
protocol specification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a shallow and hence efficient embedding of the security protocol specification language MSR into rewriting logic with dependent types, an instance of the open calculus of constructions which integrates key concepts from equational logic, rewriting logic, and type theory. MSR is based on a form of first-order multiset rewriting extended with existential name generation and a flexible type infrastructure centered on dependent types with subsorting. This encoding is intended to serve as the basis for implementing an MSR specification and analysis environment using existing first-order rewriting engines such as Maude.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2004.06.023