Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types

DOI10.1007/s10990-007-9003-3zbMath1115.68073OpenAlexW3192975255MaRDI QIDQ880987

Iliano Cervesato, Mark-Oliver Stehr

Publication date: 21 May 2007

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-007-9003-3

zbMATH Keywords

SpecificationDependent typesMultiset rewritingSecurity protocol

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (4)

The rewriting logic semantics project ⋮ Twenty years of rewriting logic ⋮ An algebraic semantics for MOF ⋮ Memory Representations in Rewriting Logic Semantics Definitions

Uses Software

• ASSET
• SPIN
• Maude
• ProVerif
• Automath
• NRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Conditional rewriting logic as a unified model of concurrency
• The chemical abstract machine
• A calculus for cryptographic protocols: The spi calculus
• Maude: specification and programming in rewriting logic
• Specification and proof in membership equational logic
• The NRL Protocol Analyzer: An Overview
• Analyzing security protocols with secrecy types and logic programs
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Types for Proofs and Programs

This page was built for publication: Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types