Affordable Access

Publisher Website

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

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
117
Identifiers
DOI: 10.1016/j.entcs.2004.06.023
Keywords
  • Msr
  • Protocol Specification
  • Open Calculus Of Constructions
  • Dependent Types
  • Maude

Abstract

Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.