{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:42:39Z","timestamp":1725486159170},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426103"},{"type":"electronic","value":"9783540454182"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45418-7_10","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T21:08:09Z","timestamp":1180904889000},"page":"111-123","source":"Crossref","is-referenced-by-count":0,"title":["CardS4: Modal Theorem Proving on Java Smartcards"],"prefix":"10.1007","author":[{"given":"Rajeev Prabhakar","family":"Gor\u00e9","sequence":"first","affiliation":[]},{"given":"Phuong Th\u00ea","family":"Nguy\u00ean","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems, 8:18\u201336, 1990.","journal-title":"ACM Transactions on Computer Systems"},{"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.","key":"10_CR2","DOI":"10.1007\/BFb0095042"},{"key":"10_CR3","series-title":"Synthese Library","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library. D. Reidel, Dordrecht, Holland, 1983."},{"unstructured":"Pierre Girard. Which security policy for multiapplication smart cards. In Proceedings USENIX Workshop on Smartcard Technology, pages 21\u201328, Chicago, USA, 1999.","key":"10_CR4"},{"key":"10_CR5","series-title":"CSLI Lecture Notes","volume-title":"Logics of Time and Computation","author":"R. I. Goldblatt","year":"1987","unstructured":"R. I. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes Number 7, Center for the Study of Language and Information, Stanford, 1987."},{"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.","key":"10_CR6","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"10_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45744-5","volume-title":"Proc. Java Card Workshop","author":"R. Gor\u00e9","year":"2001","unstructured":"R Gor\u00e9 and L. D. Nguyen. CardKt: Automated Multi-modal Deduction on Javacards for Multi-application Security. In Proc. Java Card Workshop. Springer LNCS, to appear 2001."},{"key":"10_CR8","volume-title":"Automated Deduction in Some Propositional Modal Logics","author":"A. Heuerding","year":"1999","unstructured":"A. Heuerding. Automated Deduction in Some Propositional Modal Logics. Institut f\u00fcr Angewandte Mathematik und Informatik. Universit\u00e4te Bern, Switzerland, 1999."},{"doi-asserted-by":"crossref","unstructured":"G. E. Hughes and M. J. Cresswell. A New Introduction To Modal Logic. Routledge, 1996.","key":"10_CR9","DOI":"10.4324\/9780203290644"},{"unstructured":"J. Hudelmaier. Improved decision procedures for the modal logics K, T and S4.","key":"10_CR10"},{"issue":"3","key":"10_CR11","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","unstructured":"R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing, 6(3):467\u2013480, September 1977.","journal-title":"SIAM Journal of Computing"},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","unstructured":"Richard Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing, 6(3):467\u2013480, 1977.","journal-title":"SIAM Journal of Computing"},{"key":"10_CR13","series-title":"PhD thesis","volume-title":"Contributions to Authentication Logics and Analysis of Authentication Protocols","author":"A. Mathuria","year":"1997","unstructured":"Anish Mathuria. Contributions to Authentication Logics and Analysis of Authentication Protocols. PhD thesis, School of Information Technology and Computer Science, University of Woolongong, Woolongong, Australia, 1997."},{"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. \n                    http:\/\/www.gemplus.com\/smart\/r_d\/projects\/pacap.htm\n                    \n                  .","key":"10_CR14"},{"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":"10_CR15"},{"unstructured":"Grigori F. Shvarts. Autoepistemic modal logics. In Rohit Parikh, editor, Theoretical Aspects About Reasoning About Knowledge, pages 97\u2013109, 1990.","key":"10_CR16"}],"container-title":["Lecture Notes in Computer Science","Smart Card Programming and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45418-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T03:52:27Z","timestamp":1550375547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}