{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:44:51Z","timestamp":1771703091690,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_22","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"335-351","source":"Crossref","is-referenced-by-count":14,"title":["Using Coq to Verify Java CardTM Applet Isolation Properties"],"prefix":"10.1007","author":[{"given":"June","family":"Andronick","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boutheina","family":"Chetali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Ly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Andronick, J., Chetali, B., Ly, O.: Formal Verification of the Confidentiality Property in Java CardTM Technology. Submitted at Journal of Logic and Algebraic Programming"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45418-7_2","volume-title":"Smart Card Programming and Security","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Huisman, M., de Sousa, S.M.: Jakarta: a Toolset to Reason about the JavaCard Platform. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, pp. 2\u201318. Springer, Heidelberg (2001)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., de Sousa, S.M.: A Formal Correspondence between Offencive and Defensive JavaCard Virtual Machine. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 32\u201345. Springer, Heidelberg (2002)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 302\u2013319. Springer, Heidelberg (2001)"},{"key":"22_CR5","unstructured":"Betarte, G., Chetali, B., Gimenez, E., Loiseaux, C.: Formavie: Formal Modelling and Verification of the JavaCard 2.1.1 Security Architecture. In: E-SMART 2002, pp. 213\u2013231 (2002)"},{"key":"22_CR6","volume-title":"Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide","author":"Z. Chen","year":"2000","unstructured":"Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. Addison Wesley, Reading (2000)"},{"key":"22_CR7","first-page":"233","volume-title":"13th IEEE Computer Security Foundations Workshop","author":"M. Dam","year":"2000","unstructured":"Dam, M., Giambiagi, P.: Confidentiality for Mobile Code: The Case of a Simple Payment Protocol. In: 13th IEEE Computer Security Foundations Workshop, July 2000, pp. 233\u2013244. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"22_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/SP.1982.10014","volume-title":"Proc. of the 1982 Symposium on Security and Privacy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security Policy and Security Models. In: Proc. of the 1982 Symposium on Security and Privacy, pp. 11\u201320. IEEE Computer Society Press, Los Alamitos (1982)"},{"key":"22_CR9","first-page":"75","volume-title":"Proc. of the 1982 Symposium on Security and Privacy","author":"J.A. Goguen","year":"1984","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and interference control. In: Proc. of the 1982 Symposium on Security and Privacy, pp. 75\u201386. IEEE Computer Society Press, Los Alamitos (1984)"},{"key":"22_CR10","volume-title":"Securing Java: Getting Down to Business with Mobile Code","author":"G. McGrow","year":"1999","unstructured":"McGrow, G., Felten, E.: Securing Java: Getting Down to Business with Mobile Code. John Wiley & Sons, Chichester (1999)"},{"key":"22_CR11","unstructured":"Sun Microsystems. Java Card 2.1.1 Specification (2000), http:\/\/java.sun.com\/products\/javacard\/"},{"key":"22_CR12","unstructured":"Sun Microsystems. Java Card 2.2 API Specification (2002), http:\/\/java.sun.com\/products\/javacard\/"},{"key":"22_CR13","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: A Type System for Checking Applet Isolation in Java Card. In: Drossopoulou, S., et al. (eds.) Proceedings of FTfJP 2001 (2001)"},{"key":"22_CR14","volume-title":"Java Security","author":"S. Oaks","year":"1998","unstructured":"Oaks, S.: Java Security. O\u2019Reilly, Sebastopol (1998)"},{"key":"22_CR15","unstructured":"Poll, E., Hartel, P., de Jong, E.: A Java Reference Model of Transacted Memory for Smart Cards. In: Fifth Smart Card Research and Advanced Application Conf, CARDIS 2002 (2002) (to appear), See http:\/\/www.cs.kun.nl\/VerifiCard\/files\/publications.html"},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S1389-1286(01)00163-3","volume":"36","author":"E. Poll","year":"2001","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Formal specification of the Java Card API in JML: the APDU class. Computer Networks\u00a036(4), 407\u2013421 (2001)","journal-title":"Computer Networks"},{"key":"22_CR17","unstructured":"The Coq Development Team LogiCal Project. The Coq Proof Assistant Reference Manual, http:\/\/pauillac.inria.fr\/coq\/doc\/main.html"},{"key":"22_CR18","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies (December 1992)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"van den Berg, J., Jacobs, B., Poll, E.: Formal Specification and Verification of JavaCard\u2019s Application Identifier Class. In: Proceedings of the Java Card 2000 Workshop (2000), http:\/\/www.irisa.fr\/lande\/jensen\/jcw-program.html","DOI":"10.1007\/3-540-45165-X_11"},{"key":"22_CR21","volume-title":"Inside the Java Virtual Machine","author":"B. Venners","year":"1997","unstructured":"Venners, B.: Inside the Java Virtual Machine. McGraw-Hill, New York (1997)"}],"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\/10930755_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T15:40:19Z","timestamp":1586965219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/10930755_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}