{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T05:53:03Z","timestamp":1768542783158,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425250","type":"print"},{"value":"9783540447559","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_8","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"91-104","source":"Crossref","is-referenced-by-count":20,"title":["Mechanical Proofs about a Non-repudiation Protocol"],"prefix":"10.1007","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"8_CR1","unstructured":"G. Bella. Message Reception in the Inductive Approach. Research Report 460, University of Cambridge \u2014 Computer Laboratory, 1999."},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 7th International Workshop on Security Protocols","author":"G. Bella","year":"1999","unstructured":"G. Bella. Modelling Agents\u2019 Knowledge Inductively. In Proc. of the 7th International Workshop on Security Protocols, LNCS 1796. Springer-Verlag, 1999."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of International Conference on Research in Smart Cards (e-Smart\u201901)","author":"G. Bella","year":"2001","unstructured":"G. Bella. Mechanising a protocol for smart cards. In Proc. of International Conference on Research in Smart Cards (e-Smart\u201901), LNCS. Springer-Verlag, 2001. In Press."},{"key":"8_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/10722599_10","volume-title":"Proc. of the 6th European Symposium on Research in Computer Security (ESORICS 2000)","author":"G. Bella","year":"2000","unstructured":"G. Bella, F. Massacci, L.C. Paulson, and P. Tramontano. Formal Verification of Cardholder Registration in SET. In F. Cuppens, Y. Deswarte, D. Gollmann, and M. Waidner, editors, Proc. of the 6th European Symposium on Research in Computer Security (ESORICS 2000), LNCS 1895, pages 159\u2013174. Springer-Verlag, 2000."},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Proc. of the 5th European Symposium on Research in Computer Security (ESORICS\u201998)","author":"G. Bella","year":"1998","unstructured":"G. Bella and L.C. Paulson. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In J.-J. Quisquater, Y. Deswarte, C. Meadows, and D. Gollmann, editors, Proc. of the 5th European Symposium on Research in Computer Security (ESORICS\u201998), LNCS 1485, pages 361\u2013375. Springer-Verlag, 1998."},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/BFb0028763","volume-title":"Proc. of the International Conference on Computer-Aided Verification (CAV\u201998)","author":"G. Bella","year":"1998","unstructured":"G. Bella and L.C. Paulson. Mechanising BAN Kerberos by the Inductive Method. In A. J. Hu and M. Y. Vardi, editors, Proc. of the International Conference on Computer-Aided Verification (CAV\u201998), LNCS 1427, pages 416\u2013427. Springer-Verlag, 1998."},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/18.50372","volume":"36","author":"M. Ben-Or","year":"1990","unstructured":"M. Ben-Or, O. Goldreich, S. Micali, and R. Rivest. A Fair Protocol for Signing Contracts. IEEE Transactions on Information Theory, 36(1):40\u201346, 1990.","journal-title":"IEEE Transactions on Information Theory"},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C.A. Meadows","year":"1996","unstructured":"C.A. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2):113\u2013131, 1996.","journal-title":"Journal of Logic Programming"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"T. Okamoto and K. Ohta. How to Simultaneously Exchange Secrets by General Assumptions. In Proc. of the 2nd ACM Conference on Computer and Communication Security (CCS\u201994), pages 184\u2013192, 1994.","DOI":"10.1145\/191177.191221"},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle: A Generic Theorem Prover. LNCS 828. Springer-Verlag, 1994."},{"key":"8_CR11","unstructured":"L.C. Paulson. Theory for public-key protocols, 1996. \n                    http:\/\/www4.informatik.tu-muenchen.de\/~isabelle\/library\/HOL\/Auth\/Public.html\n                    \n                  ."},{"key":"8_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"L.C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 6:85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Inductive Analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security, 1999. In press.","DOI":"10.1145\/322510.322530"},{"key":"8_CR14","unstructured":"P.Y.A. Ryan and S.A. Schneider. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2000."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"S. Schneider. Verifying Authentication Protocols with CSP. In Proc. of the 10th IEEE Computer Security Foundations Workshop, pages 3\u201317. IEEE Computer Society Press, 1997.","DOI":"10.1109\/CSFW.1997.596775"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"S. Schneider. Formal Analysis of a Non-Repudiation Protocol. In Proc. of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 1998.","DOI":"10.1109\/CSFW.1998.683155"},{"key":"8_CR17","unstructured":"G. Zhou and D. Gollmann. Towards Verification of Non-Repudiation Protocols. In Proc. of the 1998 International Refinement Workshop and Formal Methods Pacific, pages 370\u2013380. Springer-Verlag, 1998."},{"key":"8_CR18","unstructured":"J. Zhou and D. Gollmann. A Fair Non-Repudiation Protocol. In Proc. of the 15th IEEE Symposium on Security and Privacy, pages 55\u201361. IEEE Computer Society Press, 1996."},{"key":"8_CR19","unstructured":"J. Zhou and D. Gollmann. An Efficient Non-Repudiation Protocol. In Proc. of the 10th IEEE Computer Security Foundations Workshop, pages 126\u2013132. IEEE Computer Society Press, 1996."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T06:38:35Z","timestamp":1550731115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}