{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,7]],"date-time":"2024-06-07T12:04:01Z","timestamp":1717761841652},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Inf Secur"],"published-print":{"date-parts":[[2005,6]]},"DOI":"10.1007\/s10207-004-0057-5","type":"journal-article","created":{"date-parts":[[2005,1,18]],"date-time":"2005-01-18T11:46:51Z","timestamp":1106048811000},"page":"155-171","source":"Crossref","is-referenced-by-count":5,"title":["Analyzing SLE 88 memory management security using Interacting State Machines"],"prefix":"10.1007","volume":"4","author":[{"given":"David","family":"von Oheimb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Volkmar","family":"Lotz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Walter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"57_CR1","unstructured":"Atmel, Hitachi Europe, Infineon Technologies, Philips Semiconductors (2001) Smartcard IC Platform Protection Profile, version 1.0, July 2001. http:\/\/www.bsi.de\/cc\/pplist\/ssvgpp01.pdf"},{"key":"57_CR2","unstructured":"Atmel, Hitachi Europe, Infineon Technologies, Philips Semiconductors (2002) Smartcard Integrated Circuit Platform Augmentations, version 1.0, March 2002. http:\/\/www.bsi.de\/cc\/pplist\/augpp002.pdf"},{"key":"57_CR3","unstructured":"Biba KJ (1977) Integrity considerations for secure computer systems. Technical Report MTR 3153, Mitre Corporation, Bedford, MA"},{"key":"57_CR4","first-page":"mathematical","volume":"systems","author":"Bell","year":"1973","unstructured":"Bell DE, LaPadula L (1973) Secure computer systems: mathematical foundations (NTIS AD-770 768), A mathematical model (NTIS AD-771 543), A refinement of the mathematical model (NTIS AD-780 528). Technical Report MTR 2547, Mitre Corporation, Bedford, MA","journal-title":"Secure computer"},{"key":"57_CR5","unstructured":"(1999) Common Criteria for information technology security evaluation (CC), version 2.1, ISO\/IEC 15408"},{"key":"57_CR6","doi-asserted-by":"crossref","unstructured":"Clark DR, Wilson DR (1987) A comparison of commercial and military computer security policies. In: Symposium on security and privacy. IEEE Press, New York, pp 184\u2013194","DOI":"10.1109\/SP.1987.10001"},{"key":"57_CR7","doi-asserted-by":"crossref","unstructured":"Goguen JA, Meseguer J (1982) Security policies and security models. In: Symposium on security and privacy. IEEE Press, New York","DOI":"10.1109\/SP.1982.10014"},{"key":"57_CR8","doi-asserted-by":"crossref","unstructured":"Huber F, Sch\u00e4tz B, Schmidt A, Spies K (1996) Autofocus \u2013 a tool for distributed systems specification. In: Proceedings FTRTFT\u201996 \u2013 Formal techniques in real-time and fault-tolerant systems. Lecture notes in computer science, vol 1135. Springer, Berlin Heidelberg New York, pp 467\u2013470. See also http:\/\/autofocus.in.tum.de\/index-e.html","DOI":"10.1007\/3-540-61648-9_58"},{"key":"57_CR9","doi-asserted-by":"crossref","unstructured":"Kuhn T, von Oheimb D (2003) Interacting State Machines for mobility. In: Araki K, Gnesi S, Mandrioli D (eds) Proc. 12th international FME symposium (FM\u201903). Lecture notes in computer science, vol 2805. Springer, Berlin Heidelberg New York, September 2003. http:\/\/ddvo.net\/papers\/ISMfM.html","DOI":"10.1007\/978-3-540-45236-2_38"},{"key":"57_CR10","doi-asserted-by":"crossref","first-page":"702","DOI":"10.1109\/32.879809","volume":"26","author":"Lotz","year":"2000","unstructured":"Lotz V, Kessler V, Walter G (2000) A formal security model for microprocessor hardware. IEEE Trans Softw Eng 26:702\u2013712","journal-title":"IEEE Trans Softw Eng"},{"key":"57_CR11","unstructured":"Lynch N, Tuttle M (1989) An introduction to input\/output automata. CWI Q 2(3):219\u2013246. http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/CWI89.html"},{"key":"57_CR12","unstructured":"Motre S, Teri C (2000) Using B method to formalize the Java Card runtime security policy for a Common Criteria evaluation. In: 23rd national information systems security conference . http:\/\/csrc.nist.gov\/nissc\/2000\/proceedings\/toc.html"},{"key":"57_CR13","unstructured":"Nanz S (2002) Integration of CASE tools and theorem provers: a framework for system modeling and verification with AutoFocus and Isabelle. Master\u2019s thesis, TU M\u00fcnchen. http:\/\/www.doc.ic.ac.uk\/ nanz\/publications\/csthesis\/"},{"key":"57_CR14","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson L, Wenzel M (2002) Isabelle\/HOL \u2013 A proof assistant for higher-order logic. Lecture notes in computer science, vol 2283. Springer, Berlin Heidelberg New York. http:\/\/isabelle.in.tum.de\/docs.html","DOI":"10.1007\/3-540-45949-9"},{"key":"57_CR15","doi-asserted-by":"crossref","unstructured":"von Oheimb D (2002) Interacting State Machines: a stateful approach to proving security. In: Abdallah AE, Ryan P, Schneider S (eds) Formal aspects of security. Lecture notes in computer science, vol 2629. Springer, Berlin Heidelberg New York, pp 15\u201332. http:\/\/ddvo.net\/papers\/ISMs.html","DOI":"10.1007\/978-3-540-40981-6_4"},{"key":"57_CR16","doi-asserted-by":"crossref","unstructured":"von Oheimb D (2004) Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati P, Ryan P, Gollmann D, Molva R (eds) Computer Security \u2013 ESORICS 2004. Lecture notes in computer science, vol 3193. Springer, Berlin Heidelberg New York. http:\/\/ddvo.net\/papers\/Noninfluence.html","DOI":"10.1007\/978-3-540-30108-0_14"},{"key":"57_CR17","doi-asserted-by":"crossref","unstructured":"von Oheimb D, Lotz V (2002) Formal security analysis with Interacting State Machines. In: Gollmann D, Karjoth G, Waidner M (eds) Proc. 7th European symposium on research in computer security (ESORICS). Lecture notes in computer science, vol 2502. Springer, Berlin Heidelberg New York, pp 212\u2013228. http:\/\/ddvo.net\/papers\/FSA_ISM.html","DOI":"10.1007\/3-540-45853-0_13"},{"key":"57_CR18","doi-asserted-by":"crossref","unstructured":"von Oheimb D, Lotz V (2003) Generic Interacting State Machines and their instantiation with dynamic features. In: Dong JS, Woodcock J (eds) Formal methods and software engineering (ICFEM). Lecture notes in computer science, vol 2885. Springer, Berlin Heidelberg New York, November 2003, pp 144\u2013166. http:\/\/ddvo.net\/papers\/GenISMs.html","DOI":"10.1007\/978-3-540-39893-6_10"},{"key":"57_CR19","unstructured":"von Oheimb D, Nanz S (2002) ISM Homepage: documentation, sources and distribution. http:\/\/ddvo.net\/ISM\/"},{"key":"57_CR20","unstructured":"Rushby J (1992) Noninterference, transitivity, and channel-control security policies. Technical Report CS-92-02, SRI International"},{"key":"57_CR21","doi-asserted-by":"crossref","unstructured":"Schellhorn G, Reif W, Schairer A, Karger P, Austel V, Toll D (2000) Verification of a formal security model for multiapplicative smart cards. In: Cuppens F, Deswarte Y, Gollmann D, Waidner M (eds) Proc. 6th European symposium on research in computer security (ESORICS). Lecture notes in computer science, vol 1895. Springer, Berlin Heidelberg New York","DOI":"10.1007\/10722599_2"},{"key":"57_CR22","unstructured":"Walter G, Noller J (2003) Infineon Technologies SLE88CX 720P \/ Security Target. www.bsi.de\/???0215???, Version 1.00"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0057-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-004-0057-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0057-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T16:59:25Z","timestamp":1682960365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-004-0057-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["57"],"URL":"https:\/\/doi.org\/10.1007\/s10207-004-0057-5","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}