{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:27Z","timestamp":1761597027438},"publisher-location":"Berlin, Heidelberg","reference-count":19,"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_9","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T17:08:09Z","timestamp":1180890489000},"page":"95-110","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["An Operational Semantics of the Java Card Firewall"],"prefix":"10.1007","author":[{"given":"Marc","family":"\u00c9luard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewen","family":"Denne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"9_CR1","unstructured":"Java Card 2.1.1. \n                    http:\/\/java.sun.com\/products\/javacard\/javacard21.html\n                    \n                  ."},{"key":"9_CR2","unstructured":"The bali project, Last visited 2001. \n                    http:\/\/www4.informatik.tu-muenchen.de\/~isabelle\/bali\/\n                    \n                  ."},{"key":"9_CR3","unstructured":"The loop project, Last visited 2001. \n                    http:\/\/www.cs.kun.nl\/~bart\/LOOP\/\n                    \n                  ."},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Formal syntax and semantics of Java","year":"1999","unstructured":"Jim Alves-Foss, editor. Formal syntax and semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer-Verlag, 1999. 404 pages."},{"key":"9_CR5","unstructured":"Peter Bertelsen. Semantics of Java Byte Code. Technical report, Dep. of Information Technology, Technical University of Denmark, March 1997. Home page \n                    http:\/\/www.dina.kvl.dk\/~pmb\/\n                    \n                  ."},{"key":"9_CR6","unstructured":"Peter Bertelsen. Dynamic semantics of Java bytecode. In Workshop on Principles on Abstract Machines, September 1998. Home page \n                    http:\/\/www.dina.kvl.dk\/~pmb\/\n                    \n                  ."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Java Card Workshop (JCW)","author":"P. Bieber","year":"2000","unstructured":"Pierre Bieber, Jacques Cazin, Abdellah El Marouani, Pierre Girard, Jean-Louis Lanet, Virginie Wiels, and Guy Zanon. The PACAP prototype: a tool for detecting Java Card illegal flow. In Isabelle Attali and Thomas Jensen, editors, Java Card Workshop (JCW), volume 2041 of Lecture Notes in Computer Science, September 2000."},{"key":"9_CR8","unstructured":"Zhiqun Chen. Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. Addison Wesley, 2000."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Ewen Denney and Thomas Jensen. Correctness of Java Card method lookup via logical relations. In 9th European Symp. on Programming (ESOP), pages 104\u2013118. Springer-Verlag, March 2000.","DOI":"10.1007\/3-540-46425-5_7"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Stephen N. Freund and John C. Mitchell. A formal framework for the Java bytecode language and verifier. Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 34(10):147\u2013166, November 1999.","DOI":"10.1145\/320384.320397"},{"key":"9_CR11","unstructured":"James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification, Second Edition. Addison Wesley, 2000. 896 pages, \n                    http:\/\/java.sun.com\/docs\/books\/jls\/index.html\n                    \n                  ."},{"key":"9_CR12","unstructured":"Sun Microsystems. Java Card 2.1.1 runtime environment (JCRE) specification, May 2000. Revision 1.0, 61 pages."},{"key":"9_CR13","unstructured":"St\u00e9phanie Motr\u00e9. Mod\u00e9lisation et impl\u00e9mentation formelle de la politique de s\u00e9curit\u00e9 dynamique de la Java Card. In Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciel (AFADL), pages 158\u2013172. LSR\/IMAG, January 2000."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Erik Poll, Joachim van den Berg, and Bart Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, 4th Smart Card Research and Advanced Application Conf. (CARDIS), pages 135\u2013154. Kluwer Acad. Publ., 2000.","DOI":"10.1007\/978-0-387-35528-3_8"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Erik Poll, Joachim van den Berg, and Bart Jacobs. Formal specification of the JavaCard API in JML: the APDU class. Computer Networks Magazine, 2001.","DOI":"10.1016\/S1389-1286(01)00163-3"},{"key":"9_CR16","unstructured":"Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle\/HOL. Technical Report TUM-I9816, Institut f\u00fcr informatik, Technische Universt\u00e4t M\u00fcnchen, 1998."},{"key":"9_CR17","unstructured":"Soot: a Java optimization framework. \n                    http:\/\/www.sable.mcgill.ca\/soot\/\n                    \n                  ."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"David von Oheimb. Hoare logic for Java in Isabelle\/HOL. Concurrency: Practice and Experience, 2001.","DOI":"10.1002\/cpe.598"},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 119\u2013156. Springer-Verlag, 1999."}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:38:50Z","timestamp":1558258730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_9","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"}}]}}