{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:41:49Z","timestamp":1760060509694,"version":"build-2065373602"},"reference-count":37,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T00:00:00Z","timestamp":1756944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"US National Science Foundation (NSF)","award":["2152057","2318891"],"award-info":[{"award-number":["2152057","2318891"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCP"],"abstract":"<jats:p>Obligations in the Next-Generation Access Control (NGAC) standard enable the development of security-intensive workflow systems where access privileges evolve over time. However, specifying obligations for dynamic access requirements poses challenges, with errors having the potential to cause significant harm to the authorization state in NGAC applications. To identify and rectify such errors, our work aims to verify obligations by translating NGAC policies into logical formulas in SMTs (Satisfiability Modulo Theories). A primary challenge lies in the formalization of procedural obligations into declarative SMT formulas, given the potential for interference among administrative actions within an obligation. To address this issue, this paper analyzes all conflicts among obligation actions and formalizes them as logical formulas for the correct SMT-based verification of obligations in NGAC policies. We implemented the approach using the cvc5 solver and applied it to real-world systems. The results illustrate the successful formalization and verification of access control requirements.<\/jats:p>","DOI":"10.3390\/jcp5030066","type":"journal-article","created":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T08:08:46Z","timestamp":1756973326000},"page":"66","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analyzing Action Interference of Administrative Obligations for SMT-Based Verification"],"prefix":"10.3390","volume":"5","author":[{"given":"Vladislav","family":"Dubrovenski","sequence":"first","affiliation":[{"name":"Division of Computing, Analytics and Mathematics, School of Science and Engineering, University of Missouri-Kansas City, Kansas City, MO 64110, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leo","family":"Chen","sequence":"additional","affiliation":[{"name":"Division of Computing, Analytics and Mathematics, School of Science and Engineering, University of Missouri-Kansas City, Kansas City, MO 64110, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dianxiang","family":"Xu","sequence":"additional","affiliation":[{"name":"Division of Computing, Analytics and Mathematics, School of Science and Engineering, University of Missouri-Kansas City, Kansas City, MO 64110, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2025,9,4]]},"reference":[{"key":"ref_1","unstructured":"Irwin, K., Yu, T., and Winsborough, W. (November, January 30). On the Modeling and Analysis of Obligations. Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS\u201906), Alexandria, VA, USA."},{"key":"ref_2","unstructured":"OASIS (2025, August 31). eXtensible Access Control Markup Language (XACML), Version 3.0. Available online: https:\/\/www.oasis-open.org\/committees\/tc_home.php?wg_abbrev=xacml."},{"key":"ref_3","unstructured":"Li, N., Chen, H., and Bertino, E. (2012, January 8\u201310). On Practical Specification and Enforcement of Obligations. Proceedings of the 2nd ACM Conference on Data and Application Security and Privacy (CODASPY\u201912), San Antonio, TX, USA."},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Gorodetsky, V., Popyack, L., and Skormin, V. (2003). Usage Control: A Vision for Next Generation Access Control. Computer Network Security, Springer.","DOI":"10.1007\/b12005"},{"key":"ref_5","unstructured":"Jansen, W. (2020). Next Generation Access Control (NGAC), DPANS INCITS 565, Final, ANSI."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Elrakaiby, Y., Mouelhi, T., and Traon, Y.L. (2012, January 17\u201321). Testing Obligation Policy Enforcement Using Mutation Analysis. Proceedings of the 7th International Workshop on Mutation Analysis, Montreal, QC, Canada.","DOI":"10.1109\/ICST.2012.157"},{"key":"ref_7","unstructured":"Khamaiseh, S., Chapman, P., and Xu, D. (2018, January 16\u201320). Model-Based Testing of Obligatory ABAC Systems. Proceedings of the 18th International Conference on Software Quality, Reliability and Security (QRS\u201918), Lisbon, Portugal."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/984334.984339","article-title":"The UCON ABC Usage Control Model","volume":"7","author":"Park","year":"2004","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Dubrovenski, V., Chen, E., and Xu, D. (2023, January 26\u201330). SMT-Based Verification of NGAC Policies. Proceedings of the 2023 IEEE 47th Annual Computers, Software, and Applications Conference (COMPSAC), Torino, Italy.","DOI":"10.1109\/COMPSAC57700.2023.00115"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Chen, E., Dubrovenski, V., and Xu, D. (2021, January 16\u201318). Mutation Analysis of NGAC Policies. Proceedings of the 26th ACM Symposium on Access Control Models and Technologies, Virtual. SACMAT\u201921.","DOI":"10.1145\/3450569.3463563"},{"key":"ref_11","unstructured":"Fisman, D., and Rosu, G. (2022). cvc5: A Versatile and Industrial-Strength SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems, Springer."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/TSE.2017.2765640","article-title":"A Rigorous Framework for Specification, Analysis and Enforcement of Access Control Policies","volume":"45","author":"Margheri","year":"2019","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Hariri, A., Ibrahim, A., Alangot, B., Bandopadhyay, S., La Marra, A., Rosetti, A., Joumaa, H., and Dimitrakos, T. (2023). UCON+: Comprehensive Model, Architecture and Implementation for Usage Control and Continuous Authorization. Collaborative Approaches for Cyber Security in Cyber-Physical Systems, Springer.","DOI":"10.1007\/978-3-031-16088-2_10"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Sch\u00f6pp, U., Xu, C., Ibrahim, A., Faghih, F., and Dimitrakos, T. (2023). Specifying a Usage Control System. Proceedings of the 28th ACM Symposium on Access Control Models and Technologies, Trento, Italy, 7\u20139 June 2023, Association for Computing Machinery.","DOI":"10.1145\/3589608.3593843"},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"897","DOI":"10.1109\/TIFS.2017.2771492","article-title":"Specification and Verification of Separation of Duty Constraints in Attribute-Based Access Control","volume":"13","author":"Jha","year":"2018","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Jha, S., Sural, S., Atluri, V., and Vaidya, J. (2016, January 1\u20133). An Administrative Model for Collaborative Management of ABAC Systems and Its Security Analysis. Proceedings of the 2016 IEEE 2nd International Conference on Collaboration and Internet Computing (CIC), Pittsburgh, PA, USA.","DOI":"10.1109\/CIC.2016.022"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1049\/iet-ifs.2018.5010","article-title":"Security Analysis of ABAC under an Administrative Model","volume":"13","author":"Jha","year":"2019","journal-title":"IET Inf. Secur."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/300830.300839","article-title":"The ARBAC97 Model for Role-based Administration of Roles","volume":"2","author":"Sandhu","year":"1999","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"ref_19","first-page":"2349","article-title":"Cree: A Performant Tool for Safety Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies","volume":"18","author":"Shahen","year":"2021","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Biere, A., and Bloem, R. (2014). VAC\u2014Verifier of Administrative Role-Based Access Control Policies. Computer Aided Verification, Springer.","DOI":"10.1007\/978-3-319-08867-9"},{"key":"ref_21","first-page":"841","article-title":"Reachability Analysis for Attributes in ABAC with Group Hierarchy","volume":"20","author":"Maanak","year":"2022","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Shahen, J. (2015, January 1\u20133). Automated Safety Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies using Mohawk+T. Proceedings of the 20th ACM Symposium on Access Control Models and Technologies (SACMAT\u201915), Vienna, Austria.","DOI":"10.1145\/2752952.2752966"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Truong, A., and That, D. (2016, January 23\u201325). Solving the User-Role Reachability Problem in ARBAC with Role Hierarchy. Proceedings of the 2016 International Conference on Advanced Computing and Applications (ACOMP), Can Tho City, Vietnam.","DOI":"10.1109\/ACOMP.2016.011"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2595222","article-title":"Sophisticated Access Control via SMT and Logical Frameworks","volume":"16","author":"Arkoudas","year":"2014","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., and Varming, C. (November, January 30). Semantic-based Automated Reasoning for AWS Access Policies using SMT. Proceedings of the 2018 Formal Methods in Computer Aided Design (FMCAD), Austin, TX, USA.","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Xu, D., Shrestha, R., and Shen, N. (2020, January 10\u201312). Automated Strong Mutation Testing of XACML Policies. Proceedings of the 25th ACM Symposium on Access Control Models and Technologies (SACMAT\u201920), Barcelona, Spain.","DOI":"10.1145\/3381991.3395599"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Xu, D., Shrestha, R., and Shen, N. (2018, January 13\u201315). Automated Coverage-based Testing of XACML Policies. Proceedings of the 23rd ACM Symposium on Access Control Models and Technologies (SACMAT\u201918), Indianapolis, IN, USA.","DOI":"10.1145\/3205977.3205979"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1109\/TDSC.2024.3395187","article-title":"Detecting Errors in NGAC Policies Via Fault-Based Testing","volume":"22","author":"Chen","year":"2024","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Dubrovenski, V., Karim, N., Erzhuo, C., and Xu, D. (2023, January 22\u201326). Dynamic Access Control with Administrative Obligations: A Case Study. Proceedings of the Workshop of 2023 IEEE 23nd International Conference on Software Quality, Reliability and Security (QRS), Chiang Mai, Thailand.","DOI":"10.1109\/QRS-C60940.2023.00071"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Olivetti, N., and Tiwari, A. (2016). A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. Automated Reasoning, Springer.","DOI":"10.1007\/978-3-319-40229-1"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"de Moura, L. (2017). Relational Constraint Solving in SMT. Automated Deduction\u2014CADE 26, Springer.","DOI":"10.1007\/978-3-319-63046-5"},{"key":"ref_32","unstructured":"Arxer, J. (2018). Smt Techniques for Planning Problems. [Ph.D. Thesis, University of Girona]."},{"key":"ref_33","unstructured":"Kautz, H., and Selman, B. (1992, January 3\u20137). Planning as Satisfiability. Proceedings of the 10th European Conference on Artificial Intelligence (ECAI\u201992), Vienna, Austria."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., and Zhu, Y. (1999). Symbolic Model Checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), Springer.","DOI":"10.21236\/ADA360973"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1145\/360303.360333","article-title":"Protection in operating systems","volume":"19","author":"Harrison","year":"1976","journal-title":"Commun. ACM"},{"key":"ref_36","unstructured":"NGACTeam (2025, August 31). NGAC Reference Implementation. Available online: https:\/\/github.com\/usnistgov\/policy-machine-core."},{"key":"ref_37","unstructured":"Xu, D. (2025, August 31). Modern Software Engineering: Principles and Practices\u2014Writing Clean, Dependable Code. Available online: https:\/\/www.amazon.co.jp\/-\/en\/Modern-Software-Engineering-Principles-Dependable\/dp\/B08TY85J94."}],"container-title":["Journal of Cybersecurity and Privacy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2624-800X\/5\/3\/66\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:39:12Z","timestamp":1760035152000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2624-800X\/5\/3\/66"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,4]]},"references-count":37,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2025,9]]}},"alternative-id":["jcp5030066"],"URL":"https:\/\/doi.org\/10.3390\/jcp5030066","relation":{},"ISSN":["2624-800X"],"issn-type":[{"type":"electronic","value":"2624-800X"}],"subject":[],"published":{"date-parts":[[2025,9,4]]}}}