Abstract
Temporal Role Based Access Control (TRBAC) is an extension of the role based access control (RBAC) model in the temporal domain. It is used by organizations needing to enforce temporal constraints on enabling and disabling of roles. For any chosen access control model, decentralization of administrative authority necessitates the use of a separate administrative model. Even with the use of an administrative model, decentralization often leads to an increased concern for security. Analysis of security properties of RBAC has been extensively done using its administrative model (ARBAC97). However, TRBAC security analysis in the presence of an administrative model so far has received limited attention. This paper proposes a method for performing formal security analysis of TRBAC considering a recently proposed administrative model named AMTRAC, which includes all the relations of ARBAC97 as well as an additional set of relations (named REBA) for administering the role enabling base of a TRBAC system. All the components of TRBAC and AMTRAC are specified in Prolog along with the desired safety and liveness properties. Initially, these properties are verified considering the non-temporal relations only, followed by handling of the temporal relations as well. Experimental results show that the method is both effective as well as scalable.