{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T16:32:32Z","timestamp":1792945952867,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540204916","type":"print"},{"value":"9783540399582","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39958-2_12","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:06:04Z","timestamp":1294394764000},"page":"170-184","source":"Crossref","is-referenced-by-count":53,"title":["Proof Scores in the OTS\/CafeOBJ Method"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A Logical Approach to Discrete Math","author":"D. Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)"},{"key":"12_CR2","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","year":"2000","unstructured":"Goguen, J., Malcolm, G. (eds.): Software Engineering with OBJ: Algebraic Specification in Action. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"12_CR3","first-page":"357","volume-title":"APAQS 2001","author":"K. Ogata","year":"2001","unstructured":"Ogata, K., Futatsugi, K.: Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm. In: APAQS 2001, pp. 357\u2013366. IEEE CS Press, Los Alamitos (2001)"},{"key":"12_CR4","first-page":"181","volume-title":"FMOODS 2002","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: FMOODS 2002, pp. 181\u2013195. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"12_CR5","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":"12_CR6","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":"12_CR7","unstructured":"CafeOBJ: CafeOBJ web page (2001), http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, 6. World Scientific, Singapore (1998)","DOI":"10.1142\/3831"},{"key":"12_CR9","first-page":"74","volume":"6","author":"R. Diaconescu","year":"2000","unstructured":"Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. Journal of Universal Computer Science\u00a06, 74\u201396 (2000)","journal-title":"Journal of Universal Computer Science"},{"key":"12_CR10","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.\u00a056, 131\u2013133 (1995)","journal-title":"Inf. Process. Lett."},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"12_CR12","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 (1988)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Comm. ACM\u00a021, 993\u2013999 (1978)","journal-title":"Comm. ACM"},{"key":"12_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\u00a0IT-29, 198\u2013208 (1983)","journal-title":"IEEE Trans. Inform. Theory"},{"key":"12_CR15","unstructured":"Hsiang, J.: Refutational Theorem Proving using Term Rewriting Systems. PhD thesis, University of Illinois at Champaign-Urbana (1981)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higer-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1644","DOI":"10.1007\/3-540-48118-4_37","volume-title":"FM\u201999 - Formal Methods","author":"R. Diaconescu","year":"1999","unstructured":"Diaconescu, R., Futatsugi, K., Iida, S.: Component-based algebraic specification and verification in CafeOBJ. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1644\u20131663. Springer, Heidelberg (1999)"},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/CSFW.1997.596782","volume-title":"10th IEEE Computer Security Foundations Workshop","author":"G. Lowe","year":"1997","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: 10th IEEE Computer Security Foundations Workshop, pp. 31\u201343. IEEE CS Press, Los Alamitos (1997)"},{"key":"12_CR19","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)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Open Object-Based Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39958-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T13:41:30Z","timestamp":1559914890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39958-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204916","9783540399582"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39958-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}