{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:22:15Z","timestamp":1742948535602,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319571850"},{"type":"electronic","value":"9783319571867"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-57186-7_52","type":"book-chapter","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T11:29:15Z","timestamp":1491996555000},"page":"725-735","source":"Crossref","is-referenced-by-count":0,"title":["BYODCert: Toward a Cross-Organizational BYOD Paradigm"],"prefix":"10.1007","author":[{"given":"Alessio","family":"Merlo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,13]]},"reference":[{"issue":"1","key":"52_CR1","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1109\/COMST.2014.2350994","volume":"17","author":"W Mazurczyk","year":"2015","unstructured":"Mazurczyk, W., Caviglione, L.: Steganography in modern smartphones, mitigation techniques. IEEE Commun. Surv. Tutor. 17(1), 334\u2013357 (2015). Firstquarter","journal-title":"IEEE Commun. Surv. Tutor."},{"issue":"1","key":"52_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.scico.2008.09.004","volume":"74","author":"I Aktug","year":"2008","unstructured":"Aktug, I., Naliuka, K.: Conspec: a formal language for policy specification. Sci. Comput. Program. 74(1), 2\u201312 (2008)","journal-title":"Sci. Comput. Program."},{"key":"52_CR3","unstructured":"Ibm byod solution. \nhttp:\/\/www.ibm.com\/mobile\/bring-your-own-device\/\n\n. Accessed 7 Mar 2017"},{"key":"52_CR4","unstructured":"Blackberry byod solution. \nhttp:\/\/us.blackberry.com\/bring-your-own-device\n\n. Accessed 7 Mar 2017"},{"key":"52_CR5","unstructured":"Appthority. \nhttps:\/\/www.appthority.com\n\n. Accessed 7 Mar 2017"},{"key":"52_CR6","unstructured":"Huawei byod solution. \nhttp:\/\/enterprise.huawei.com\/topic\/byod_en\/\n\n. Accessed 7 Mar 2017"},{"issue":"3","key":"52_CR7","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"52_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"52_CR9","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"5","key":"52_CR10","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.entcs.2009.11.021","volume":"253","author":"L Desmet","year":"2009","unstructured":"Desmet, L., Joosen, W., Massacci, F., Naliuka, K., Philippaerts, P., Piessens, F., Vanoverberghe, D.: The s3ms.net run time monitor. Electron. Notes Theor. Comput. Sci. 253(5), 153\u2013159 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"52_CR11","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.pmcj.2015.05.005","volume":"24","author":"A Merlo","year":"2015","unstructured":"Merlo, A., Migliardi, M., Caviglione, L.: A survey on energy-aware security mechanisms. Pervasive Mob. Comput. 24, 77\u201390 (2015). Cited by 7","journal-title":"Pervasive Mob. Comput."},{"issue":"5","key":"52_CR12","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1016\/j.jlap.2009.02.013","volume":"78","author":"N Bielova","year":"2009","unstructured":"Bielova, N., Dragoni, N., Massacci, F., Naliuka, K., Siahaan, I.: Matching in security-by-contract for mobile code. J. Log. Algebr. Program. 78(5), 340\u2013358 (2009). The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS07)","journal-title":"J. Log. Algebr. Program."},{"key":"52_CR13","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, SAC 2013, pp. 1852\u20131858. ACM, New York (2013)","DOI":"10.1145\/2480362.2480707"},{"issue":"6","key":"52_CR14","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/MC.2014.164","volume":"47","author":"A Armando","year":"2014","unstructured":"Armando, A., Costa, G., Verderame, L., Merlo, A.: Securing the bring your own device paradigm. Computer 47(6), 48\u201356 (2014)","journal-title":"Computer"},{"key":"52_CR15","doi-asserted-by":"crossref","unstructured":"Armando, A., Costa, G., Merlo, A., Verderame, L.: Enabling BYOD through secure meta-market. In: Proceedings of the ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec 2014, pp. 219\u2013230. ACM, New York (2014)","DOI":"10.1145\/2627393.2627410"},{"key":"52_CR16","doi-asserted-by":"crossref","unstructured":"Costa, G., Merlo, A., Verderame, L., Armando, A.: Automatic security verification of mobile app configurations. Future Gener. Comput. Syst. (2016). \nhttp:\/\/dx.doi.org\/10.1016\/j.future.2016.06.014","DOI":"10.1016\/j.future.2016.06.014"},{"key":"52_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-35632-2_11","volume-title":"Runtime Verification","author":"Y Falcone","year":"2013","unstructured":"Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for android applications with RV-Droid. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 88\u201395. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-35632-2_11"},{"issue":"2","key":"52_CR18","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1016\/j.future.2012.08.001","volume":"29","author":"A Merlo","year":"2013","unstructured":"Merlo, A.: Secure cooperative access control on grid. Future Gener. Comput. Syst. 29(2), 497\u2013508 (2013). Special section: recent advances in e-Science","journal-title":"Future Gener. Comput. Syst."},{"key":"52_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-31982-5_20","volume-title":"Foundations of Software Science and Computational Structures","author":"M Bartoletti","year":"2005","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 316\u2013332. Springer, Heidelberg (2005). doi:\n10.1007\/978-3-540-31982-5_20"},{"key":"52_CR20","volume-title":"Spin Model Checker, the: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin Model Checker, the: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)","edition":"1"},{"key":"52_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-36742-7_15"},{"key":"52_CR22","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking. In: Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 398\u2013407, June 1995","DOI":"10.1109\/LICS.1995.523274"},{"key":"52_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"CJF Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The Scyther Tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414\u2013418. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-70545-1_38"},{"key":"52_CR24","doi-asserted-by":"crossref","unstructured":"Caviglione, L.: Can satellites face trends? the case of web 2.0. In: International Workshop on Satellite and Space Communications, pp. 446\u2013450, September 2009","DOI":"10.1109\/IWSSC.2009.5286305"}],"container-title":["Lecture Notes in Computer Science","Green, Pervasive, and Cloud Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57186-7_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T23:54:47Z","timestamp":1517529287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57186-7_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319571850","9783319571867"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57186-7_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}