Typed MSR: Syntax and Examples

Abstract. Many design flaws and incorrect analyses of cryptographic protoAppeared in the Proceedings of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security — MMM’01 (V.I. Gorodetski, V.A. Skormin and L.J. Popyack, editors), pp. 159–176, c Springer-Verlag LNCS 2052, St. Petersburg, Russia, 21–23 May 2001 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 faithfu...

• Type: Conference
• Year: 2001
• Where: MMMACNS
• Authors: Iliano Cervesato
• Keywords: Computer Network Security, Information Management, Many Design flaws, MMMACNS 2001, Specification Language