{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:43:11Z","timestamp":1759092191291},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"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":[[2014,4]]},"DOI":"10.1007\/s10207-013-0205-x","type":"journal-article","created":{"date-parts":[[2013,7,16]],"date-time":"2013-07-16T03:26:49Z","timestamp":1373945209000},"page":"97-111","source":"Crossref","is-referenced-by-count":28,"title":["Security policy verification for multi-domains in cloud systems"],"prefix":"10.1007","volume":"13","author":[{"given":"Antonios","family":"Gouglidis","sequence":"first","affiliation":[]},{"given":"Ioannis","family":"Mavridis","sequence":"additional","affiliation":[]},{"given":"Vincent C.","family":"Hu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,7,17]]},"reference":[{"issue":"6","key":"205_CR1","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/MSP.2010.194","volume":"8","author":"J Alcaraz Calero","year":"2010","unstructured":"Alcaraz Calero, J., Edwards, N., Kirschnick, J., Wilcock, L., Wray, M.: Toward a multi-tenancy authorization system for cloud services. IEEE Secur. Priv. 8(6), 48\u201355 (2010)","journal-title":"IEEE Secur. Priv."},{"key":"205_CR2","unstructured":"Alloy. A language and tool for relational models, http:\/\/alloy.mit.edu\/alloy\/"},{"key":"205_CR3","unstructured":"ANSI. ANSI INCITS 359\u20132004, role based access control, (2004)"},{"key":"205_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., Ranise, S.: Automated symbolic analysis of arbac-policies (extended version). arXiv, preprint arXiv:1012.5590, (2010)","DOI":"10.1007\/978-3-642-22444-7_2"},{"key":"205_CR5","doi-asserted-by":"crossref","unstructured":"Bacon, J., Evans, D., Eyers, D.M., Migliavacca, M., Pietzuch, P., Shand, B.: Enforcing end-to-end application security in the cloud (big ideas paper). In: Proceedings of the ACM\/IFIP\/USENIX 11th International Conference on Middleware, pp. 293\u2013312. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16955-7_15"},{"key":"205_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"205_CR7","doi-asserted-by":"crossref","unstructured":"Boost. Boost c++ libraries, http:\/\/www.boost.org\/ , 2011","DOI":"10.1002\/wilm.10057"},{"key":"205_CR8","doi-asserted-by":"crossref","unstructured":"Bryans, J.W., Fitzgerald, J.S.: Formal Engineering of XACML Access Control Policies in VDM++. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-76650-6_4"},{"key":"205_CR9","doi-asserted-by":"crossref","unstructured":"Capitani di Vimercati, S., Foresti, S., Samarati, P.: Authorization and access control. In: Petkovic, M., Jonker, W. (eds.) Security, Privacy, and Trust in Modern Data Management, Data-Centric Systems and Applications, pp. 39\u201353. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69861-6_4"},{"key":"205_CR10","unstructured":"CITRIX. Available role based access control permissions for xenserver, http:\/\/support.citrix.com\/article\/ctx126441 , (2013)"},{"key":"205_CR11","doi-asserted-by":"crossref","unstructured":"Crampton, J., Loizou, G.: Administrative scope and role hierarchy operations. In: In Proceedings of Seventh ACM Symposium on Access Control Models and Technologies (SACMAT 2002), pp. 145\u2013154, (2002)","DOI":"10.1145\/507711.507736"},{"key":"205_CR12","unstructured":"Ferraiolo, D.F., Kuhn, D.R., Chandramouli, R.: Role-Based Access Control. Artech House, Inc., (2003)"},{"key":"205_CR13","doi-asserted-by":"crossref","unstructured":"Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, ICSE \u201905, pp. 196\u2013205. ACM, New York (2005)","DOI":"10.1145\/1062455.1062502"},{"key":"205_CR14","unstructured":"Foster, I., Yong, Z., Raicu, I., Lu, S.: Cloud computing and grid computing 360-degree compared. In: Grid Computing Environments Workshop, 2008. GCE \u201908, pp. 1\u201310, (2008)"},{"key":"205_CR15","unstructured":"Gong, L., Qian, X.: Computational issues in secure interoperation, (1996)"},{"issue":"4","key":"205_CR16","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1016\/j.cose.2012.01.010","volume":"31","author":"A Gouglidis","year":"2012","unstructured":"Gouglidis, A., Mavridis, I.: domRBAC: An access control model for modern collaborative systems. Comput. Secur. 31(4), 540\u2013556 (2012)","journal-title":"Comput. Secur."},{"key":"205_CR17","doi-asserted-by":"crossref","unstructured":"Hansen, F., Oleshchuk, V.: Conformance checking of RBAC policy and its implementation. In: Deng, R., Bao, F., Pang, H., Zhou, J. (eds.) Information Security Practice and Experience, volume 3439 of Lecture Notes in Computer Science, pp. 144\u2013155. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31979-5_13"},{"key":"205_CR18","doi-asserted-by":"crossref","unstructured":"Hu, H., Ahn, G.: Enabling verification and conformance testing for access control model. In: Proceedings of the 13th ACM Symposium on Access Control Models and Technologies, SACMAT \u201908, pp. 195\u2013204. ACM, New York (2008)","DOI":"10.1145\/1377836.1377867"},{"key":"205_CR19","doi-asserted-by":"crossref","unstructured":"Hu, V.C., Kuhn, D.R., Xie, T.: Property verification for generic access control models. In: Proceedings of the 2008 IEEE\/IFIP International Conference on Embedded and Ubiquitous Computing, vol. 02, EUC \u201908, pp. 243\u2013250. IEEE Computer Society, Washington, DC (2008)","DOI":"10.1109\/EUC.2008.22"},{"issue":"1","key":"205_CR20","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1142\/S021819401100513X","volume":"21","author":"VC Hu","year":"2011","unstructured":"Hu, V.C., Kuhn, D.R., Xie, T., Hwang, J.: Model checking for verification of mandatory access control models and properties. Int. J. Softw. Eng. Knowl. Eng. 21(1), 103\u2013127 (2011)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"issue":"6","key":"205_CR21","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/s10009-008-0087-9","volume":"10","author":"G Hughes","year":"2008","unstructured":"Hughes, G., Bultan, T.: Automated verification of access control policies using a SAT solver. Int. J. Softw. Tools Technol. Transf. 10(6), 503\u2013520 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"205_CR22","doi-asserted-by":"crossref","unstructured":"Hwang, J., Xie, T., Hu, V., Altunay, M.: ACPT: a tool for modeling and verifying access control policies. In: Proceedings of the 2010 IEEE International Symposium on Policies for Distributed Systems and Networks, POLICY \u201910, pp. 40\u201343. IEEE Computer Society, Washington, DC (2010)","DOI":"10.1109\/POLICY.2010.22"},{"key":"205_CR23","doi-asserted-by":"crossref","unstructured":"Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M., Chapin, S.: Automatic error finding in access-control policies. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS \u201911, pp. 163\u2013174. ACM, New York (2011)","DOI":"10.1145\/2046707.2046727"},{"key":"205_CR24","unstructured":"JeeHyun, H., Mine, A., Tao, X., Vincent, H.. Model Checking Grid Policies. https:\/\/sites.google.com\/site\/gridpolicyproject\/home"},{"key":"205_CR25","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TDSC.2007.70225","volume":"5","author":"S Jha","year":"2008","unstructured":"Jha, S., Li, N., Tripunitara, M., Wang, Q., Winsborough, W.: Towards formal verification of role-based access control policies. IEEE Trans. Dependable Secur. Comput. 5, 242\u2013255 (2008)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"issue":"3","key":"205_CR26","doi-asserted-by":"crossref","first-page":"036118","DOI":"10.1103\/PhysRevE.71.036118","volume":"71","author":"P Krapivsky","year":"2005","unstructured":"Krapivsky, P., Redner, S.: Network growth by copying. Phys. Rev. E 71(3), 036118 (2005)","journal-title":"Phys. Rev. E"},{"key":"205_CR27","doi-asserted-by":"crossref","unstructured":"Kuhn, D.R., Kacker, D.R.: Automated combinatorial test methods\u2014beyond pairwise testing (2010)","DOI":"10.6028\/NIST.SP.800-142"},{"key":"205_CR28","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 1st edn. Addison-Wesley Professional, Reading (2002)","edition":"1"},{"key":"205_CR29","unstructured":"Li, W., Wan, H., Ren, X., Li. S.: A refined rbac model for cloud computing. In: Computer and Information Science (ICIS), 2012 IEEE\/ACIS 11th International Conference on, pp. 43\u201348, (2012)"},{"issue":"6","key":"205_CR30","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MSP.2007.158","volume":"5","author":"N Li","year":"2007","unstructured":"Li, N., Byun, J.-W., Bertino, E.: A critique of the ANSI standard on role-based access control. IEEE Secur. Priv. 5(6), 41\u201349 (2007)","journal-title":"IEEE Secur. Priv."},{"key":"205_CR31","unstructured":"Mather, T., Kumaraswamy, S., Latif, S.: Cloud Security and Privacy: An Enterprise Perspective on Risks and Compliance. Oreilly & Associates Inc, (2009)"},{"key":"205_CR32","unstructured":"Microsoft. Windows azure security guidance, http:\/\/www.windowsazure.com\/en-us\/develop\/net\/best-practices\/security\/ , (2013)"},{"key":"205_CR33","doi-asserted-by":"crossref","unstructured":"Migliavacca, M., Papagiannis, I., Eyers, D.M., Shand, B., Bacon, J., Pietzuch, P.: Distributed middleware enforcement of event flow security policy. In: Middleware 2010, pp. 334\u2013354. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16955-7_17"},{"key":"205_CR34","unstructured":"NASA. Nebula\u2019s implementation of role based access control (RBAC), http:\/\/nebula.nasa.gov\/blog\/2010\/06\/03\/nebulas-implementation-role-based-access-control-rbac\/ , (2010)"},{"key":"205_CR35","unstructured":"NetworkX. Networkx, http:\/\/networkx.lanl.gov\/ , (2012)"},{"key":"205_CR36","unstructured":"NIST. Combinatorial and Pairwise Testing, http:\/\/csrc.nist.gov\/groups\/sns\/acts\/ , (2012)"},{"key":"205_CR37","unstructured":"NIST. Role based access control (RBAC) and role based security, http:\/\/csrc.nist.gov\/groups\/sns\/rbac\/index.html"},{"key":"205_CR38","unstructured":"NuSMV. A New Symbolic Model Checker, http:\/\/nusmv.fbk.eu\/"},{"key":"205_CR39","unstructured":"Nuutila, E.: Efficient transitive closure computation in large digraphs. PhD thesis, Acta Polytechnica Scandinavica. Helsinki University of Technology, (1995)"},{"key":"205_CR40","doi-asserted-by":"crossref","unstructured":"Oh, S., Sandhu, R.: A model for role administration using organization structure, (2002)","DOI":"10.1145\/507711.507737"},{"key":"205_CR41","unstructured":"OpenStack. Managing compute users, http:\/\/docs.openstack.org\/diablo\/openstack-compute\/admin\/content\/managing-compute-users.html , (2013)"},{"key":"205_CR42","unstructured":"OpenStack. Users and projects, http:\/\/docs.openstack.org\/diablo\/openstack-compute\/admin\/content\/users-and-projects.html (2013)"},{"key":"205_CR43","unstructured":"Peter, M., Timothy, G.: The NIST definition of cloud computing, September (2011)"},{"key":"205_CR44","doi-asserted-by":"crossref","unstructured":"Power, D., Slaymaker, M., Simpson, A.: Conformance checking of dynamic access control policies. In: Formal Methods and Software Engineering, pp. 227\u2013242. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24559-6_17"},{"key":"205_CR45","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BF01940892","volume":"10","author":"P Purdom","year":"1970","unstructured":"Purdom, P.: A transitive closure algorithm. BIT Numer. Math. 10, 76\u201394 (1970). doi: 10.1007\/BF01940892","journal-title":"BIT Numer. Math."},{"key":"205_CR46","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/35.312842","volume":"32","author":"RS Sandhu","year":"1994","unstructured":"Sandhu, R.S., Samarati, P.: Access control: principles and practice. IEEE Commun. Mag. 32, 40\u201348 (1994)","journal-title":"IEEE Commun. Mag."},{"issue":"2","key":"205_CR47","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.485845","volume":"29","author":"RS Sandhu","year":"1996","unstructured":"Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Comput. 29(2), 38\u201347 (1996)","journal-title":"IEEE Comput."},{"issue":"1","key":"205_CR48","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/300830.300839","volume":"2","author":"R Sandhu","year":"1999","unstructured":"Sandhu, R., Bhamidipati, V., Munawer, Q.: The arbac97 model for role-based administration of roles. ACM Trans. Inf. Syst. Secur. 2(1), 105\u2013135 (1999)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"205_CR49","unstructured":"SAnToS Laboratory. Spec patterns, response property pattern, http:\/\/patterns.projects.cis.ksu.edu\/ , (2012)"},{"key":"205_CR50","doi-asserted-by":"crossref","unstructured":"Schaad, A., Moffett, J., Jacob, J.: The role-based access control system of a european bank: a case study and discussion. In: Proceedings of the Sixth ACM Symposium on Access Control Models and Technologies, pp. 3\u20139. ACM (2001)","DOI":"10.1145\/373256.373257"},{"key":"205_CR51","doi-asserted-by":"crossref","unstructured":"Shafiq, B., Joshi, J.B.D., Bertino, E., Ghafoor, A.: Secure interoperation in a multidomain environment employing RBAC policies. IEEE Trans. Knowl. Data Eng. 17(11), 1557 (2005)","DOI":"10.1109\/TKDE.2005.185"},{"key":"205_CR52","unstructured":"SPIN. The SPIN model checker, http:\/\/spinroot.com\/spin\/"},{"issue":"6","key":"205_CR53","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/MSP.2010.186","volume":"8","author":"H Takabi","year":"2010","unstructured":"Takabi, H., Joshi, J.B., Ahn, G.-J.: Security and privacy challenges in cloud computing environments. IEEE Secur. & Priv. 8(6), 24\u201331 (2010)","journal-title":"IEEE Secur. & Priv."},{"key":"205_CR54","doi-asserted-by":"crossref","unstructured":"Tang, Z., Wei, J., Sallam, A., Li, K., Li, R.: A new rbac based access control model for cloud computing. In: Li, R., Cao, J., Bourgeois, J. (eds.) Advances in Grid and Pervasive Computing, volume 7296 of Lecture Notes in Computer Science, pp. 279\u2013288. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30767-6_24"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-013-0205-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-013-0205-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-013-0205-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,18]],"date-time":"2019-07-18T06:18:43Z","timestamp":1563430723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-013-0205-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,17]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["205"],"URL":"https:\/\/doi.org\/10.1007\/s10207-013-0205-x","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,17]]}}}