Analyzing Action Interference of Administrative Obligations for SMT-Based Verification

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.