Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9656021 | Electronic Notes in Theoretical Computer Science | 2005 | 25 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Iliano Cervesato, Mark-Oliver Stehr,