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.

翻译：现有的访问控制策略验证方法要求策略在验证前必须完整且完全确定，但在实践中策略通常通过迭代方式开发、由独立维护的组件组合而成，并随着组织结构演变而扩展。我们提出鲁棒性验证问题：即确定策略结构在未决决策如何解决以及后续扩展如何发生的情况下所必然满足的性质。我们定义了支持判断$\Vdash_{P}φ$以表示策略$P$具有鲁棒性质$φ$，其中包含蕴含、合取、析取与否定等逻辑连接词，通过单调性定理证明了该判断具有组合性（已验证性质在策略扩展下保持不变），并表明尽管该判断需对所有可能的策略扩展进行全称量化，但仍可归约为二阶逻辑编程语言中的证明搜索问题。我们建立了该归约的可靠性与完备性，从而得到了一种可有限执行且适用于鲁棒安全性质的验证方法。