{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:24Z","timestamp":1725490104464},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_23","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"302-318","source":"Crossref","is-referenced-by-count":6,"title":["A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Sprenger","sequence":"first","affiliation":[]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"Isabelle home page (2007), http:\/\/isabelle.in.tum.de"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003\/015 (January 2003)","DOI":"10.1145\/948109.948140"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proc. of Principles of Programming Languages (POPL) (2004)","DOI":"10.1145\/964001.964003"},{"key":"23_CR4","unstructured":"Brucker, A., Wolff, B.: A package for extensible object-oriented data models with an application to IMP++. In: International Verification Workshop (VERIFY) (August 2006)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48167-2_6","volume-title":"Types for Proofs and Programs","author":"J.-C. Filli\u00e2tre","year":"1999","unstructured":"Filli\u00e2tre, J.-C.: Proof of imperative programs in type theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, Springer, Heidelberg (1999)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/11541868_10","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Huffman","year":"2005","unstructured":"Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle\/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 147\u2013162. Springer, Heidelberg (2005)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest precondition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming\u00a058, 61\u201388 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0304-3975(02)00366-3","volume":"291","author":"B. Jacobs","year":"2003","unstructured":"Jacobs, B., Poll, E.: Coalgebras and monads in the semantics of Java. Theoretical Computer Science\u00a0291(3), 329\u2013349 (2003)","journal-title":"Theoretical Computer Science"},{"key":"23_CR10","first-page":"222","volume":"6","author":"B. Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bulletin\u00a06, 222\u2013259 (1997)","journal-title":"EATCS Bulletin"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-47813-2_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Krsti\u0107","year":"2002","unstructured":"Krsti\u0107, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 182\u2013195. Springer, Heidelberg (2002)"},{"key":"23_CR12","first-page":"93","volume":"17","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Software - Concepts and Tools\u00a017, 93\u2013102 (1996)","journal-title":"Software - Concepts and Tools"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-58450-1_52","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"T. L\u00e5ngbacka","year":"1994","unstructured":"L\u00e5ngbacka, T.: A HOL formalisation of the temporal logic of actions. In: Melham, T.F., Camilleri, J. (eds.) Higher Order Logic Theorem Proving and Its Applications. LNCS, vol.\u00a0859, pp. 332\u2013345. Springer, Heidelberg (1994)"},{"issue":"1","key":"23_CR14","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Computer Science\u00a083(1), 97\u2013139 (1991)","journal-title":"Theoretical Computer Science"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093, 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BFb0055146","volume-title":"Theorem Proving in Higher Order Logics","author":"W. Naraschewski","year":"1998","unstructured":"Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a01479, pp. 349\u2013366. Springer, Heidelberg (1998)"},{"key":"23_CR17","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer, Dordrecht (2002)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"23_CR19","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. Paulson","year":"1998","unstructured":"Paulson, L.: The inductive approach to verifying cryptographic protocols. J. Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"J. Computer Security"},{"key":"23_CR20","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-1-4471-3182-3_11","volume-title":"IVth Higher Order Workshop, Banff 1990","author":"A.M. Pitts","year":"1991","unstructured":"Pitts, A.M.: Evaluation logic. In: Birtwistle, G. (ed.) IVth Higher Order Workshop, Banff 1990. Workshops in Computing, pp. 162\u2013189. Springer, Heidelberg (1991)"},{"key":"23_CR21","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1109\/CSFW.2006.10","volume-title":"19th IEEE Computer Security Foundations Workshop","author":"C. Sprenger","year":"2006","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: 19th IEEE Computer Security Foundations Workshop, Venice, Italy, July 2006, pp. 153\u2013166. IEEE Computer Society, Los Alamitos (2006)"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-45614-7_6","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 89\u2013105. Springer, Heidelberg (2002)"},{"key":"23_CR23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:23:02Z","timestamp":1605763382000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}