Verification of Robust Properties for Access Control Policies
2026-03-13 • Cryptography and Security
Cryptography and SecurityLogic in Computer Science
AI summaryⓘ
The authors address a problem in checking security rules for computer systems, which normally require the rules to be complete before checking. They introduce a new way to verify properties that hold true no matter how the rules might change or grow in the future. They create a method to prove these "robust" properties using logical reasoning and show that this method works even as policies evolve. Their approach turns a complex problem into one that can be solved with existing logic programming techniques, making verification practical and reliable.
access control policiespolicy verificationrobust propertymonotonicitysecond-order logiclogic programmingcompositionalitysecurity properties
Authors
Alexander V. Gheorghiu
Abstract
Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed, but in practice policies are developed iteratively, composed from independently maintained components, and extended as organisational structures evolve. We introduce robust property verification: the problem of determining what a policy's structure commits it to regardless of how pending decisions are resolved and regardless of subsequent extension. We define a support judgment $\Vdash_{P}φ$ stating that policy $P$ has robust property $φ$, with connectives for implication, conjunction, disjunction, and negation, prove that it is compositional (verified properties persist under policy extension by a monotonicity theorem), and show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language. Soundness and completeness of this reduction are established, yielding a finitary and executable verification procedure for robust security properties.