{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:42:47Z","timestamp":1725486167013},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426103"},{"type":"electronic","value":"9783540454182"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45418-7_3","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T17:08:09Z","timestamp":1180890489000},"page":"19-33","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Mechanising a Protocol for Smart Cards"],"prefix":"10.1007","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"M. Abadi and R. M. Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering, 22(1):6\u201315, January 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","first-page":"125","volume-title":"Proc. of the 5th International Workshop on Security Protocols","author":"R. J. Anderson","year":"1997","unstructured":"R. J. Anderson and M. J. Kuhn. Low Cost Attacks on Tamper Resistant Devices. In M. e. a. Lomas, editor, Proc. of the 5th International Workshop on Security Protocols, LNCS 1361, pages 125\u2013136. Springer-Verlag, 1997."},{"key":"3_CR3","unstructured":"G. Bella. Message Reception in the Inductive Approach. Research Report 460, University of Cambridge \u2014 Computer Laboratory, 1999."},{"key":"3_CR4","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":"3_CR5","unstructured":"G. Bella. Inductive Verification of Cryptographic Protocols. PhD thesis, University of Cambridge, Computer Laboratory, 2000. Research Report 493."},{"key":"3_CR6","unstructured":"G. Bella and L. C. Paulson. Are Timestamps Worth the Effort? A Formal Treatment. Research Report 447, University of Cambridge \u2014 Computer Laboratory, 1998."},{"key":"3_CR7","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. Desware, 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":"3_CR8","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."},{"key":"3_CR9","unstructured":"R. Jerdonek, P. Honeyman, K. Coffman, J. Rees, and K. Wheeler. Implementation of a Provably Secure, Smartcard-based Key Distribution Protocol. In J.-J. Quisquater and B. Schneier, editors, Proc. of the 3rd Smart Card Research and Advanced Application Conference (CARDIS\u201998), 1998."},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","first-page":"456","volume-title":"Proc. of Advances in Cryptography \u2014 CRYPTO\u201993","author":"T. Leighton","year":"1993","unstructured":"T. Leighton and S. Micali. Secret-key Agreement without Public-key Cryptography. In D. R. Stinson, editor, Proc. of Advances in Cryptography \u2014 CRYPTO\u201993, LNCS 773, pages 456\u2013479. Springer-Verlag, 1993."},{"key":"3_CR11","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":"3_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":"3_CR13","unstructured":"P. Y. A. Ryan and S. A. Schneider. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2000."},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/3-540-68339-9_28","volume-title":"Advances in Cryptology \u2014 Eurocrypt\u201996","author":"V. Shoup","year":"1996","unstructured":"V. Shoup and A. Rubin. Session Key Distribution using Smart Cards. In U. Maurer, editor, Advances in Cryptology \u2014 Eurocrypt\u201996, LNCS 1070, pages 321\u2013331. Springer-Verlag, 1996."}],"container-title":["Lecture Notes in Computer Science","Smart Card Programming and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45418-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:39:05Z","timestamp":1558258745000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"11 September 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}