{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:25:33Z","timestamp":1759091133129,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,4,1]],"date-time":"2013-04-01T00:00:00Z","timestamp":1364774400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2013,4]]},"abstract":"<jats:p>\n            Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present techniques for abstraction-refinement and bound-estimation for bounded model checkers to automatically find errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. In the abstraction-refinement portion of our approach, we identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step). We then restore such abstracted roles incrementally (the refinement steps). In the bound-estimation portion of our approach, we lower the estimate of the diameter of the reachability graph from the worst-case by recognizing relationships between roles and state-change rules. Our techniques complement one another, and are used with conventional bounded model checking. Our approach is sound and complete: an error is found if and only if it exists. We have implemented our technique in an access-control policy analysis tool called\n            <jats:sc>Mohawk<\/jats:sc>\n            . We show empirically that\n            <jats:sc>Mohawk<\/jats:sc>\n            scales well to realistic policies, and provide a comparison with prior tools.\n          <\/jats:p>","DOI":"10.1145\/2445566.2445570","type":"journal-article","created":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T12:17:58Z","timestamp":1365509878000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Mohawk"],"prefix":"10.1145","volume":"15","author":[{"given":"Karthick","family":"Jayaraman","sequence":"first","affiliation":[{"name":"Microsoft"}]},{"given":"Mahesh","family":"Tripunitara","sequence":"additional","affiliation":[{"name":"University of Waterloo"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[{"name":"MIT"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[{"name":"MIT"}]},{"given":"Steve","family":"Chapin","sequence":"additional","affiliation":[{"name":"Syracuse University"}]}],"member":"320","published-online":{"date-parts":[[2013,4]]},"reference":[{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. 87--97","author":"Ammann P.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","unstructured":"Aveksa. 2012. What is business-driven identity and access management? http:\/\/www.aveksa.com\/ what-we-do\/What-Is-Business-Driven-Identity-and-Access-Management.cfm.  Aveksa. 2012. What is business-driven identity and access management? http:\/\/www.aveksa.com\/ what-we-do\/What-Is-Business-Driven-Identity-and-Access-Management.cfm."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_4_1","first-page":"413","article-title":"Safety in grammatical protection systems","volume":"12","author":"Budd T. A.","year":"1983","journal-title":"Int. J. Paral. Prog."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0182-5"},{"key":"e_1_2_1_8_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking . The MIT Press."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/762476.762478"},{"key":"e_1_2_1_10_1","unstructured":"Ferraiolo D. F. Kuhn D. R. and Chandramouli R. 2003. Role-Based Access Control. Artech House Inc. Norwood MA.   Ferraiolo D. F. Kuhn D. R. and Chandramouli R. 2003. Role-Based Access Control . Artech House Inc. Norwood MA."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.28"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062502"},{"volume-title":"Proceedins of the 19th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science","author":"Ganesh V.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_4"},{"volume-title":"Proceedings of the 15th European Conference on Research in Computer Security (ESORICS\u201910)","author":"Gofman M. I.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1478873.1478928"},{"volume-title":"Proceedings of the Conference on Foundations of Secure Computation. 461--471","author":"Harrison M. A.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/800213.806517"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1377836.1377867"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/EUC.2008.22"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220888.3221027"},{"key":"e_1_2_1_22_1","unstructured":"Jayaramam K. 2012. Mohawk -- Automatic Verification of Access-Control Policies. http:\/\/code.google.com\/p\/mohawk\/.  Jayaramam K. 2012. Mohawk -- Automatic Verification of Access-Control Policies. http:\/\/code.google.com\/p\/mohawk\/."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046727"},{"key":"e_1_2_1_24_1","unstructured":"Jayaraman K. Ganesh V. Tripunitara M. Rinard M. C. and Chapin S. J. 2012. Real-world case studies of using ARBAC to enforce separation-of-duty constraints. http:\/\/kjayaram.mysite.syr.edu\/mohawk\/casestudy.pdf.  Jayaraman K. Ganesh V. Tripunitara M. Rinard M. C. and Chapin S. J. 2012. Real-world case studies of using ARBAC to enforce separation-of-duty constraints. http:\/\/kjayaram.mysite.syr.edu\/mohawk\/casestudy.pdf."},{"key":"e_1_2_1_25_1","first-page":"3","article-title":"Model Checking SPKI\/SDSI","volume":"12","author":"Jha S.","year":"2004","journal-title":"J. Comput. Sec."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.70225"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/784592.784781"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242664"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.07.021"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/990036.990058"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1187441.1187442"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066103"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242663"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/335305.335341"},{"key":"e_1_2_1_37_1","unstructured":"NuSMV. 2012. http:\/\/nusmv.irst.itc.it\/.  NuSMV. 2012. http:\/\/nusmv.irst.itc.it\/."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/POLICY.2007.51"},{"key":"e_1_2_1_39_1","unstructured":"SailPoint. 2012. Policy enforcement. http:\/\/www.sailpoint.com\/products\/identity-iq\/compliance-manager\/policy-enforcement.php.  SailPoint. 2012. Policy enforcement. http:\/\/www.sailpoint.com\/products\/identity-iq\/compliance-manager\/policy-enforcement.php."},{"volume-title":"Proc. IEEE.","author":"Saltzer J. H.","key":"e_1_2_1_40_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/300830.300839"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/882488.884182"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.485845"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.22"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.009"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/373256.373257"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2008.28"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy, 56","author":"Solworth J. A.","key":"e_1_2_1_48_1"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/646648.699356"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1315245.1315300"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370684.1370685"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560647_25"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2445566.2445570","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2445566.2445570","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:09Z","timestamp":1750239249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2445566.2445570"}},"subtitle":["Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies"],"short-title":[],"issued":{"date-parts":[[2013,4]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["10.1145\/2445566.2445570"],"URL":"https:\/\/doi.org\/10.1145\/2445566.2445570","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"type":"print","value":"1094-9224"},{"type":"electronic","value":"1557-7406"}],"subject":[],"published":{"date-parts":[[2013,4]]},"assertion":[{"value":"2012-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}