{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:49:15Z","timestamp":1725533355420},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642024436"},{"type":"electronic","value":"9783642024443"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02444-3_4","type":"book-chapter","created":{"date-parts":[[2009,6,6]],"date-time":"2009-06-06T09:15:35Z","timestamp":1244279735000},"page":"49-63","source":"Crossref","is-referenced-by-count":0,"title":["A Framework for the Analysis of Access Control Models for Interactive Mobile Devices"],"prefix":"10.1007","author":[{"given":"Juan Manuel","family":"Crespo","sequence":"first","affiliation":[]},{"given":"Gustavo","family":"Betarte","sequence":"additional","affiliation":[]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.-L.: Static analysis for stack inspection. Design and Implementation of Programming Languages\u00a054 (2001)","DOI":"10.1016\/S1571-0661(04)00236-1"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11863908_8","volume-title":"Computer Security \u2013 ESORICS 2006","author":"F. Besson","year":"2006","unstructured":"Besson, F., Dufay, G., Jensen, T.: A formal model of access control for mobile interactive devices. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 110\u2013126. Springer, Heidelberg (2006)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3233\/JCS-2001-9303","volume":"9","author":"F. Besson","year":"2001","unstructured":"Besson, F., Jensen, T., Le M\u00e9tayer, D., Thorn, T.: Model ckecking security properties of control flow graphs. Journal of Computer Security\u00a09, 217\u2013250 (2001)","journal-title":"Journal of Computer Security"},{"key":"4_CR4","first-page":"95","volume-title":"Information and Computation","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. In: Information and Computation, vol.\u00a076, pp. 95\u2013120. Academic Press, London (1988)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"4_CR6","unstructured":"JSR 118\u00a0Expert Group. Mobile information device profile for java 2 micro edition. version 2.0. Technical report, Sun Microsystems, Inc. and Motorola, Inc. (2002)"},{"key":"4_CR7","unstructured":"JSR 37\u00a0Expert Group. Mobile information device profile for java 2 micro edition. version 1.0. Technical report, Sun Microsystems, Inc. (2000)"},{"key":"4_CR8","first-page":"89","volume-title":"Proc. of the 20th IEEE Symp. on Security and Privacy","author":"T. Jensen","year":"1999","unstructured":"Jensen, T., Le M\u00e9tayer, D., Thorn, T.: Verification of control flow based security properties. In: Proc. of the 20th IEEE Symp. on Security and Privacy, pp. 89\u2013103. IEEE Computer Society, New York (1999)"},{"key":"4_CR9","volume-title":"I Chilean Workshop on Formal Methods","author":"R. Roushani","year":"2008","unstructured":"Roushani, R., Betarte, G., Luna, C.: A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices. In: I Chilean Workshop on Formal Methods, Punta Arenas, Chile. IEEE Computer Society, Los Alamitos (2008) (to be published)"},{"key":"4_CR10","unstructured":"Sun Microsystems, Inc. Java Platform Micro Edition (last accessed October 2008), http:\/\/java.sun.com\/javame\/index.jsp"},{"key":"4_CR11","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.1 (2006)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-75227-1_15","volume-title":"Formal Aspects in Security and Trust","author":"S. Zanella B\u00e9guelin","year":"2007","unstructured":"Zanella B\u00e9guelin, S., Betarte, G., Luna, C.: A formal specification of the MIDP 2.0 security model. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol.\u00a04691, pp. 220\u2013234. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02444-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T18:46:33Z","timestamp":1558377993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02444-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642024436","9783642024443"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02444-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}