{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:22:09Z","timestamp":1725488529810},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421672"},{"type":"electronic","value":"9783540451655"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45165-x_4","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T06:17:47Z","timestamp":1186726667000},"page":"38-51","source":"Crossref","is-referenced-by-count":0,"title":["CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Gor\u00e9","sequence":"first","affiliation":[]},{"given":"Lan Duy","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,18]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"N Bonnette and R Gor\u00e9. A labelled sequent system for tense logic Kt. In AI98: Proceedings of the Australian Joint Conference on Artificial Intelligence, LNAI 1502:71\u201382. Springer, 1998.","DOI":"10.1007\/BFb0095042"},{"key":"4_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-48754-9_5","volume-title":"Proc. International Conference on Theorem Proving with Analytic Tableau","author":"V. Boyapati","year":"1999","unstructured":"V Boyapati and R Gor\u00e9. System description: KtSeqC. In N. Murray, editor, Proc. International Conference on Theorem Proving with Analytic Tableau, volume LNCS 1617: 29\u201331. Springer, 1999."},{"issue":"1","key":"4_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1305\/ndjfl\/1093634564","volume":"34","author":"P. Blackburn","year":"1993","unstructured":"P Blackburn. Nominal tense logic. Notre Dame Journal of Formal Logic, 34(1):56\u201383, 1993.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"4_CR4","unstructured":"P Girard. Which security policy for multiapplication smart cards. In Proceedings USENIX Workshop on Smartcard Technology, pages 21\u201328, Chicago, USA, 1999."},{"key":"4_CR5","unstructured":"G Grimaud, J-L Lanet, and J-J Vandewalle. FACADE: a typed intermediate language dedicated to smart cards. Technical report, Gemplus Research, http:\/\/www.gemplus.com\/smart\/r_d\/publications\/index.html ,1999."},{"key":"4_CR6","unstructured":"R. I. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes No. 7, Center for the Study of Language and Information, Stanford, 1987."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"R Gor\u00e9. Chapter 6: Tableau methods for modal and temporal logics. In M D\u2019Agostino, D Gabbay, R H\u00e4nle, J Posegga, editor, Handbook of Tableau Methods, pages 297\u2013396. Kluwer Academic Publishers, 1999.","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"G. E. Hughes and M. J. Cresswell. A New Introduction To Modal Logic. Routledge, 1996.","DOI":"10.4324\/9780203290644"},{"key":"4_CR9","unstructured":"Funge Inc. http:\/\/www.funge.net\/ , 1999."},{"issue":"3","key":"4_CR10","first-page":"1","volume":"15","author":"B. Lampson","year":"1993","unstructured":"B Lampson M Abadi, M Burrows and G Plotkin. A calculus for access control in distributed systems. AM Transactions on Programming Languages and Systems, 15(3):1\u201329, 1993.","journal-title":"AM Transactions on Programming Languages and Systems"},{"key":"4_CR11","unstructured":"A Mathuria. Contributions to Authentication Logics and Analysis of Authentication Protocols. PhD thesis, School of Information Technology and Computer Science, University of Wollongong, Australia, 1997."},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Abadi","year":"1990","unstructured":"M Abadi M Burrows and R Needham. A logic of authentication. ACM Transactions on Computer Systems, 8:18\u201336, 1990.","journal-title":"ACM Transactions on Computer Systems"},{"key":"4_CR13","unstructured":"Sun Microsystems. Sun\u2019s java web site. http:\/\/www.java.sun.com , 2000."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"G Necula. Proof-carrying code. In Proc. of 24th Annual Symposium on Principles Of Programming Languages, 1997.","DOI":"10.1145\/263699.263712"},{"key":"4_CR15","unstructured":"P Girard J-L Lanet V Wiels G Zanon P Bieber, J Cazin. Checking secure interactions of smart card applets. Technical report, Gemplus R&D Centre, 2000. http:\/\/www.gemplus.com\/smart\/r_d\/projects\/pacap.htm ."},{"key":"4_CR16","unstructured":"C C Peter. http:\/\/www.cityu.edu.hk\/computer\/c3_smartcard.htm ."},{"key":"4_CR17","unstructured":"A Rao and M Georgeff. A model-theoretic approach to the verification of situated reasoning systems. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 318\u2013324. Morgan-Kauffman, 1993."},{"key":"4_CR18","unstructured":"A Slater, R Gor\u00e9, J Posegga, and H Vogt. CardTAP: Automated theorem proving on a smart card. In AI98: Proceedings of the Australian Joint Conference on Artificial Intelligence, LNAI 1502:239\u2013248. Springer, 1998."},{"key":"4_CR19","unstructured":"G F. Shvarts. Autoepistemic modal logics. In Rohit Parikh, editor, Theoretical Aspects About Reasoning About Knowledge, pages 97\u2013109, 1990."}],"container-title":["Lecture Notes in Computer Science","Java on Smart Cards:Programming and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45165-X_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:12:11Z","timestamp":1556734331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45165-X_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421672","9783540451655"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45165-x_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}