{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:59:27Z","timestamp":1743130767141,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203001"},{"type":"electronic","value":"9783540396505"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39650-5_13","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T15:20:21Z","timestamp":1277479221000},"page":"217-234","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Security Model of the Infineon SLE 88 Smart Card Memory Management"],"prefix":"10.1007","author":[{"given":"David","family":"von Oheimb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Walter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Volkmar","family":"Lotz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Atmel, Hitachi Europe, Infineon Technologies, and Philips Semiconductors. Smartcard IC Platform Protection Profile, Version 1.0 (July 2001), \n                  \n                    http:\/\/www.bsi.de\/cc\/pplist\/ssvgpp01.pdf"},{"key":"13_CR2","unstructured":"Atmel, Hitachi Europe, Infineon Technologies, and Philips Semiconductors. Smartcard Integrated Circuit Platform Augmentations, Version 1.0 (March 2002), \n                  \n                    http:\/\/www.bsi.de\/cc\/pplist\/augpp002.pdf"},{"key":"13_CR3","unstructured":"Common Criteria for Information Technology Security Evaluation (CC), Version 2.1, ISO\/IEC 15408 (1999)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/3-540-48119-2_40","volume-title":"FM\u201999 - Formal Methods","author":"V. Lotz","year":"1999","unstructured":"Lotz, V., Kessler, V., Walter, G.: A Formal Security Model for Microprocessor Hardware. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 718\u2013737. Springer, Heidelberg (1999)"},{"issue":"3","key":"13_CR5","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Quarterly\u00a02(3), 219\u2013246 (1989), \n                  \n                    http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/CWI89.html","journal-title":"CWI Quarterly"},{"key":"13_CR6","unstructured":"Motre, S., Teri, C.: Using B method to formalize the Java Card runtime security policy for a Common Criteria evaluation. In: 23rd National Information Systems Security Conference (2000), \n                  \n                    http:\/\/csrc.nist.gov\/nissc\/2000\/proceedings\/toc.html"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-40981-6_4","volume-title":"Formal Aspects of Security","author":"D. Oheimb von","year":"2003","unstructured":"von Oheimb, D.: Interacting State Machines: a stateful approach to proving security. In: Abdallah, A.E., Ryan, P.Y.A., Schneider, S. (eds.) FASec 2002. LNCS, vol.\u00a02629, pp. 15\u201332. Springer, Heidelberg (2003), \n                  \n                    http:\/\/ddvo.net\/papers\/ISMs.html"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/3-540-45853-0_13","volume-title":"Computer Security - ESORICS 2002","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb, D., Lotz, V.: Formal Security Analysis with Interacting State Machines. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol.\u00a02502, pp. 212\u2013228. Springer, Heidelberg (2002), \n                  \n                    http:\/\/ddvo.net\/papers\/FSA_ISM.html\n                  \n                  \n                ; A more detailed journal version is submitted for publication"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-39893-6_10","volume-title":"Formal Methods and Software Engineering","author":"D. Oheimb von","year":"2003","unstructured":"von Oheimb, D., Lotz, V.: Generic Interacting State Machines and their instantiation with dynamic features. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 144\u2013166. Springer, Heidelberg (2003) (to appear), \n                  \n                    http:\/\/ddvo.net\/papers\/GenISMs.html"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994), \n                  \n                    http:\/\/isabelle.in.tum.de\/"},{"key":"13_CR11","unstructured":"Paulson, L.C., Nipkow, T., Wenzel, M., et al.: The Isabelle\/ HOL library, \n                  \n                    http:\/\/isabelle.in.tum.de\/library\/HOL\/"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722599_2","volume-title":"Computer Security - ESORICS 2000","author":"G. Schellhorn","year":"2000","unstructured":"Schellhorn, G., Reif, W., Schairer, A., Karger, P., Austel, V., Toll, D.: Verification of a formal security model for multiapplicative smart cards. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895. Springer, Heidelberg (2000)"},{"key":"13_CR13","unstructured":"Walter, G., Noller, J.: Infineon. SLE88CX720P \/ m1491 Security Target. Version 1.00 (March 2003), \n                  \n                    http:\/\/www.bsi.de\/???0215???"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2003"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39650-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:26:46Z","timestamp":1559507206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39650-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203001","9783540396505"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39650-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}