file.pdf (151.54 kB)

Typed MSR: Syntax and Examples

Download (151.54 kB)
journal contribution
posted on 01.07.2010 by Iliano Cervesato
Many design flaws and incorrect analyses of cryptographic proto- cols can be traced to inadequate specification languages for message components, environment assumptions, and goals. In this paper, we present MSR, a strongly typed specification language for security protocols, which is intended to address the first two issues. Its typing infrastructure, based on the theory of dependent types with subsorting, yields elegant and precise formalizations, and supports a useful array of static check that include type-checking and access control validation. It uses multiset rewriting rules to express the actions of the protocol. The availability of memory predicates enable it to faithfully encode systems consisting of a collection of coordinated subprotocols, and constraints allow tackling objects belonging to complex interpretation domains, e.g. time stamps, in an abstract and modular way. We apply MSR to the specification of several examples.


Publisher Statement

© ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published at