{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:11Z","timestamp":1725514871629},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_15","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"198-213","source":"Crossref","is-referenced-by-count":10,"title":["Industrial Use of Formal Methods for a High-Level Security Evaluation"],"prefix":"10.1007","author":[{"given":"Boutheina","family":"Chetali","sequence":"first","affiliation":[]},{"given":"Quang-Huy","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"The Coq Development Team. The Coq Proof Assistant., \n                    \n                      http:\/\/coq.inria.fr\/"},{"key":"15_CR2","unstructured":"Sun Microsystems. Java Card 2.2 Virtual Machine Specification (2002), \n                    \n                      http:\/\/www.javasoft.com\/products\/javacard"},{"key":"15_CR3","unstructured":"Sun Microsystems. Java Card 2.2 Runtime Environment Specification (2002), \n                    \n                      http:\/\/www.javasoft.com\/products\/javacard"},{"key":"15_CR4","unstructured":"Sun Microsystems. Java Card 2.2 Application Programming Interface (2002), \n                    \n                      http:\/\/www.javasoft.com\/products\/javacard"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11733447_23","volume-title":"Smart Card Research and Advanced Applications","author":"Q.-H. Nguyen","year":"2006","unstructured":"Nguyen, Q.-H., Chetali, B.: Certifying Native Java Card API by Formal Refinement. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds.) CARDIS 2006. LNCS, vol.\u00a03928, pp. 313\u2013328. Springer, Heidelberg (2006)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1145\/1363686.1363777","volume-title":"Proc. of the 23th ACM Symposium on Applied Computing (SAC 2008)","author":"J. Andronick","year":"2008","unstructured":"Andronick, J., Nguyen, Q.-H.: Certifying an Embedded Remote Method Invocation Protocol. In: Proc. of the 23th ACM Symposium on Applied Computing (SAC 2008), pp. 352\u2013359. ACM Press, New York (2008)"},{"key":"15_CR7","unstructured":"Sun Microsystems. Java Card System Protection Profile Collection - Version 1.1 (2003), \n                    \n                      http:\/\/java.sun.com\/products\/javacard\/pp.html"},{"key":"15_CR8","unstructured":"Bundesam f\u00fcr Sicherheit\u00a0der Informationstechnik\u00a0(BSI). Evualuation methodology for CC assurance classes for EAL5+, June, Version 1.00. Ref. AIS34 (2004)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/10930755_22","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Andronick","year":"2003","unstructured":"Andronick, J., Chetali, B., Ly, O.: Using Coq to Verify Java Card Applet Isolation Properties. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 335\u2013351. Springer, Heidelberg (2003)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D. Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable Translator of B Specifications to Embedded C Programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/11526841_21","volume-title":"FM 2005: Formal Methods","author":"J. Andronick","year":"2005","unstructured":"Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal Verification of Security Properties of Smart Card Embedded Source Code. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 302\u2013317. Springer, Heidelberg (2005)"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"Procs. of POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Procs. of POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a c compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/11554578_5","volume-title":"Foundations of Security Analysis and Design III","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Dufay, G.: Formal Methods for Smartcard Security. In: Aldini, A., Gorrieri, R., Martinelli, F. (eds.) FOSAD 2005. LNCS, vol.\u00a03655, pp. 133\u2013177. Springer, Heidelberg (2005)"},{"issue":"4","key":"15_CR15","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"P.H. Hartel","year":"2001","unstructured":"Hartel, P.H., Moreau, L.: Formalising the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys\u00a033(4), 517\u2013558 (2001)","journal-title":"ACM Computing Surveys"},{"key":"15_CR16","unstructured":"Common Criteria, \n                    \n                      http:\/\/www.commoncriteria.org\/"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:35Z","timestamp":1620017015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_15","relation":{},"subject":[]}}