{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:49:31Z","timestamp":1783684171414,"version":"3.55.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T00:00:00Z","timestamp":1172275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,4,4]]},"DOI":"10.1007\/s10990-007-9003-3","type":"journal-article","created":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T03:09:26Z","timestamp":1172286566000},"page":"3-35","source":"Crossref","is-referenced-by-count":1,"title":["Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types"],"prefix":"10.1007","volume":"20","author":[{"given":"Iliano","family":"Cervesato","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark-Oliver","family":"Stehr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,2,24]]},"reference":[{"key":"9003_CR1","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/1044731.1044735","volume":"521","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52(1), 102\u2013146 (2005)","journal-title":"J. ACM"},{"key":"9003_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"1481","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Inf. Comput. 148(1), 1\u201370 (1999)","journal-title":"Inf. Comput."},{"key":"9003_CR3","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P.: Lambda-calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Background: Computational Structures, vol. 2 Handbook of Logic in Computer Science. Claredon Press, Oxford (1992)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"9003_CR4","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"961","author":"G. Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comp. Sci. 96(1), 217\u2013248 (1992)","journal-title":"Theor. Comp. Sci."},{"key":"9003_CR5","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"9003_CR6","unstructured":"Blanchet, B.: ProVerif Automatic Cryptographic Protocol Verifier user Manual. CNRS, D\u00e9partement dInformatique, \u00c9cole Normale Sup\u00e9rieure, Paris (2005)"},{"key":"9003_CR7","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comp. Sci. 236, 35\u2013132 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"9003_CR8","doi-asserted-by":"crossref","unstructured":"Brackin, S., Meadows, C., Millen, J.: CAPSL interface for the NRL protocol analyzer. In: 2nd IEEE Workshop on Application-Specific Software Engineering and Technology (ASSET \u201999). IEEE Computer Society (1999)","DOI":"10.1109\/ASSET.1999.756753"},{"key":"9003_CR9","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using MSR. In: Fifteenth Computer Security Foundations Workshop, pp. 175\u2013190. IEEE Computer Society Press (2002)"},{"key":"9003_CR10","unstructured":"Cervesato, I.: A specification language for crypto-protocols based on multiset rewriting, dependent types and subsorting. In: Workshop on Specification, Analysis and Validation for Emerging Technologies, pp. 1\u201322 (2001)"},{"key":"9003_CR11","doi-asserted-by":"crossref","unstructured":"Cervesato, I.: Typed MSR: Syntax and examples. In: 1st International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, pp. 159\u2013177. Springer-Verlag LNCS 2052 (2001)","DOI":"10.1007\/3-540-45116-1_18"},{"key":"9003_CR12","doi-asserted-by":"crossref","unstructured":"Cervesato, I.: Data access specification and the most powerful symbolic attacker in MSR. In: Software Security, Theories and Systems, volume 2609 of Lecture Notes in Computer Science, pp. 384\u2013416. Springer-Verlag (2003)","DOI":"10.1007\/3-540-36532-X_23"},{"key":"9003_CR13","unstructured":"Cervesato, I.: MSR: Language definition and programming environment Nov. (2003). Draft available from http:\/\/theory.stanford.edu\/ iliano\/MSR\/"},{"key":"9003_CR14","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society (2000)","DOI":"10.1109\/CSFW.2000.856924"},{"key":"9003_CR15","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Durgin, N., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: 12th Computer Security Foundations Workshop, pp. 55\u201369. IEEE Computer Society Press (1999)","DOI":"10.1109\/CSFW.1999.779762"},{"key":"9003_CR16","unstructured":"Cervesato, I.: The logical meeting point of multiset rewriting and process algebra: Progress report. Technical Memo CHACS-5540-153, Center for High Assurance Computer Systems, Naval Research Laboratory, Washington, DC (Sep. 2004)"},{"key":"9003_CR17","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"2852","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theor. Comp. Sci. 285(2), 187\u2013243 (2002)","journal-title":"Theor. Comp. Sci."},{"key":"9003_CR18","unstructured":"Denker, G.: Design of a CIL connector to Maude. In: Veith, H., Heintze, N., Clarke, E. (eds.) Workshop on Formal Methods and Computer Security (2000)"},{"key":"9003_CR19","unstructured":"Denker, G., Millen, J.K.: CAPSL intermediate language. In: Heintze, N., Clarke, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols\u2014FMSP, Trento, Italy (1999)"},{"key":"9003_CR20","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer J.: A rewriting-based inference system for the NRL Protocol Analyzer: Grammar generation. In: K\u00fcsters, R., Mitchell, J. (eds.) Proceedings of the 2005 ACM Workshop on Formal Methods in Security Engineering\u2014FMSE 2005. Alexandria, VA, ACM. To appear (Nov. 2005)","DOI":"10.1145\/1103576.1103578"},{"key":"9003_CR21","unstructured":"Holzmann, G.J.: The Spin Model Checker\u2014Primer and Reference Manual. Addison-Wesley (2003)"},{"key":"9003_CR22","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Proceedings of TACAS, vol. 1055 of Lecture Notes in Computer Science, pp. 147\u2013166. Springer-Verlag (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"9003_CR23","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"262","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Progr. 26(2), 113\u2013131 (1996)","journal-title":"J. Logic Progr."},{"key":"9003_CR24","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comp. Sci. 96, 73\u2013155 (1992)","journal-title":"Theor. Comp. Sci."},{"key":"9003_CR25","unstructured":"Millen, J.: A CAPSL connector to Athena. In: Veith, H., Heintze, N., Clarke, E. (eds.) Workshop of Formal Methods and Computer Security (2000)"},{"key":"9003_CR26","doi-asserted-by":"crossref","unstructured":"Millen, J., Denker, G.: CAPSL and MuCAPSL. J. Telecommun. Info. Technol. (4), 16\u201327 (2002)","DOI":"10.26636\/jtit.2002.4.148"},{"key":"9003_CR27","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communication Security, pp. 166\u2013175. ACM SIGSAC (2001)","DOI":"10.1145\/502006.502007"},{"key":"9003_CR28","unstructured":"Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press (1999)"},{"key":"9003_CR29","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using mur\u03c6. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 141\u2013153. IEEE Computer Society Press (1997)","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"9003_CR30","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/24592.24594","volume":"211","author":"D. Otway","year":"1987","unstructured":"Otway, D., Rees, O.: Efficient and timely mutual authentication. Oper. Sys. Rew. 21(1), 8\u201310 (1987)","journal-title":"Oper. Sys. Rew."},{"key":"9003_CR31","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"61","author":"L. Paulson","year":"1998","unstructured":"Paulson, L.: The inductive approach to verifying cryptographic protocols. J. Comp. Security 6(1), 85\u2013128 (1998)","journal-title":"J. Comp. Security"},{"key":"9003_CR32","unstructured":"Reich, S.: Implementing and Extending the MSR Crypto-Protocol Specification Language. Diplomarbeit. Universit\u00e4t Hamburg, Fachbereich Informatik (April 2006)"},{"key":"9003_CR33","doi-asserted-by":"crossref","unstructured":"Stehr, M.-O.: CINNI\u2014A generic calculus of explicit substitutions and its application to \u03bb-, \u03c3- and \u03c0-calculi. In: Futatsugi, K. (ed.) 3rd International Workshop on Rewriting Logic and its Applications, vol. 36 of ENTCS, pp. 71\u201392. Elsevier (2000) http\/\/www.elsevier.nl\/locate\/entcs\/volume36.html","DOI":"10.1016\/S1571-0661(05)80125-2"},{"key":"9003_CR34","unstructured":"Stehr, M.-O.: Programming, Specification, and Interactive Theorem Proving\u2014Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory. Doctoral Thesis, Universit\u00e4t Hamburg, Fachbereich Informatik, Germany (2002), http:\/\/www.sub.uni-hamburg.de\/disse\/810\/"},{"issue":"1\u20132","key":"9003_CR35","doi-asserted-by":"crossref","first-page":"131","DOI":"10.3233\/FUN-2005-681-205","volume":"68","author":"M.-O. Stehr","year":"2005","unstructured":"Stehr, M.-O.: The open calculus of constructions (part i): An equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundamenta Informaticae 68(1\u20132), 131\u2013174 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"9003_CR36","doi-asserted-by":"crossref","first-page":"249","DOI":"10.3233\/FUN-2005-68304","volume":"683","author":"M.-O. Stehr","year":"2005","unstructured":"Stehr, M.-O.: The open calculus of constructions (part ii): An equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundamenta Informaticae 68(3), 249\u2013288 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"9003_CR37","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic. In: From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl, vol. 2635 of LNCS. Springer-Varlag (2004)"},{"key":"9003_CR38","unstructured":"Thayer, J., Herzog, J., Guttman, J.: Strand spaces: Why is a security protocol correct? In: 1998 IEEE Symposium on Security and Privacy, pp. 160\u2013171. IEEE Computer Society (1998)"},{"key":"9003_CR39","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University (2003)","DOI":"10.21236\/ADA418517"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9003-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9003-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9003-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,14]],"date-time":"2025-01-14T04:14:52Z","timestamp":1736828092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9003-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,24]]},"references-count":39,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,4,4]]}},"alternative-id":["9003"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9003-3","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2,24]]}}}