On formalizing of inconsistency and semi-consistency in spatio-temporal access control

Incorporating the Role-Based Access Control (RBAC) model with the spatial and the temporal information cater for the needs of many mobile applications and wireless networks. However by doing so, it further increases the complexity of an already complex Access Control model. As a result, this increases the possibility of having contradictory statements in the Access Control specification. Such statements are commonly known as inconsistencies. One of the aims of this paper is to provide a formal definition of inconsistency in Spatio-Temporal Role Based Access Control (STRBAC) and then define several examples of inconsistencies in STRBAC specification. To achieve this, we shall first present a Relational Semantics of STRBAC model. In addition, the paper introduces the concept of “semi-consistency” in STRBAC and presents several scenarios that are involving semi-consistencies. A semi-consistency is a special case where the inconsistency can be avoided if the assignment of user to role is controlled. Finally, the paper presents a tool called AC2Alloy that transforms STRBAC specification to Alloy in order to detect inconsistencies and semi-consistencies in the STRBAC specification. With the help of an example, we show how AC2Alloy converts the STRBAC model to the Alloy model and verifies the resulting model using the Alloy analyser to identify inconsistencies and semi-consistencies.