{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:08:33Z","timestamp":1725548913969},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236351"},{"type":"electronic","value":"9783540376217"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-37621-7_3","type":"book-chapter","created":{"date-parts":[[2010,2,28]],"date-time":"2010-02-28T19:29:47Z","timestamp":1267385387000},"page":"45-64","source":"Crossref","is-referenced-by-count":2,"title":["Formal Analysis of the NetBill Electronic Commerce 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","reference":[{"key":"3_CR1","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. Information Processing Letters\u00a056, 131\u2013133 (1995)","journal-title":"Information Processing Letters"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0020-0190(02)00480-5","volume":"86","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Information Processing Letters\u00a086, 57\u201362 (2003)","journal-title":"Information Processing Letters"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Abadi","year":"1990","unstructured":"Abadi, M., Burrows, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems\u00a08, 18\u201336 (1990)","journal-title":"ACM Transactions on Computer Systems"},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J.T. F\u00e1brega","year":"1999","unstructured":"F\u00e1brega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"3_CR5","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":"3_CR6","series-title":"ENTCS","volume-title":"WRLA 2002","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: WRLA 2002. ENTCS, vol.\u00a071. Elsevier Science Publishers, Amsterdam (2002)"},{"key":"3_CR7","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":"3_CR8","unstructured":"MasterCard\/Visa: SET secure electronic transactions protocol. Book One: Business Specifications, Book Two: Technical Specification, Book Three: Formal Protocol Definition (1997), \n                    \n                      http:\/\/www.setco.org\/set_specifications.html"},{"key":"3_CR9","unstructured":"Cox, B., Tygar, J.D., Sirbu, M.: NetBill security and transaction protocol. In: First USENIX Workshop on Electronic Commerce, pp. 77\u201388 (1995)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-36532-X_25","volume-title":"Software Security \u2013 Theories and Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 441\u2013460. Springer, Heidelberg (2003)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-36384-X_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal verification of the Horn-Preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 238\u2013252. Springer, Heidelberg (2002)"},{"key":"3_CR12","unstructured":"CafeOBJ: CafeOBJ homepage (2001), \n                    \n                      http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"3_CR13","series-title":"AMAST Series in Computing, 6","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ report","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, 6. World Scientific, Singapore (1998)"},{"key":"3_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 Transactions on Information Theory\u00a0IT-29, 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"3_CR16","unstructured":"Heintze, N., Tygar, J., Wing, J., Wong, H.C.: Model checking electronic commerce protocols. In: Second USENIX Workshop on Electronic Commerce, pp. 147\u2013164 (1996)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Transactions on Information and System Security\u00a02, 332\u2013351 (1999)","journal-title":"ACM Transactions on Information and System Security"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","first-page":"159","volume-title":"ESORICS 2000","author":"G. Bella","year":"1997","unstructured":"Bella, G., Massacci, F., Paulson, L.C., Tramontano, P.: Formal verification of Cardholder Registration in SET. In: ESORICS 2000. LNCS, vol.\u00a01709, pp. 159\u2013174. Springer, Heidelberg (1997)"},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"21","author":"G. Bella","year":"2003","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET registration protocols. IEEE Journal on Selected Area in Communications\u00a021, 77\u201387 (2003)","journal-title":"IEEE Journal on Selected Area in Communications"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/586110.586113","volume-title":"9th ACM CCS","author":"G. Bella","year":"2002","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: The verification of an industrial payment protocol: The SET purchase phase. In: 9th ACM CCS, pp. 12\u201320. ACM Press, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Software Security - Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-37621-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:40:54Z","timestamp":1605742854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-37621-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236351","9783540376217"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-37621-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}