Typed MSR: Syntax and Examples

  • Iliano Cervesato
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2052)


Many design flaws and incorrect analyses of cryptographic protocols 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.


Authentication Protocol Security Protocol Generic Role Dependent Type Access Control Policy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M. and Gordon, A.: A calculus for cryptographic protocols: the spi calculus. Information and Computation, 148,1, (1999) 1–70zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Abadi, M. and Needham, R.: Prudent Engineering Practice for Cryptographic Protocols. Research Report 125, Digital Equipment Corp., System Research Center, (1994)Google Scholar
  3. 3.
    Aspinall, D. and Compagnoni, A.: Subtyping Dependent Types. In E.N. Clarke, editor, Proc. LICS’96. New Brunswick, NJ. IEEE Computer Society Press (1996) 86–97Google Scholar
  4. 4.
    Balenson, D., McGrew, D. and Sherman, A.: Key Management for Large Dynamic Groups: One-Way Function Trees and Amortized Initialization. Internet Draft (work in progres), draft-irtf-smug-groupkeymgmt-oft-00.txt, Internet Engineering Task Force (August 25, 2000)Google Scholar
  5. 5.
    Burrows, M., Abadi, M. and Needham, R.: A Logic of Authentication. Proceedings of the Royal Society, Series A, 426,1871 (1989) 233–271zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Cervesato, I.: MSR, Access Control, and the Most Powerful Attacker. Submitted to LICS’01, Boston, MA, 2001.
  7. 7.
    Cervesato, I.: A Specification Language for Crypto-Protocol based on Multiset Rewriting, Dependent Types and Subsorting.Google Scholar
  8. 8.
    Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. Submitted to Proc. MFCSIT’00, ENTCS.
  9. 9.
    Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J. and Scedrov, A.: A Meta-Notation for Protocol Analysis. In Proc. CSFW’99. Mordano, Italy, IEEE/CS Press, (1999) 55–69Google Scholar
  10. 10.
    Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J. and Scedrov, A.: Relating Strands and Multiset Rewriting for Security Protocol Analysis. In Proc. CSFW’00, (2000) 35–51Google Scholar
  11. 11.
    Cervesato, I., Durgin, N.A., Kanovich, M. and Scedrov, A.: Interpreting Strands in Linear Logic. In Proc. FMCS’00. Chigaco, IL, (2000)Google Scholar
  12. 12.
    Clark, J. and Jacob, J.: A Survey of Authentication Protocol Literature. Department of Computer Science, University of York. (1997) Web Draft Version 1.0 available from
  13. 13.
    Denker, G. and Millen, J.K.: CAPSL Intermediate Language. In N. Heintze and E. Clarke (eds.): Proc. FMSP’99. Trento, Italy (1999)Google Scholar
  14. 14.
    Dolev, D. and Yao, A.C.: On the security of public-key protocols. IEEE Transactions on Information Theory. (1983) 2(29): 198–208CrossRefMathSciNetGoogle Scholar
  15. 15.
    Durgin, N., Lincoln, P., Mitchell, J. and Scedrov, A.: Undecidability of bounded security protocols. In Heintze, N. and Clarke, E. (eds.): Proc. FMSP’99. Trento, Italy (1999)Google Scholar
  16. 16.
    Fàabrega, F.J.T., Herzog, J.C. and Guttman, J.D.: Strand Spaces: Why is a Security Protocol Correct?. In Proc. SSP’98. (1998) 160–171 Oakland, CA, IEEE/CS PressGoogle Scholar
  17. 17.
    Kanovich, M.I., Okada, M. and Scedrov, A.: Specifying real-time finite-state systems in linear logic. In Proc. COTIC’98. Nice, France (1998) ENTCS 16(1)Google Scholar
  18. 18.
    Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Programming, (1996) 26(2): 113–131zbMATHCrossRefGoogle Scholar
  19. 19.
    Needham, R.M. and Schroeder, M.D.: Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM. (1978) 21(12): 993–999zbMATHCrossRefGoogle Scholar
  20. 20.
    Neuman, B.C. and Stubblebine, S.G.: A Note on the Use of Timestamps as Nonces. Operating Systems Review, (1993) 27(2) 10–14CrossRefGoogle Scholar
  21. 21.
    Pfenning, F.: Refinement Types for Logical Frameworks. In Geuvers, H. (ed.): Proc. TYPES’93. Nijmegen, The Netherlands (1993) 285–299Google Scholar
  22. 22.
    Syverson, P.F.: A Different Look at Secure Distributed Computation. In Proc. CSFW-10, (1997) 109–115 IEEE Computer Society PressGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Iliano Cervesato
    • 1
  1. 1.Advanced Engineering and Sciences DivisionITT Industries, Inc.AlexandriaUSA

Personalised recommendations