Formal verification of security properties in trust management policy

Trust management is a scalable form of access control that relies heavily on delegation. Different parts of the policy are under the control of different principals in the system. While these two characteristics may be necessary in large or decentralized systems, they make it difficult to anticipate how policy changes made by others will affect whether ones own security objectives are met. Automated analysis tools are needed for assessing this question. The article develops techniques that support the development of tools to solve many analysis problem instances. When an access control policy fails to satisfy desired security objectives, the tools provide information about how and why the failure occurs. Such information can assist policy authors design appropriate policies. The approach to performing the analysis is based on model checking. To assist in making the approach effective, a collection of reduction techniques is introduced. We prove the correctness of these reductions and empirically evaluate their effectiveness. While the class of analysis problem instances we examine is generally intractable, we find that our reduction techniques are often able to reduce some problem instances into a form that can be automatically verified.