Paper Info
Title
Towards formal security analysis of GTRBAC using timed automata
Abstract
An access control system is often viewed as a state transition system. Given a set of access control policies, a general safety requirement in such a system is to determine whether a desirable property is satisfied in all the reachable states. Such an analysis calls for formal verification. While formal analysis on traditional RBAC has been done to some extent, the extensions of RBAC lack such an analysis. In this paper, we propose a formal technique to perform security analysis on the Generalized Temporal RBAC (GTRBAC) model which can be used to express a wide range of temporal constraints on different RBAC components like role, user and permission. In the proposed approach, at first the GTRBAC system is mapped to a state transition system built using timed automata. Characteristics of each role, user and permission are captured with the help of timed automata. A single global clock is used to express the various temporal constraints supported in a GTRBAC model. Next, a set of safety and liveness properties is specified using computation tree logic (CTL). Model checking based formal verification is then done to verify the properties against the model to determine if the system is secure with respect to a given set of access control policies. Both time and space analysis has been done for studying the performance of the approach under different configurations.
Year
DOI
Venue
2009
10.1145/1542207.1542214
SACMAT
Keywords
Field
DocType
gtrbac model,access control system,gtrbac system,security analysis,towards formal security analysis,analysis call,access control policy,space analysis,formal analysis,formal verification,state transition system,model checking,ctl,access control,satisfiability,computation tree logic
Computation tree logic,Transition system,Permission,Model checking,Computer science,Role-based access control,Theoretical computer science,Access control,Formal verification,Liveness
Conference
Citations 
PageRank 
References 
16
0.65
21
Authors
3
Name
Order
Citations
PageRank
Samrat Mondal110018.02
Shamik Sural2100896.36
Vijayalakshmi Atluri33256424.98