Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types |
| |
Authors: | Iliano Cervesato Mark-Oliver Stehr |
| |
Affiliation: | (1) Carnegie Mellon University, Qatar Campus, P.O. Box 42866, Doha, Qatar;(2) Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025, USA |
| |
Abstract: | This paper presents a shallow and efficient embedding of the security protocol specification language MSR into an extension
of rewriting logic with dependent types. The latter is 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.
The encoding presented in this paper has served as the basis for the implementation of an MSR specification and analysis environment
using the first-order rewriting engine Maude. |
| |
Keywords: | Security protocol Multiset rewriting Specification Dependent types |
本文献已被 SpringerLink 等数据库收录! |
|