Security Analysis of RBAC with Temporal Constraints - A Model Checking Approach

Role Based Access Control (RBAC) is a well accepted access control mechanism for various applications such as database management systems, operating systems, etc. The traditional RBAC models, however, cannot handle the time varying nature of access control policies. Temporal RBAC (TRBAC) has been developed on top of the RBAC model to incorporate various temporal constraints. In this paper, a security analysis framework is proposed for TRBAC. For this purpose timed automata based model checking approach is suggested. A timed automaton is a state transition system with real valued clocks. Each role of a TRBAC system is modeled using a timed automaton. Temporal constraints on role enabling and disabling are specified in a separate automaton, known as the controller automaton. The timed automaton is constructed in such a way that it can handle role trigger, an important feature of TRBAC. The desirable security properties are specified using Computation Tree Logic (CTL) and verified against the proposed model. We have specifically considered safety and liveness properties to show the usefulness of our approach.