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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 2004
Accession Number
ADA484963

Entities

People

  • Iliano Cervesato
  • Mark-oliver Stehr

Organizations

  • ITT Corporation

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Authentication
  • Calculus
  • Coding
  • Computer Science
  • Construction
  • Cryptography
  • Demographic Cohorts
  • Embedding
  • Environment
  • Language
  • Notation
  • Security Protocols
  • Specifications
  • Standards
  • Symbols
  • Translations

Readers

  • Computational Linguistics