Rigorous Analysis of Temporal Access Control Properties in Mobile Systems

Access control models must be analyzed to uncover flaws that can be exploited to gain unauthorized access. The UML has been used to describe access control models and there are a number of proposed approaches for analyzing UML access control models. Practical support for checking UML access control models against temporal properties is still lacking. In this paper, we describe a lightweight approach to analyzing a UML model of security policies against linear temporal properties. The access control policies are based on a generalized spatio-temporal role-based access control (GSTRBAC) model. We use a demonstration case study to show how the approach can be used to uncover access control problems.