Towards formal security analysis of GTRBAC using timed automata

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

• Type: Conference
• Year: 2009
• Where: SACMAT
• Authors: Samrat Mondal, Shamik Sural, Vijayalakshmi Atluri
• Keywords: Access Controls, SACMAT 2009, Security Privacy, State Transition System, Timed Automata