{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T20:51:52Z","timestamp":1761339112546},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642124587"},{"type":"electronic","value":"9783642124594"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12459-4_18","type":"book-chapter","created":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T02:49:38Z","timestamp":1272509378000},"page":"248-262","source":"Crossref","is-referenced-by-count":5,"title":["Integrating Automated and Interactive Protocol Verification"],"prefix":"10.1007","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian A.","family":"M\u00f6dersheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., H\u00e9am, P.C., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005), \n                    \n                      http:\/\/www.avispa-project.org"},{"issue":"1","key":"18_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"6","author":"A. Armando","year":"2007","unstructured":"Armando, A., Compagna, L.: SAT-based Model-Checking for Security Protocols Analysis. Int. J. of Information Security\u00a06(1), 3\u201332 (2007)","journal-title":"Int. J. of Information Security"},{"key":"18_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68136-6","volume-title":"Formal Correctness of Security Protocols","author":"G. Bella","year":"2007","unstructured":"Bella, G.: Formal Correctness of Security Protocols. Springer, Heidelberg (2007)"},{"key":"18_CR4","first-page":"82","volume-title":"CSFW 2001","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW 2001, pp. 82\u201396. IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"5","key":"18_CR5","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.ipl.2005.05.011","volume":"95","author":"B. Blanchet","year":"2005","unstructured":"Blanchet, B.: Security protocols: from linear to classical logic by abstract interpretation. Information Processing Letters\u00a095(5), 473\u2013479 (2005)","journal-title":"Information Processing Letters"},{"key":"18_CR6","unstructured":"Boichut, Y., H\u00e9am, P.C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: AVIS 2004, pp. 1\u201311 (2004)"},{"issue":"1","key":"18_CR7","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10009-005-0189-6","volume":"8","author":"L. Bozga","year":"2006","unstructured":"Bozga, L., Lakhnech, Y., Perin, M.: Pattern-based abstraction for verifying secrecy in protocols. Int. J. on Software Tools for Technology Transfer\u00a08(1), 57\u201376 (2006)","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"18_CR8","unstructured":"Brucker, A., M\u00f6dersheim, S.: Integrating Automated and Interactive Protocol Verification (extended version). Tech. Rep. RZ3750, IBM Zurich Research Lab (2009), \n                    \n                      http:\/\/domino.research.ibm.com\/library\/cyberdig.nsf"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-36532-X_22","volume-title":"Software Security \u2013 Theories and Systems","author":"I. Cervesato","year":"2003","unstructured":"Cervesato, I., Durgin, N., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 356\u2013383. Springer, Heidelberg (2003)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-45657-0_24","volume-title":"Computer Aided Verification","author":"Y. Chevalier","year":"2002","unstructured":"Chevalier, Y., Vigneron, L.: Automated Unbounded Verification of Security Protocols. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 324\u2013337. Springer, Heidelberg (2002)"},{"key":"18_CR11","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocol: Literature: Version 1.0 (1997), \n                    \n                      http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"issue":"4","key":"18_CR12","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. of Foundations of Computer Science\u00a014(4), 583\u2013604 (2003)","journal-title":"Int. J. of Foundations of Computer Science"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-36575-3_8","volume-title":"Programming Languages and Systems","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 99\u2013113. Springer, Heidelberg (2003)"},{"issue":"2","key":"18_CR14","first-page":"324","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P.: Abstract interpretation. Symposium on Models of Programming Languages and Computation, ACM Computing Surveys\u00a028(2), 324\u2013328 (1996)","journal-title":"Symposium on Models of Programming Languages and Computation, ACM Computing Surveys"},{"key":"18_CR15","unstructured":"Cremers, C.: Scyther. Semantics and Verification of Security Protocols. Phd-thesis, University Eindhoven (2006)"},{"key":"18_CR16","unstructured":"Erk\u00f6k, L., Matthews, J.: Using Yices as an automated solver in Isabelle\/HOL. In: AFM 2008 (2008)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"18_CR18","first-page":"224","volume-title":"CSF 2008","author":"J. Goubault-Larrecq","year":"2008","unstructured":"Goubault-Larrecq, J.: Towards producing formally checkable security proofs, automatically. In: CSF 2008, pp. 224\u2013238. IEEE Computer Society, Los Alamitos (2008)"},{"key":"18_CR19","volume-title":"CSFW 2000","author":"J. Heather","year":"2000","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: CSFW 2000. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"18_CR21","unstructured":"Meier, S.: A formalization of an operational semantics of security protocols. Diploma thesis, ETH Zurich (2007), \n                    \n                      http:\/\/people.inf.ethz.ch\/meiersi\/fossp"},{"issue":"10","key":"18_CR22","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Information and Computation\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Information and Computation"},{"issue":"2\u20134","key":"18_CR23","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.ic.2007.07.006","volume":"206","author":"S. M\u00f6dersheim","year":"2008","unstructured":"M\u00f6dersheim, S.: On the Relationships between Models in Protocol Verification. J. of Information and Computation\u00a0206(2\u20134), 291\u2013311 (2008)","journal-title":"J. of Information and Computation"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","first-page":"166","volume-title":"FOSAD","author":"S. M\u00f6dersheim","year":"2007","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol.\u00a04677, pp. 166\u2013194. Springer, Heidelberg (2007)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer-Verlag (2002)"},{"issue":"1-2","key":"18_CR26","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. of Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"J. of Computer Security"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"L.C. Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 232\u2013245. Springer, Heidelberg (2007)"},{"key":"18_CR28","unstructured":"Roscoe, A.W., Goldsmith, M.: The perfect spy for model-checking crypto-protocols. In: DIMACS (1997)"},{"issue":"1","key":"18_CR29","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. of Applied Logic\u00a07(1), 26\u201340 (2009)","journal-title":"J. of Applied Logic"},{"key":"18_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: Spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-74591-4_26","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"2007","unstructured":"Wenzel, M., Wolff, B.: Building formal method tools in the Isabelle\/Isar framework. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 352\u2013367. Springer, Heidelberg (2007)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11690634_28","volume-title":"Foundations of Software Science and Computation Structures","author":"R. Zunino","year":"2006","unstructured":"Zunino, R., Degano, P.: Handling exp, \u00d7 (and Timestamps) in Protocol Analysis. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 413\u2013427. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12459-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T14:33:06Z","timestamp":1558276386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12459-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642124587","9783642124594"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12459-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}