{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,27]],"date-time":"2023-12-27T11:35:16Z","timestamp":1703676916159},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2015,12,18]],"date-time":"2015-12-18T00:00:00Z","timestamp":1450396800000},"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 Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10009-015-0410-1","type":"journal-article","created":{"date-parts":[[2015,12,18]],"date-time":"2015-12-18T10:54:44Z","timestamp":1450436084000},"page":"559-573","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Parameterized model checking for security policy analysis"],"prefix":"10.1007","volume":"18","author":[{"given":"Silvio","family":"Ranise","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anh","family":"Truong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Traverso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,18]]},"reference":[{"issue":"2","key":"410_CR1","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1504\/IJCSE.2007.015739","volume":"3","author":"S Capitani di Vimercati De","year":"2007","unstructured":"De Capitani di Vimercati, S., Foresti, S., Jajodia, S., Samarati, P.: Access control policies and languages. Int J Comput Sci Eng (IJCSE) 3(2), 94\u2013102 (2007)","journal-title":"Int J Comput Sci Eng (IJCSE)"},{"issue":"8","key":"410_CR2","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1145\/360303.360333","volume":"19","author":"MA Harrison","year":"1976","unstructured":"Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. CACM 19(8), 461\u2013471 (1976)","journal-title":"CACM"},{"issue":"1","key":"410_CR3","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/TDSC.2012.77","volume":"10","author":"M Tripunitara","year":"2013","unstructured":"Tripunitara, M., Li, N.: The foundational work of Harrison\u2013Ruzzo\u2013Ullman revisited. IEEE Trans Depend Sec Comput 10(1), 28\u201339 (2013)","journal-title":"IEEE Trans Depend Sec Comput"},{"issue":"4","key":"410_CR4","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/JCS-2012-0461","volume":"20","author":"A Armando","year":"2012","unstructured":"Armando, A., Ranise, S.: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. J Comput Secur 20(4), 309\u2013352 (2012)","journal-title":"J Comput Secur"},{"key":"410_CR5","doi-asserted-by":"crossref","unstructured":"Ferrara, A.L., Madhusudan, P., Parlato, G.: Policy analysis for self-administrated role-based access control. In: TACAS. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_30"},{"issue":"29","key":"410_CR6","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.485845","volume":"2","author":"R Sandhu","year":"1996","unstructured":"Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-based access control models. IEEE Comput 2(29), 38\u201347 (1996)","journal-title":"IEEE Comput"},{"issue":"2","key":"410_CR7","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/300830.300839","volume":"1","author":"R Sandhu","year":"1999","unstructured":"Sandhu, R., Bhamidipati, V., Munawer, Q.: The ARBAC97 model for role-based control administration of roles. ACM TISSEC 1(2), 105\u2013135 (1999)","journal-title":"ACM TISSEC"},{"key":"410_CR8","doi-asserted-by":"crossref","unstructured":"Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M., Chapin, S.: Automatic error finding for access-control policies. In: CCS. ACM, New York (2011)","DOI":"10.1145\/2046707.2046727"},{"issue":"4","key":"410_CR9","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/1187441.1187442","volume":"9","author":"N Li","year":"2006","unstructured":"Li, N., Tripunitara, M.V.: Security analysis in role-based access control. ACM TISSEC 9(4), 391\u2013420 (2006)","journal-title":"ACM TISSEC"},{"key":"410_CR10","doi-asserted-by":"crossref","unstructured":"Stoller, S.D., Yang, P., Ramakrishnan, C.R., Gofman, M.I.: Efficient policy analysis for administrative role based access control. In: CCS. ACM Press, New York (2007)","DOI":"10.1145\/1315245.1315300"},{"key":"410_CR11","doi-asserted-by":"crossref","unstructured":"Yang, P., Gofman, M.l., Stoller, S., Yang, Z.: Policy analysis for administrative role based access control without separate administration. J Comput Secur (2014)","DOI":"10.1007\/978-3-642-39256-6_4"},{"key":"410_CR12","doi-asserted-by":"crossref","unstructured":"Sasturkar, A., Yang, P., Stoller, S.D., Ramakrishnan, C.R.: Policy analysis for administrative role based access control. In: CSF. IEEE Press, New York (2006)","DOI":"10.1109\/CSFW.2006.22"},{"key":"410_CR13","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"410_CR14","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. In: LMCS, vol. 6, no 4 (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"410_CR15","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Proceedings of IJCAR\u201910. LNCS, New York (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"issue":"4","key":"410_CR16","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J Autom Reas 44(4), 401\u2013424 (2010)","journal-title":"J Autom Reas"},{"key":"410_CR17","doi-asserted-by":"crossref","unstructured":"Crampton, J.: Understanding and developing role-based administrative models. In: Proceedings of the 12th CCS. ACM Press, New York, pp. 158\u2013167 (2005)","DOI":"10.1145\/1102120.1102143"},{"issue":"44","key":"410_CR18","doi-asserted-by":"crossref","first-page":"6208","DOI":"10.1016\/j.tcs.2011.05.009","volume":"412","author":"A Sasturkar","year":"2011","unstructured":"Sasturkar, A., Yang, P., Stoller, S.D., Ramakrishnan, C.R.: Policy analysis for administrative role based access control. Theor Comput Sci 412(44), 6208\u20136234 (2011)","journal-title":"Theor Comput Sci"},{"issue":"1","key":"410_CR19","first-page":"24","volume":"42","author":"S Ranise","year":"2013","unstructured":"Ranise, S.: Symbolic backward reachability with effectively propositional logic-applications to security policy analysis. FMSD 42(1), 24\u201345 (2013)","journal-title":"FMSD"},{"issue":"1","key":"410_CR20","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"s2\u201330","author":"FP Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc Lond Math Soc s2\u201330(1), 264\u2013286 (1930)","journal-title":"Proc Lond Math Soc"},{"issue":"6","key":"410_CR21","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"B Beckert","year":"2006","unstructured":"Beckert, B., Hoare, C.A.R., H\u00e4hnle, R., Smith, R., Green, D.R., Ranise, S., Tinelli, C., Ball, T., Rajamani, S.K.: Intelligent systems and formal methods in software engineering. IEEE Int Syst 21(6), 71\u201381 (2006)","journal-title":"IEEE Int Syst"},{"key":"410_CR22","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"1972","unstructured":"Enderton, H.B.: A mathematical introduction to logic. Academic Press Inc, New York (1972)"},{"key":"410_CR23","doi-asserted-by":"crossref","unstructured":"Alberti, F., Armando, A., Ranise, S.: ASASP: automated symbolic analysis of security policies. In: CADE. LNCS, vol. 6803. Springer, Berlin, pp 26\u201334 (2011)","DOI":"10.1007\/978-3-642-22438-6_4"},{"key":"410_CR24","doi-asserted-by":"crossref","unstructured":"Ranise, S., Truong, T.A., Armando, A.: Boosting model checking to analyse large ARBAC policies. In: 8th STM Workshop, LNCS, vol. 7783. Springer, Berlin, pp 273\u2013288 (2012)","DOI":"10.1007\/978-3-642-38004-4_18"},{"key":"410_CR25","doi-asserted-by":"crossref","unstructured":"Gofman, M.I., Luo, R., Solomon, A.C., Zhang, Y., Yang, P., Stoller, S.D.: Rbac-pat: a policy analysis tool for role based access control. In: TACAS, LNCS, vol. 5505. Springer, Berlin, pp 46\u201349 (2009)","DOI":"10.1007\/978-3-642-00768-2_4"},{"key":"410_CR26","doi-asserted-by":"crossref","unstructured":"Li, N., Tripunitara, M.V.: Security analysis in role-based access control. In: Symp. on Access Control Models and Technologies. ACM Press, New York, pp 126\u2013135 (2004)","DOI":"10.1145\/990036.990058"},{"issue":"4","key":"410_CR27","first-page":"242","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 TDSeC 5(4), 242\u2013255 (2008)","journal-title":"IEEE TDSeC"},{"key":"410_CR28","doi-asserted-by":"crossref","unstructured":"Alberti, F., Armando, A., Ranise, S.: Efficient symbolic automated analysis of administrative role based access control policies. In: ASIACCS. ACM Press, New York (2011)","DOI":"10.1145\/1966913.1966935"},{"key":"410_CR29","doi-asserted-by":"crossref","unstructured":"Jayaraman, K., Tripunitara, M.V., Ganesh, V., Rinard, M.C., Chapin, S.J.: Mohawk: abstraction-refinement and bound-estimation for verifying access control policies. ACM TISSeC 15(4) (2013)","DOI":"10.1145\/2445566.2445570"},{"key":"410_CR30","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Strichman, O., Zhu, Y., Biere, A., Cimatti, A.: Bounded model checking. Adv Comput 58, 117\u2013148 (2003)","journal-title":"Adv Comput"},{"key":"410_CR31","doi-asserted-by":"crossref","unstructured":"Ranise, S., Traverso, R.: ALPS: an action language for policy specification and automated safety analysis. In: STM Workshop, number 8743 in LNCS. Springer, Berlin, pp. 146\u2013161 (2014)","DOI":"10.1007\/978-3-319-11851-2_10"},{"issue":"3","key":"410_CR32","first-page":"189","volume":"2","author":"Richard E Fikes","year":"1972","unstructured":"Fikes, Richard E., Nilsson, Nils J.: Strips: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3), 189\u2013208 (1972)","journal-title":"Artif. Intell."},{"key":"410_CR33","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0004-3702(94)00080-K","volume":"76","author":"K Erol","year":"1991","unstructured":"Erol, K., Nau, D.S., Subrahmanian, V.S.: Complexity, decidability and undecidability results for domain-independent planning: a detailed analysis. Artif. Intell. 76, 75\u201388 (1991)","journal-title":"Artif. Intell."},{"key":"410_CR34","doi-asserted-by":"crossref","unstructured":"Ranise, S., Truong, A.: Incremental analysis of evolving administrative role based access control policies. In: 28th Annual IFIP WG 11.3 Working Conference DBSeC14, Vienna, Austria, 14-16 July 2014. LNCS, vol 8566. Springer, Berlin, pp. 260\u2013275 (2014)","DOI":"10.1007\/978-3-662-43936-4_17"},{"key":"410_CR35","unstructured":"Gofman, M., Yang, P.: Efficient policy analysis for evolving administrative role based access control. Int J Softw Inf (2014)"},{"key":"410_CR36","doi-asserted-by":"crossref","unstructured":"Gofman, M.I., Luo, R., Yang, P.: User-role reachability analysis of evolving administrative role based access control. In: ESORICS, vol. 6345. LNCS, Berlin, pp. 455\u2013471 (2010)","DOI":"10.1007\/978-3-642-15497-3_28"},{"key":"410_CR37","doi-asserted-by":"crossref","unstructured":"Ranise, S., Truong, A., Armando, A.: Scalable and precise automated analysis of administrative temporal role-based access control. In: tACM SACMAT, London, Ontario, Canada, June 25\u201325 2014. ACM Press, New York, pp. 103\u2013114 (2014)","DOI":"10.1145\/2613087.2613102"},{"key":"410_CR38","doi-asserted-by":"crossref","unstructured":"Uzun, E., Atluri, V., Sural, S., Vaidya, J, Parlato G, Ferrara AL (2012) Analyzing temporal role based access control models. In: SACMAT. ACM, New York, pp. 177\u2013186 (2014)","DOI":"10.1145\/2295136.2295169"},{"key":"410_CR39","doi-asserted-by":"crossref","unstructured":"Ranise, S., Truong, A., Vigan\u00f2, L.: Automated analysis of RBAC policies with temporal constraints and static role hierarchies. In: 30th ACM\/SIGAPP SAC, Salamanca, Spain, April 13\u201317, 2015. ACM Press, New York (2015)","DOI":"10.1145\/2695664.2695787"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0410-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0410-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0410-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,2]],"date-time":"2019-09-02T18:04:38Z","timestamp":1567447478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0410-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,18]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["410"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0410-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,18]]}}}