@article{967,
  author = {Emsaieb Geepalla, Behzad Bordbar},
  title = {An Automated Approach to Detect Inconsistency and Semi-consistency Spatio-Temporal Role Based Access Control Specification},
  journal = {Journal of Data Processing},
  year = {2012},
  volume = {2},
  number = {3},
  doi = {},
  url = {http://www.dline.info/jdp/fulltext/v2n3/4.pdf},
  abstract = {In the last decade, researchers have developed a number of RBAC extensions such as Spatio-Temporal Role Based Access Control (STRBAC) that takes into consideration the location of users and the time of access. These models that incorporate time and location information into the basic model RBAC are mainly proposed to support 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. In this study, we 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 formal algebraic notations 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 semiconsistency is a special case where the inconsistency can be avoided if the assignment of user to role is controlled. Finally, the paper presents an eclipse application called AC2Alloy that transforms STRBAC specification into Alloy. The produced Alloy models can be analysed using Alloy Analyser 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.},
}