Security policy analysis in a trust management environment

Trust management is a scalable and flexible form of access control that relies heavily on delegation techniques. While these techniques may be necessary in large or decentralized systems, stakeholders need an analysis methodology and automated tools for reasoning about who will have access to their resources today as well as in the future. When an access control policy fails to satisfy the policy author's security objectives, tools should provide information that demonstrate how and why the failure occurred. Such information is useful in that it may assist policy authors in constructing policies that satisfy security objectives, which support policy authoring and maintenance. This dissertation presents a collection of reduction, optimization, and verification techniques useful in determining whether security properties are satisfied by RT policies. We provide proofs of correctness for each of the reductions and implement them in a tool called RT-SPACE. Furthermore, we demonstrate the degree of effectiveness and efficiency the techniques provide through empirical evaluation of a collection of manually and randomly constructed problem instances. While the type of analysis problem we examine is intractable in the general case, we demonstrate that our reduction and optimization techniques are able to reduce many problem instances to a form that can be automatically verified.

This work is significant because it bridges the early theoretical work with the practical concerns of analyzing security objectives in trust management. First, it identifies several techniques for reducing a prohibitively expensive problem instance into a form that can be evaluated using model checking. Second, through the leverage of symbolic model checking we are able to evaluate non-trivial problem instances and produce counterexamples in the case that the policy fails to satisfy the desired security property. This information is critical as it provides stakeholders insight to policy correction. Finally, we implement our framework as a tool that can be reviewed by other researchers. The summation of this work is a framework that advances our understanding of techniques that provide decisive answers to access control questions for the purpose of ensuring security on today's information systems.