Theoretical Foundation for Model Checking Role Containment in RT
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 paper 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 as well as demonstrate the degree of effectiveness and efficiency the techniques provide through empirical evaluation. While the type of analysis problem we examine is generally intractable, we demonstrate that our reduction and optimization techniques may be able to reduce problem instances into a form that can be automatically verified.