Verification of Robust Properties for Access Control Policies

Computer Science > Cryptography and Security [Submitted on 13 Mar 2026] Verification of Robust Properties for Access Control Policies Alexander V. Gheorghiu 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}\phi stating that policy P has robust property \phi, 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. Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO) Cite as: arXiv:2603.13181 [cs.CR]   (or arXiv:2603.13181v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2603.13181 Focus to learn more Submission history From: Alexander Gheorghiu [view email] [v1] Fri, 13 Mar 2026 17:14:38 UTC (24 KB) Access Paper: HTML (experimental) view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-03 Change to browse by: cs cs.LO References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)