{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:43:31Z","timestamp":1759092211420},"reference-count":68,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,5,10]],"date-time":"2013-05-10T00:00:00Z","timestamp":1368144000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10703-013-0187-3","type":"journal-article","created":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T06:57:46Z","timestamp":1368082666000},"page":"450-492","source":"Crossref","is-referenced-by-count":18,"title":["Verification and enforcement of access control policies"],"prefix":"10.1007","volume":"43","author":[{"given":"Antonio","family":"Cau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helge","family":"Janicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ben","family":"Moszkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,5,10]]},"reference":[{"key":"187_CR1","first-page":"1","volume-title":"10th annual network and distributed system symposium (NDSS\u201903)","author":"M Abadi","year":"2003","unstructured":"Abadi M, Fournet C (2003) Access control based on execution history. In: 10th annual network and distributed system symposium (NDSS\u201903). The Internet Society, Reston, pp 1\u201315"},{"issue":"2","key":"187_CR2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"VM Antimirov","year":"1996","unstructured":"Antimirov VM (1996) Partial derivatives of regular expressions and finite automaton constructions. Theor Comput Sci 155(2):291\u2013319. doi: 10.1016\/0304-3975(95)00182-4","journal-title":"Theor Comput Sci"},{"key":"187_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/DYSPAN.2010.5457867","volume-title":"2010 IEEE symposium on new frontiers in dynamic spectrum","author":"B Bahrak","year":"2010","unstructured":"Bahrak B, Deshpande A, Whitaker M, Park JM (2010) Bresap: a policy reasoner for processing spectrum access policies represented by binary decision diagrams. In: 2010 IEEE symposium on new frontiers in dynamic spectrum, pp 1\u201312. doi: 10.1109\/DYSPAN.2010.5457867"},{"key":"187_CR4","volume-title":"Handbook of network and system administration","author":"AK Bandara","year":"2007","unstructured":"Bandara AK, Lupu EC, Sloman M (2007) Policy-based management. In: Burgess M, Bergstra J (eds) Handbook of network and system administration. Elsevier, Amsterdam"},{"issue":"3","key":"187_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/501978.501979","volume":"4","author":"E Bertino","year":"2001","unstructured":"Bertino E, Bonatti PA, Ferrari E (2001) TRBAC: a temporal role-based access control model. ACM Trans Inf Syst Secur 4(3):191\u2013233. doi: 10.1145\/501978.501979","journal-title":"ACM Trans Inf Syst Secur"},{"issue":"8","key":"187_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691. doi: 10.1109\/TC.1986.1676819","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"187_CR7","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u2013318. doi: 10.1145\/136035.136043","journal-title":"ACM Comput Surv"},{"key":"187_CR8","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski JA (1964) Derivatives of regular expressions. J ACM 11:481\u2013494. doi: 10.1145\/321239.321249","journal-title":"J ACM"},{"issue":"2","key":"187_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170. doi: 10.1016\/0890-5401(92)90017-A","journal-title":"Inf Comput"},{"issue":"5","key":"187_CR10","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Chaochen Z, Hoare CAR, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269\u2013276. doi: 10.1016\/0020-0190(91)90122-X","journal-title":"Inf Process Lett"},{"key":"187_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"CAV","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) CAV. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 359\u2013364"},{"issue":"10","key":"187_CR12","doi-asserted-by":"crossref","first-page":"1737","DOI":"10.1109\/TCAD.2008.2003303","volume":"27","author":"A Cimatti","year":"2008","unstructured":"Cimatti A, Roveri M, Tonetta S (2008) Symbolic compilation of PSL. IEEE Trans Comput-Aided Des Integr Circuits Syst 27(10):1737\u20131750. doi: 10.1109\/TCAD.2008.2003303","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"187_CR13","volume-title":"Model checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke EM Jr, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"187_CR14","first-page":"111","volume-title":"Proceedings of the IFIP international workshop on applied formal methods for correct VLSI design","author":"O Coudert","year":"1989","unstructured":"Coudert O, Berthet C, Madre JC (1989) Verification of sequential machines using boolean functional vectors. In: Claesen L (ed) Proceedings of the IFIP international workshop on applied formal methods for correct VLSI design, Leuven, Belgium, pp 111\u2013128"},{"key":"187_CR15","series-title":"LNCS","first-page":"365","volume-title":"Automatic verification methods for finite state systems, international workshop","author":"O Coudert","year":"1989","unstructured":"Coudert O, Berthet C, Madre JC (1989) Verification of synchronous sequential machines based on symbolic execution. In: Sifakis J (ed) Automatic verification methods for finite state systems, international workshop, Grenoble, France. LNCS, vol 407. Springer, Berlin, pp 365\u2013373"},{"key":"187_CR16","first-page":"126","volume-title":"Proceedings of the IEEE international conference on computer aided design","author":"O Coudert","year":"1990","unstructured":"Coudert O, Berthet C, Madre JC (1990) A unified framework for the formal verification of sequential circuits. In: Proceedings of the IEEE international conference on computer aided design, pp 126\u2013129"},{"key":"187_CR17","volume-title":"Workshop on policies for distributed systems and networks (Policy2001)","author":"N Damianou","year":"2001","unstructured":"Damianou N, Dulay N, Lupu E, Sloman M (2001) The Ponder specification language. In: Workshop on policies for distributed systems and networks (Policy2001)"},{"key":"187_CR18","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan Z, Tian C, Zhang L (2008) A decision procedure for propositional projection temporal logic with infinite models. Acta Inform 45:43\u201378. doi: 10.1007\/s00236-007-0062-z","journal-title":"Acta Inform"},{"key":"187_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Proceedings of the 10th international conference on computer-aided verification, CAV \u201998","author":"J Elgaard","year":"1998","unstructured":"Elgaard J, Klarlund N, M\u00f8ller A (1998) MONA 1.x: new techniques for WS1S and WS2S. In: Proceedings of the 10th international conference on computer-aided verification, CAV \u201998. LNCS, vol 1427. Springer, Berlin, pp 516\u2013520"},{"issue":"1","key":"187_CR20","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Log 2(1):12\u201356. doi: 10.1145\/371282.371311","journal-title":"ACM Trans Comput Log"},{"issue":"1\u20132","key":"187_CR21","doi-asserted-by":"crossref","first-page":"105","DOI":"10.3166\/jancl.14.105-148","volume":"14","author":"R Gomez","year":"2004","unstructured":"Gomez R, Bowman H (2004) PITL2MONA: implementing a decision procedure for propositional interval temporal logic. J Appl Non-Class Log 14(1\u20132):105\u2013148. Issue on Interval temporal logics and duration calculi. V Goranko and A Montanari guest eds","journal-title":"J Appl Non-Class Log"},{"issue":"3","key":"187_CR22","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231\u2013274. doi: 10.1016\/0167-6423(87)90035-9","journal-title":"Sci Comput Program"},{"key":"187_CR23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D Harel","year":"2000","unstructured":"Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press, Cambridge"},{"issue":"5","key":"187_CR24","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"187_CR25","series-title":"SACMAT \u201911","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1145\/1998441.1998472","volume-title":"Proceedings of the 16th ACM symposium on access control models and technologies","author":"H Hu","year":"2011","unstructured":"Hu H, Ahn GJ, Kulkarni K (2011) Anomaly discovery and resolution in web access control policies. In: Proceedings of the 16th ACM symposium on access control models and technologies. SACMAT \u201911. ACM, New York, pp 165\u2013174. doi: 10.1145\/1998441.1998472"},{"key":"187_CR26","unstructured":"IBM Cooperation (2003) Enterprise privacy authorisation language (EPAL) version 1.2. Submitted to the W3C. http:\/\/www.w3.org\/Submission4\/2003\/SUBM-EPAL-20031110\/"},{"key":"187_CR27","doi-asserted-by":"crossref","unstructured":"IEEE (2005) IEEE standard for property specification language (PSL), std 1850-2005. Tech rep, IEEE. doi: 10.1109\/IEEESTD.2005.97780","DOI":"10.1109\/IEEESTD.2005.97780"},{"key":"187_CR28","unstructured":"ISO\/IEC (2006) ISO\/IEC 10181-3:1996 information technology\u2014open systems interconnection\u2014security frameworks for open systems: access control framework. http:\/\/www.iso.org\/iso\/en\/CatalogueDetailPage.CatalogueDetail?CSNUMBER=18199"},{"issue":"2","key":"187_CR29","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1145\/383891.383894","volume":"26","author":"S Jajodia","year":"2001","unstructured":"Jajodia S, Samarati P, Sapino ML, Subrahmanian VS (2001) Flexible support for multiple access control policies. ACM Trans Database Syst 26(2):214\u2013260. doi: 10.1145\/383891.383894","journal-title":"ACM Trans Database Syst"},{"key":"187_CR30","first-page":"173","volume-title":"Proceedings of POLICY2006","author":"H Janicke","year":"2006","unstructured":"Janicke H, Cau A, Siewe F, Zedan H, Jones K (2006) A compositional event & time-based policy model. In: Proceedings of POLICY2006, London, Ontario, Canada. IEEE Computer Society, London, pp 173\u2013182"},{"key":"187_CR31","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/POLICY.2007.15","volume-title":"Proceedings of the 8th IEEE international workshop on policies for distributed systems (POLICY2007)","author":"H Janicke","year":"2007","unstructured":"Janicke H, Cau A, Siewe F, Zedan H (2007) Deriving enforcement mechanisms from policies. In: Proceedings of the 8th IEEE international workshop on policies for distributed systems (POLICY2007), pp 161\u2013170"},{"key":"187_CR32","author":"H Janicke","year":"2012","unstructured":"Janicke H, Cau A, Siewe F, Zedan H (2012) Dynamic access control policies: specification and verification. Comput J. doi: 10.1093\/comjnl\/bxs102","journal-title":"Comput J"},{"issue":"2","key":"187_CR33","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TDSC.2005.18","volume":"2","author":"J Joshi","year":"2005","unstructured":"Joshi J, Bertino E, Ghafoor A (2005) An analysis of expressiveness and design issues for the generalized temporal role-based access control model. IEEE Trans Dependable Secure Comput 2(2):157\u2013175. doi: 10.1109\/TDSC.2005.18","journal-title":"IEEE Trans Dependable Secure Comput"},{"issue":"1","key":"187_CR34","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/TKDE.2005.1","volume":"17","author":"J Joshi","year":"2005","unstructured":"Joshi J, Bertino E, Latif U, Ghafoor A (2005) A generalized temporal role-based access control model. IEEE Trans Knowl Data Eng 17(1):4\u201323. doi: 10.1109\/TKDE.2005.1","journal-title":"IEEE Trans Knowl Data Eng"},{"key":"187_CR35","unstructured":"Klarlund N, M\u00f8ller A (2001) MONA version 1.4 user manual. Notes series NS-01-1, BRICS, Department of Computer Science, Aarhus University. Available from http:\/\/www.brics.dk\/mona\/ . Revision of BRICS NS-98-3"},{"key":"187_CR36","doi-asserted-by":"crossref","unstructured":"Kolovski V (2008) Logic-based framework for web access control policies. PhD thesis, Computer Science Department of University of Maryland, College Park","DOI":"10.1145\/1242572.1242664"},{"key":"187_CR37","series-title":"Lecture notes in artificial intelligence","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/3-540-58976-7_3","volume-title":"Executable modal and temporal logics","author":"S Kono","year":"1995","unstructured":"Kono S (1995) A combination of clausal and non-clausal temporal logic programs. In: Fisher M, Owens R (eds) Executable modal and temporal logics. Lecture notes in artificial intelligence, Cambery, France, vol 897. Springer, Berlin, pp 40\u201357"},{"key":"187_CR38","unstructured":"Kozen D (1992) Private commuication"},{"key":"187_CR39","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03809-3","volume-title":"Introduction to formal hardware verification: methods and tools for designing correct circuits and systems","author":"T Kropf","year":"1999","unstructured":"Kropf T (1999) Introduction to formal hardware verification: methods and tools for designing correct circuits and systems, 1st edn. Springer, New York","edition":"1"},{"issue":"3","key":"187_CR40","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872\u2013923. doi: 10.1145\/177492.177726","journal-title":"ACM Trans Program Lang Syst"},{"issue":"1","key":"187_CR41","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/775265.775268","volume":"8","author":"BW Lampson","year":"1974","unstructured":"Lampson BW (1974) Protection. Oper Syst Rev 8(1):18\u201324. doi: 10.1145\/775265.775268","journal-title":"Oper Syst Rev"},{"key":"187_CR42","first-page":"3","volume-title":"TIME","author":"M Leucker","year":"2010","unstructured":"Leucker M, S\u00e1nchez C (2010) Regular linear-time temporal logic. In: Markey N, Wijsen J (eds) TIME. IEEE Computer Society, Los Alamitos, pp 3\u20135. doi: 10.1109\/TIME.2010.29"},{"issue":"6","key":"187_CR43","doi-asserted-by":"crossref","first-page":"852","DOI":"10.1109\/32.824414","volume":"25","author":"EC Lupu","year":"1999","unstructured":"Lupu EC, Sloman M (1999) Conflicts in policy-based distributed systems management. IEEE Trans Softw Eng 25(6):852\u2013869. doi: 10.1109\/32.824414","journal-title":"IEEE Trans Softw Eng"},{"key":"187_CR44","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems: specification","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, New York"},{"issue":"2","key":"187_CR45","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1109\/TDSC.2008.41","volume":"7","author":"A Masood","year":"2010","unstructured":"Masood A, Ghafoor A, Mathur AP (2010) Conformance testing of temporal role-based access control systems. IEEE Trans Dependable Secure Comput 7(2):144\u2013158. doi: 10.1109\/TDSC.2008.41","journal-title":"IEEE Trans Dependable Secure Comput"},{"key":"187_CR46","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic, Norwell"},{"key":"187_CR47","unstructured":"Moszkowski B (1983) Reasoning about digital circuits. PhD thesis, Department of Computer Science, Stanford University, technical report STAN-CS-83-970"},{"issue":"2","key":"187_CR48","first-page":"10","volume":"18","author":"B Moszkowski","year":"1985","unstructured":"Moszkowski B (1985) A temporal logic for multilevel reasoning about hardware. IEEE Trans Comput 18(2):10\u201319","journal-title":"IEEE Trans Comput"},{"issue":"1\u20132","key":"187_CR49","doi-asserted-by":"crossref","first-page":"55","DOI":"10.3166\/jancl.14.55-104","volume":"14","author":"B Moszkowski","year":"2004","unstructured":"Moszkowski B (2004) A hierarchical completeness proof for propositional interval temporal logic with finite time. J Appl Non-Class Log 14(1\u20132):55\u2013104. Special issue on Interval temporal logics and duration calculi","journal-title":"J Appl Non-Class Log"},{"key":"187_CR50","first-page":"371","volume-title":"We will show them: essays in honour of Dov Gabbay","author":"B Moszkowski","year":"2005","unstructured":"Moszkowski B (2005) A hierarchical analysis of propositional temporal logic based on intervals. In: Artemov S, Barringer H, d\u2019Avila Garcez AS, Lamb LC, Woods J (eds) We will show them: essays in honour of Dov Gabbay, vol 2. King\u2019s College, London, pp 371\u2013440"},{"key":"187_CR51","first-page":"107","volume-title":"International syposium on temporal representation and reasoning","author":"B Moszkowski","year":"2011","unstructured":"Moszkowski B (2011) Compositional reasoning using intervals and time reversal. In: International syposium on temporal representation and reasoning, pp\u00a0107\u2013114. doi: 10.1109\/TIME.2011.25"},{"key":"187_CR52","unstructured":"OASIS (2005) eXtensible access control markup language (XACML) version 2.0. http:\/\/www.oasis-open.org\/committees\/tc_home.php?wg_abbrev=xacml#XACML20"},{"key":"187_CR53","volume-title":"Proceedings of workshop on real-time tools (RT-TOOL\u20192001)","author":"PK Pandya","year":"2001","unstructured":"Pandya PK (2001) Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. In: Pattersson P, Yovine S (eds) Proceedings of workshop on real-time tools (RT-TOOL\u20192001). Affiliated with CONCUR 2001, Uppsala University, Sweden, technical report 2001-14, full version available as technical report TCS-00-PKP-1, Tata Institute of Fundamental Research, 2000"},{"issue":"1","key":"187_CR54","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/984334.984339","volume":"7","author":"J Park","year":"2004","unstructured":"Park J, Sandhu RS (2004) The UCON ABC usage control model. ACM Trans Inf Syst Secur 7(1):128\u2013174. doi: 10.1145\/984334.984339","journal-title":"ACM Trans Inf Syst Secur"},{"key":"187_CR55","first-page":"15","volume-title":"Proceedings of IFIP TC11\/WG 11.3 eighteenth annual conference on data and applications security","author":"J Park","year":"2004","unstructured":"Park J, Zhang X, Sandhu RS (2004) Attribute mutability in usage control. In: Farkas C, Samarati P (eds) Proceedings of IFIP TC11\/WG 11.3 eighteenth annual conference on data and applications security, Sitges, Catalonia, Spain. Kluwer, Dordrecht, pp 15\u201329"},{"key":"187_CR56","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, present and future","author":"AN Prior","year":"1967","unstructured":"Prior AN (1967) Past, present and future. Oxford University Press, Oxford"},{"key":"187_CR57","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/1542207.1542218","volume-title":"Proceedings of the 14th ACM symposium on access control models and technologies, SACMAT \u201909","author":"P Rao","year":"2009","unstructured":"Rao P, Lin D, Bertino E, Li N, Lobo J (2009) An algebra for fine-grained integration of xacml policies. In: Proceedings of the 14th ACM symposium on access control models and technologies, SACMAT \u201909. ACM, New York, pp 63\u201372. doi: 10.1145\/1542207.1542218"},{"key":"187_CR58","volume-title":"Proceeding of the second international workshop on mathematical method, models and architectures for computer networks security","author":"R Sandhu","year":"2003","unstructured":"Sandhu R, Park J (2003) The UCON ABC usage control model. In: Proceeding of the second international workshop on mathematical method, models and architectures for computer networks security"},{"key":"187_CR59","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1145\/1133058.1133079","volume-title":"SACMAT","author":"A Schaad","year":"2006","unstructured":"Schaad A, Lotz V, Sohr K (2006) A model-checking approach to analysing organisational controls in a loan origination process. In: Ferraiolo DF, Ray I (eds) SACMAT. ACM, New York, pp 139\u2013149. doi: 10.1145\/1133058.1133079"},{"issue":"1","key":"187_CR60","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider FB (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30\u201350. doi: 10.1145\/353323.353382","journal-title":"ACM Trans Inf Syst Secur"},{"key":"187_CR61","volume-title":"Proceedings of the ACM workshop on formal methods in security engineering: from specifications to code","author":"F Siewe","year":"2003","unstructured":"Siewe F, Cau A, Zedan H (2003) A compositional framework for access control policies enforcement. In: Proceedings of the ACM workshop on formal methods in security engineering: from specifications to code"},{"key":"187_CR62","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF02283186","volume":"2","author":"M Sloman","year":"1994","unstructured":"Sloman M (1994) Policy driven management for distributed systems. J Netw Syst Manag 2:333\u2013360","journal-title":"J Netw Syst Manag"},{"key":"187_CR63","unstructured":"Somenzi F (1998) CUDD: Colorado University decision diagram package. University of Colorado at Boulder. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"issue":"3","key":"187_CR64","first-page":"107","volume":"2(2","author":"TYC Woo","year":"1993","unstructured":"Woo TYC, Lam SS (1993) Authorization in distributed systems: a new approach. J Comput Secur 2(2(3):107\u2013136","journal-title":"J Comput Secur"},{"key":"187_CR65","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/990036.990038","volume-title":"SACMAT \u201904: proceedings of the ninth ACM symposium on access control models and technologies","author":"X Zhang","year":"2004","unstructured":"Zhang X, Park J, Parisi-Presicce F, Sandhu R (2004) A logical specification for usage control. In: SACMAT \u201904: proceedings of the ninth ACM symposium on access control models and technologies. ACM, New York, pp 1\u201310. doi: 10.1145\/990036.990038"},{"issue":"4","key":"187_CR66","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/1108906.1108908","volume":"8","author":"X Zhang","year":"2005","unstructured":"Zhang X, Parisi-Presicce F, Sandhu RS, Park J (2005) Formal model and policy specification of usage control. ACM Trans Inf Syst Secur 8(4):351\u2013387. doi: 10.1145\/1108906.1108908","journal-title":"ACM Trans Inf Syst Secur"},{"key":"187_CR67","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1145\/1128817.1128853","volume-title":"ASIACCS","author":"X Zhang","year":"2006","unstructured":"Zhang X, Sandhu RS, Parisi-Presicce F (2006) Safety analysis of usage control authorization models. In: Lin FC, Lee DT, Lin BS, Shieh S, Jajodia S (eds) ASIACCS. ACM, New York, pp 243\u2013254. doi: 10.1145\/1128817.1128853"},{"key":"187_CR68","first-page":"10","volume-title":"SUTC","author":"X Zhang","year":"2008","unstructured":"Zhang X, Seifert JP, Sandhu RS (2008) Security enforcement model for distributed usage control. In: Singhal M, Serugendo GDM, Tsai JJP, Lee W, R\u00f6mer K, Tseng YC, Hsiao HCW (eds) SUTC. IEEE Computer Society, Los Alamitos, pp\u00a010\u201318. doi: 10.1109\/SUTC.2008.79"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0187-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0187-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0187-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T15:45:57Z","timestamp":1563032757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0187-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,10]]},"references-count":68,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["187"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0187-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,10]]}}}