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 propert...

• Type: Conference
• Year: 2007
• Where: ICDE
• Authors: Mark Reith, Jianwei Niu, William H. Winsborough
• Keywords: Database, ICDE 2007, Model Checking, Questions Concerning Specific, Trust Management