Verification of Spatio-Temporal Role Based Access Control using Timed Automata

The verification of Spatio-Temporal Role Based Access Control policies (STRBAC) during the early development life cycle improves the security of the software. It helps to identify inconsistencies in the Access Control policies before proceeding to other phases where the cost of fixing defects is augmented. This paper proposes a formal method for an automatic analysis of STRBAC policies. It ensures that the policies are consistent and conflict-free. The method proposed in this paper makes the use of Timed Automata to verify the STRBAC policies. This is done by translating the STRBAC model into Timed Automata, and then the produced Timed Automata is implemented and verified using the model checker UPPAAL. This paper presents a security query expressed using TCTL to detect inconsistency caused due to the interaction between STRBAC policies. With the help of an example, this paper shows how we convert STRBAC model to Timed Automata models and verify the resulting models using the UPPAAL to identify an erroneous design.