Title
Apply Model Checking to Security Analysis in Trust Management
Abstract
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.
Year
DOI
Venue
2007
10.1109/ICDEW.2007.4401061
ICDE Workshops
Keywords
Field
DocType
mature model checking tool,rt policy,trust management,apply model,case study,lightweight approach,problem domain,security analysis,access control,model checking,global policy state,practical tool,smv model,software systems,system testing,algorithms,systems analysis,language,management,maturity model,formal verification,government,polynomials,automation,hazards,authorisation,control,scalability,policies,security
Data mining,Model checking,Problem domain,Computer science,Computer security,Systems analysis,Security analysis,Access control,Delegation,Database,Formal verification,Scalability
Conference
ISSN
Citations 
PageRank 
1943-2895
6
0.51
References 
Authors
10
3
Name
Order
Citations
PageRank
Mark Reith112222.82
Jianwei Niu227526.61
William H. Winsborough31909127.02