A Specification Language for Crypto-Protocols based on Multiset Rewriting, Dependent Types and Subsorting

MSR is an unambiguous, flexible, powerful and relatively simple specification framework for crypto-protocols. It uses multiset rewriting rules over first-order atomic formulas to express protocol actions and relies on a form of existential quantification to symbolically model the generation of nonces and other fresh data. It supports an array of useful static checks that include type-checking and data access verification. In this paper, we give a detailed presentation of the typing infrastructure of MSR, which is based on the theory of dependent types with subsorting. We prove that type-checking protocol specifications is decidable and show that execution preserves well-typing. We illustrate these features by formalizing a well-known protocol in MSR