{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:12:55Z","timestamp":1725574375907},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540238065"},{"type":"electronic","value":"9783540304982"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30498-2_37","type":"book-chapter","created":{"date-parts":[[2011,1,8]],"date-time":"2011-01-08T00:21:59Z","timestamp":1294446119000},"page":"364-374","source":"Crossref","is-referenced-by-count":0,"title":["A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals"],"prefix":"10.1007","author":[{"given":"Juan Carlos","family":"L\u00f3pez","sequence":"first","affiliation":[]},{"given":"Ra\u00fal","family":"Monroy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","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. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"Proceedings of the 9th Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, R., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 111\u2013120X. Springer, Heidelberg (1988)"},{"key":"37_CR3","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning\u00a07, 303\u2013324 (1991)","journal-title":"Journal of Automated Reasoning"},{"key":"37_CR4","first-page":"116","volume-title":"Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI 1993","author":"D. Basin","year":"1993","unstructured":"Basin, D., Walsh, T.: Difference unification. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI 1993, San Mateo, CA, vol.\u00a01, pp. 116\u2013122. Morgan Kaufmann, San Francisco (1993)"},{"key":"37_CR5","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062, 185\u2013253 (1993)","journal-title":"Artificial Intelligence"},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0055131","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Boulton","year":"1998","unstructured":"Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 87\u2013104. Springer, Heidelberg (1998)"},{"key":"37_CR7","volume-title":"VLSI Specification","author":"M. Gordon","year":"1988","unstructured":"Gordon, M.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification. Kluwer, Dordrecht (1988)"},{"key":"37_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"37_CR9","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1008770222354","volume":"7","author":"R. Monroy","year":"2000","unstructured":"Monroy, R., Bundy, A., Green, I.: Planning Proofs of Equations in CCS. Automated Software Engineering\u00a07, 263\u2013304 (2000)","journal-title":"Automated Software Engineering"},{"key":"37_CR10","unstructured":"Schneider, S.: Modelling Security Properties with CSP. Computer Science Department, Technical Report Series CSD-TR-96-04, Royal Holloway, University of London (1996)"},{"key":"37_CR11","first-page":"77","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 77\u201390. Academic Press, London (1990)"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence \u2013 IBERAMIA 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30498-2_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:04:49Z","timestamp":1620014689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30498-2_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540238065","9783540304982"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30498-2_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}