Correspondence:
[*]
Corresponding author: Jianwei Niu, University of Texas at San Antonio, One UTSA Circle, San Antonio, 78249 TX, USA. E-mail: jianwei.niu@utsa.edu
Note: [**] The author is affiliated with the United States Air Force. The views expressed in this article are those of the author and do not reflect the official policy or position of the United States Air Force, Department of Defense, or the U.S. Government.
Abstract: 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.
Keywords: Security policy, formal verification, trust management, model checking
