Apply Model Checking to Security Analysis in Trust Management

Trust management is a form of access control that uses delegation to achieve scalability beyond a single organization or federation. However, delegation can be difficult to control. A resource owner that delegates some authority is naturally concerned not only about who has access today, but also who will have access after others make changes to the global policy state. They need tools to help answer such questions. This problem has been studied in the case of a trust management language called RT. where, for simple questions concerning specific individuals, polynomial time algorithms are known. However, more useful questions, like "Could anyone who is not an employee ever get access?" are in general intractable. This paper concerns our efforts to build practical tools that answer such questions in many cases nevertheless by using a lightweight approach that leverages a mature model checking tool called SMV. Model checking is an automated technique that checks if desired properties hold in the model. Our experience, reported here, suggests that in our problem domain, such a tool may often be able to identify delegations that are unsafe with respect to security questions like the one mentioned above. We explain our translation from a RT policy and containment query to an SMV model and specification as well as demonstrate the feasibility of our approach with a case study.