Abstract
Security analysis of access control models is critical to confirm whether they ensure certain security properties. Administrative models specify the rules for state transition for any given access control model. While security analysis of role-based access control (RBAC) systems has been done using administrative models, work on security analysis of its temporal, spatial and spatio-temporal extensions has so far not considered the presence of any corresponding administrative model. In this paper, we present a methodology for performing security analysis of temporal RBAC (TRBAC) where state changes occur using the relations defined in a recently proposed administrative model named as AMTRAC (Administrative Model for Temporal Role-based Access Control). We initially define a number of security properties for TRBAC. These properties along with a representation of the TRBAC system and the administrative relations in AMTRAC are then formally specified using Alloy, a first order logic based language. Subsequently, validity of the specified properties is analyzed using the Alloy analyzer. We study the impact of the number of roles, users and temporal elements of TRBAC as well as various relations defined in AMTRAC on the time taken for security analysis.
•Security analysis of TRBAC in the presence of an administrative model is introduced.•Alloy is used for specifying TRBAC, its administrative model as well as the security properties.•Validity of the desired security properties is tested with the help of Alloy analyzer.•Results of extensive experiments have been presented.