{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:17:14Z","timestamp":1778249834629,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540003489","type":"print"},{"value":"9783540363842","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36384-x_20","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:21:13Z","timestamp":1196328073000},"page":"238-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal Verification of the Horn-Preneel Micropayment Protocol"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/49.839936","volume":"18","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Garay, J.A., Hauser, R., Herzberg, A., Krawczyk, H., Steiner, M., Tsudik, G., Herreweghen, E.V., Waidner, M.: Design, implementation and deployment of the iKP secure electronic payment system. IEEE Journal of Selected Areas in Communications 18 (2000) 611\u2013627","journal-title":"IEEE Journal of Selected Areas in Communications"},{"key":"20_CR2","unstructured":"MasterCard\/Visa: SET secure electronic transactions protocol. Book One: Business Specifications, Book Two: Technical Specification, Book Three: Formal Protocol Definition (http:\/\/www.setco.org\/set specifications.html) (1997)"},{"key":"20_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-45760-7_11","volume-title":"Progress in Cryptology-CT-RSA 2002","author":"S. Micali","year":"2002","unstructured":"Micali, S., Rivest, R.L.: Micropayments revisited. In: Progress in Cryptology-CT-RSA 2002. LNCS 2271, Springer (2002) 149\u2013163"},{"key":"20_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BFb0055870","volume-title":"Computer Security-ESORICS 98","author":"G. Horn","year":"1998","unstructured":"Horn, G., Preneel, B.: Authentication and payment in future mobile systems. In: Computer Security-ESORICS 98. LNCS 1485, Springer-Verlag (1998) 277\u2013293"},{"key":"20_CR5","unstructured":"Hauser, R., Steiner, M., Waidner, M.: Micro-payments based on iKP. In: 14th Worldwide Congress on Computer and Communications Security Protection. (1996) 67\u201382"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56 (1995) 131\u2013133","journal-title":"Inf. Process. Lett."},{"key":"20_CR7","unstructured":"CafeOBJ: CafeOBJ web page. http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/ (2001)"},{"key":"20_CR8","volume-title":"AMAST Series in Computing","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, 6. World Scientific, Singapore (1998)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: WRLA\u2019 02. Volume 71 of ENTCS., Elsevier Science Publishers (2002)","DOI":"10.1016\/S1571-0661(05)82536-8"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S0304-3975(99)00275-3","volume":"245","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Malcolm, G.: A hidden agenda. Theor. Comput. Sci. 245 (2000) 55\u2013101","journal-title":"Theor. Comput. Sci."},{"key":"20_CR11","volume-title":"Parallel program design: a foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel program design: a foundation. Addison-Wesley, Reading, MA (1988)"},{"key":"20_CR12","series-title":"Lect Notes Comput Sci","first-page":"59","volume-title":"Security Protocols","author":"T.P. Pedersen","year":"1996","unstructured":"Pedersen, T.P.: Electronic payments of small amounts. In: Security Protocols. LNCS 1189, Springer-Verlag (1996) 59\u201368"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"770","DOI":"10.1145\/358790.358797","volume":"24","author":"L. Lamport","year":"1981","unstructured":"Lamport, L.: Passward authentication with insecure communications. Comm. ACM 24 (1981) 770\u2013772","journal-title":"Comm. ACM"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inform. Theory IT-29 (1983) 198\u2013208","journal-title":"IEEE Trans. Inform. Theory"},{"key":"20_CR15","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. Comput. Security 6 (1998) 85\u2013128","journal-title":"J. Comput. Security"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S. Schneider","year":"1998","unstructured":"Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24 (1998) 741\u2013758","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36384-X_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:56:54Z","timestamp":1778248614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36384-X_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,16]]},"ISBN":["9783540003489","9783540363842"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-36384-x_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002,12,16]]},"assertion":[{"value":"16 December 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}