{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T07:54:02Z","timestamp":1762761242390},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,8,10]],"date-time":"2014-08-10T00:00:00Z","timestamp":1407628800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10207-014-0252-y","type":"journal-article","created":{"date-parts":[[2014,8,9]],"date-time":"2014-08-09T03:59:59Z","timestamp":1407556799000},"page":"123-140","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal modeling and automatic enforcement of Bring Your Own Device policies"],"prefix":"10.1007","volume":"14","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Costa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessio","family":"Merlo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Verderame","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,8,10]]},"reference":[{"key":"252_CR1","unstructured":"Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of the 10th Annual Network and Distributed System Security Symposium, pp. 107\u2013121 (2003)"},{"key":"252_CR2","unstructured":"Andersen, H., Lind-Nielsen, J.: MuDiv: a tool for partial model checking. In: CONCUR (1996)"},{"key":"252_CR3","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking (extended abstract). In: Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 398\u2013407. IEEE Computer Society Press (1995)","DOI":"10.1109\/LICS.1995.523274"},{"key":"252_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., Costa, G., Merlo, A.: Formal modeling and reasoning about the Android security framework. In: Proceedings of Seventh International Symposium on Trustworthy Global Computing (2012a)","DOI":"10.1007\/978-3-642-41157-1_5"},{"key":"252_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Merlo, A., Migliardi, M., Verderame, L.: Would you mind forking this process? A denial of service attack on Android (and some countermeasures). In: Proceedings of the 27th IFIP International Information Security and Privacy Conference (SEC 2012), pp. 13\u201324 (2012b)","DOI":"10.1007\/978-3-642-30436-1_2"},{"key":"252_CR6","doi-asserted-by":"crossref","unstructured":"Armando, A., Costa, G., Merlo, A.: Bring your own device, securely. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, pp. 1852\u20131858. ACM, New York, NY, USA, SAC \u201913 (2013). doi: 10.1145\/2480362.2480707","DOI":"10.1145\/2480362.2480707"},{"key":"252_CR7","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: FoSSaCS, pp. 316\u2013332 (2005)","DOI":"10.1007\/978-3-540-31982-5_20"},{"issue":"4","key":"252_CR8","doi-asserted-by":"crossref","first-page":"5","DOI":"10.5381\/jot.2009.8.4.a1","volume":"8","author":"M Bartoletti","year":"2009","unstructured":"Bartoletti, M., Costa, G., Degano, P., Martinelli, F., Zunino, R.: Securing Java with local policies. J. Object Technol. 8(4), 5\u201332 (2009)","journal-title":"J. Object Technol."},{"key":"252_CR9","unstructured":"Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.R.: Xmandroid: a new Android evolution to mitigate privilege escalation attacks. Technical Report TR-2011-04, Technische Univ. Darmstadt http:\/\/www-infsec.cs.uni-saarland.de\/bugiel\/publications\/pdfs\/XManDroid-tr-2011-04.pdf (2011)"},{"key":"252_CR10","doi-asserted-by":"crossref","unstructured":"Burguera, I., Zurutuza, U., Nadjm-Therani, S.: Crowdroid: behavior-based malware detection system for Android. In: Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM\u201911) (2011)","DOI":"10.1145\/2046614.2046619"},{"key":"252_CR11","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A.: Language-based security on Android. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, pp. 1\u20137. ACM, New York, NY, USA, PLAS \u201909 (2009)","DOI":"10.1145\/1554339.1554341"},{"key":"252_CR12","doi-asserted-by":"crossref","unstructured":"Chin, E., Felt, A.P., Greenwood, K., Wagner, D.: Analyzing inter-application communication in Android. In: Proceedings of the 9th International Conference on Mobile Systems, applications, and services, pp. 239\u2013252. ACM, New York, NY, USA, MobiSys \u201911 (2011). doi: 10.1145\/1999995.2000018","DOI":"10.1145\/1999995.2000018"},{"key":"252_CR13","unstructured":"Fuchs, A.P., Chaudhuri, A., Foster, J.S.: Scandroid: automated security certification of Android applications. Tech. rep. http:\/\/www.cs.umd.edu\/avik\/projects\/scandroidascaa\/ (2011)"},{"key":"252_CR14","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: Proceedings of the 7th Colloquium on Automata, Languages and Programming, pp. 299\u2013309. Springer, London (1980)","DOI":"10.1007\/3-540-10003-2_79"},{"key":"252_CR15","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Reading, MA (2003)","edition":"1"},{"key":"252_CR16","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. In: ACM Transactions on Programming Languages and Systems, pp. 132\u2013146 (1999)","DOI":"10.1145\/320385.320395"},{"key":"252_CR17","doi-asserted-by":"crossref","unstructured":"Janin, D., Walukiewicz, I.: (1995) Automata for the modal mu-calculus and related results. In: Wiedermann, J., H\u00e1jek, P. (eds) MFCS, Springer, Lecture Notes in Computer Science, vol. 969, pp. 552\u2013562","DOI":"10.1007\/3-540-60246-1_160"},{"issue":"2","key":"252_CR18","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977). doi: 10.1109\/TSE.1977.229904","journal-title":"IEEE Trans. Softw. Eng."},{"key":"252_CR19","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Proof system for Hennessy\u2013Milner logic with recursion. In: Dauchet, M., Nivat, M. (eds) CAAP, Springer, Lecture Notes in Computer Science, vol. 299, pp. 215\u2013230 (1988)","DOI":"10.1007\/BFb0026106"},{"key":"252_CR20","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.entcs.2006.08.029","volume":"179","author":"F Martinelli","year":"2007","unstructured":"Martinelli, F., Matteucci, I.: Through modeling to synthesis of security automata. Electron. Notes Theor. Comput. Sci. 179, 31\u201346 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"252_CR21","doi-asserted-by":"crossref","unstructured":"Nauman, M., Khan, S., Zhang, X.: Apex: extending Android permission model and enforcement with user-defined runtime constraints. In: Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, pp. 328\u2013332. ACM, New York, NY, USA, ASIACCS \u201910. (2010) doi: 10.1145\/1755688.1755732","DOI":"10.1145\/1755688.1755732"},{"key":"252_CR22","doi-asserted-by":"crossref","unstructured":"Ongtang, M., Mclaughlin, S., Enck, W., Mcdaniel, P.: Semantically rich application-centric security in Android. In: ACSAC \u201909: Annual Computer Security Applications Conference (2009)","DOI":"10.1109\/ACSAC.2009.39"},{"key":"252_CR23","unstructured":"Schlegel, R., Zhang, K., Zhou, X., Intwala, M., Kapadia, A., Wang, X.: Soundcomber: a Stealthy and Context-Aware Sound Trojan for Smartphones. In: Proceedings of the 18th Annual Network & Distributed System Security Symposium (2011)"},{"issue":"2","key":"252_CR24","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/MSP.2010.2","volume":"8","author":"A Shabtai","year":"2010","unstructured":"Shabtai, A., Fledel, Y., Kanonov, U., Elovici, Y., Dolev, S., Glezer, C.: Google Android: a comprehensive security assessment. Secur. Priv. IEEE 8(2), 35\u201344 (2010). doi: 10.1109\/MSP.2010.2","journal-title":"Secur. Priv. IEEE"},{"key":"252_CR25","doi-asserted-by":"crossref","unstructured":"Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A formal model to analyze the permission authorization and enforcement in the Android framework. In: Proceedings of the 2010 IEEE Second International Conference on Social Computing, pp. 944\u2013951. IEEE Computer Society, Washington, DC, USA, SOCIALCOM \u201910 (2010)","DOI":"10.1109\/SocialCom.2010.140"},{"key":"252_CR26","doi-asserted-by":"crossref","unstructured":"Skalka, C., Smith, S.: History effects and verification. In: Second ASIAN Symposium on Programming Languages and Systems (APLAS), pp. 107\u2013128. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"252_CR27","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/j.entcs.2005.01.027","volume":"131","author":"C Skalka","year":"2005","unstructured":"Skalka, C., Smith, S., Van Horn, D.: A Type and effect system for flexible abstract interpretation of Java. Electron. Notes Theor. Comput. Sci. 131, 111\u2013124 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"252_CR28","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"RS Streett","year":"1989","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput. 81(3), 249\u2013264 (1989)","journal-title":"Inf. Comput."},{"key":"252_CR29","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Zhang, X., Jiang, X., Freeh, V.W.: Taming information-stealing smartphone applications (on Android). In: Proceedings of the 4th International Conference on Trust and Trustworthy Computing, TRUST\u201911, pp. 93\u2013107 (2011)","DOI":"10.1007\/978-3-642-21599-5_7"},{"key":"252_CR30","unstructured":"Zhou, Y., Wang, Z., Zhou, W., Jiang, X.: Hey, You, Get Off of My Market: detecting malicious apps in official and alternative android markets. In: Proceedings of the 19th Annual Network & Distributed System Security Symposium (2012)"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-014-0252-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-014-0252-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-014-0252-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T14:53:50Z","timestamp":1565708030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-014-0252-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,10]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["252"],"URL":"https:\/\/doi.org\/10.1007\/s10207-014-0252-y","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,10]]}}}