{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:05:26Z","timestamp":1762506326958,"version":"3.41.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T00:00:00Z","timestamp":1396310400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006751","name":"U.S. Army","doi-asserted-by":"publisher","award":["W15P7T-08-C-P213"],"award-info":[{"award-number":["W15P7T-08-C-P213"]}],"id":[{"id":"10.13039\/100006751","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>We introduce a new methodology for formulating, analyzing, and applying access-control policies. Policies are expressed as formal theories in the SMT (satisfiability-modulo-theories) subset of typed first-order logic, and represented in a programmable logical framework, with each theory extending a core ontology of access control. We reduce both request evaluation and policy analysis to SMT solving, and provide experimental results demonstrating the practicality of these reductions. We also introduce a class of canonical requests and prove that such requests can be evaluated in linear time. In many application domains, access requests are either naturally canonical or can easily be put into canonical form. The resulting policy framework is more expressive than XACML and languages in the Datalog family, without compromising efficiency. Using the computational logic facilities of the framework, a wide range of sophisticated policy analyses (including consistency, coverage, observational equivalence, and change impact) receive succinct formulations whose correctness can be straightforwardly verified. The use of SMT solving allows us to efficiently analyze policies with complicated numeric (integer and real) constraints, a weak point of previous policy analysis systems. Further, by leveraging the programmability of the underlying logical framework, our system provides exceptionally flexible ways of resolving conflicts and composing policies. Specifically, we show that our system subsumes FIA (Fine-grained Integration Algebra), an algebra recently developed for the purpose of integrating complex policies.<\/jats:p>","DOI":"10.1145\/2595222","type":"journal-article","created":{"date-parts":[[2014,5,7]],"date-time":"2014-05-07T12:48:53Z","timestamp":1399466933000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Sophisticated Access Control via SMT and Logical Frameworks"],"prefix":"10.1145","volume":"16","author":[{"given":"Konstantine","family":"Arkoudas","sequence":"first","affiliation":[{"name":"Applied Communications Sciences"}]},{"given":"Ritu","family":"Chadha","sequence":"additional","affiliation":[{"name":"Applied Communications Sciences"}]},{"given":"Jason","family":"Chiang","sequence":"additional","affiliation":[{"name":"Applied Communications Sciences"}]}],"member":"320","published-online":{"date-parts":[[2014,4]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155225"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/POLICY.2005.25"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966913.1966935"},{"key":"e_1_2_2_4_1","unstructured":"Anderson R. J. 2008. Security Engineering 2nd Ed. Wiley.  Anderson R. J. 2008. Security Engineering 2nd Ed. Wiley."},{"key":"e_1_2_2_5_1","first-page":"169","article-title":"Rule-based policy specification. In Secure Data Management in Decentralized Systems, T. Yu and S. Jajodia Eds","volume":"33","author":"Antoniou G.","year":"2007","journal-title":"Advances in Information Security Series"},{"key":"e_1_2_2_6_1","unstructured":"Arkoudas K. 2004. Athena. http:\/\/proofcentral.org\/athena\/.  Arkoudas K. 2004. Athena. http:\/\/proofcentral.org\/athena\/."},{"volume-title":"Proceedings of the Design and Implementation of Formal Tools and Systems, a Workshop of Formal Methods in Computer Aided Design (DIFTS\/FMCAD\u201911)","author":"Arkoudas K.","key":"e_1_2_2_7_1"},{"volume-title":"Proceedings of the 4th International Conference on Cognitive Radios (CogArt\u201911)","author":"Arkoudas K.","key":"e_1_2_2_8_1"},{"volume-title":"Proceedings of the IEEE Symposium on New Frontiers in Dynamic Spectrum. 1--12","author":"Bahrak B.","key":"e_1_2_2_9_1"},{"volume-title":"Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY\u201903)","author":"Bandara A. K.","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.18"},{"volume-title":"Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks. 159--168","author":"Becker M. Y.","key":"e_1_2_2_12_1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/605434.605437"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/504909.504910"},{"volume-title":"Proceedings of the 17th European Conference on Artificial Intelligence. IOS Press, 200--204","author":"Bonatti P. A.","key":"e_1_2_2_15_1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1952982.1952991"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103022.1103028"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Chadha R. and Kant L. 2007. Policy-Driven Mobile Ad Hoc Network Management. Wiley\/IEEE Press.   Chadha R. and Kant L. 2007. Policy-Driven Mobile Ad Hoc Network Management . Wiley\/IEEE Press.","DOI":"10.1002\/9780470227718"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_21"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770358"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/829514.830540"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062502"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/367390.367400"},{"volume-title":"Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR\u201901)","author":"Haarslev V.","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1380564.1380569"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360303.360333"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/283751.283768"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0087-9"},{"key":"e_1_2_2_31_1","unstructured":"Huonder F. 2010. Conflict detection and resolution of xacml policies. Masters thesis University of Applied Sciences Rapperswil.  Huonder F. 2010. Conflict detection and resolution of xacml policies. Masters thesis University of Applied Sciences Rapperswil."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003500"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/383891.383894"},{"volume":"2","volume-title":"Proceedings of the 21st National Conference on Artificial Intelligence.","author":"Kagal L.","key":"e_1_2_2_35_1"},{"volume-title":"Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY\u201903)","author":"Kagal L.","key":"e_1_2_2_36_1"},{"volume-title":"Proceedings of the 18th International Conference on Very Large Data Bases (VLDB\u201992)","author":"Kemper A.","key":"e_1_2_2_37_1"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Kolovski V. 2008. Logic-based framework for web access control policies. Ph.D. thesis Computer Science Department University of Maryland.   Kolovski V. 2008. Logic-based framework for web access control policies. Ph.D. thesis Computer Science Department University of Maryland.","DOI":"10.1145\/1242572.1242664"},{"key":"e_1_2_2_39_1","unstructured":"Kolovski V. and Hendler J. 2008. XACML policy analysis using description logics. www.mindswap.org\/~kolovskiKolovskiXACMLAnalysisJCSSubmission.pdf.  Kolovski V. and Hendler J. 2008. XACML policy analysis using description logics. www.mindswap.org\/~kolovskiKolovskiXACMLAnalysisJCSSubmission.pdf."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242664"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/645773.668099"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370684.1370686"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/121133.121160"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 114--130","author":"Li N.","key":"e_1_2_2_44_1"},{"volume-title":"Proceedings of the 5th NOTERE Conference. 85--91","author":"Mankai M.","key":"e_1_2_2_45_1"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/646562.695571"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2013.02.002"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542207.1542218"},{"key":"e_1_2_2_50_1","unstructured":"Rissanen E. 2007. Extensible access control markup language (xacml) version 3.0 (core specication and schemas). www.oasis-open.org\/committees\/download.php\/23950\/xacml-3.0-core-wd-02.zip.  Rissanen E. 2007. Extensible access control markup language (xacml) version 3.0 (core specication and schemas). www.oasis-open.org\/committees\/download.php\/23950\/xacml-3.0-core-wd-02.zip."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.24"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/300830.300839"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/507711.507714"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11604655_48"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 106--115","year":"2001","author":"Trevor J.","key":"e_1_2_2_55_1"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2004.31"},{"key":"e_1_2_2_57_1","doi-asserted-by":"crossref","unstructured":"Westerinen A. Schnizlein J. Strassner J. Scherling M. Quinn B. Herzog S. Huynh A. Carlson M. Perry J. and Waldbusser S. 2001. Terminology for policy-based management. RFC 3198 (Informational).   Westerinen A. Schnizlein J. Strassner J. Scherling M. Quinn B. Herzog S. Huynh A. Carlson M. Perry J. and Waldbusser S. 2001. Terminology for policy-based management. RFC 3198 (Informational).","DOI":"10.17487\/rfc3198"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/762476.762481"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201992)","author":"Woo T. Y. C.","key":"e_1_2_2_59_1"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1993-22-304"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11556992_32"},{"key":"e_1_2_2_62_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\/2595222","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2595222","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:04Z","timestamp":1750234204000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2595222"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":62,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["10.1145\/2595222"],"URL":"https:\/\/doi.org\/10.1145\/2595222","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"type":"print","value":"1094-9224"},{"type":"electronic","value":"1557-7406"}],"subject":[],"published":{"date-parts":[[2014,4]]},"assertion":[{"value":"2012-02-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":"2014-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}