On the formal analysis of a spatio-temporal role-based access control model

With the growing use of wireless networks and mobile devices, we are moving towards an era where spatial and temporal information will be necessary for access control. The use of such information can be used for enhancing the security of an application, and it can also be exploited to launch attacks. For critical applications, a model for spatio-temporal-based access control is needed that increases the security of the application and ensures that the location information cannot be exploited to cause harm. Consequently, researchers have proposed various spatio-temporal access control models that are useful in pervasive computing applications. Such models typically have numerous different features to support the various application requirements. The different features of a spatio-temporal access control model may interact in subtle ways resulting in conflicts. We illustrate how the access control model can be formally analyzed to detect the presence of conflicts. We use Alloy, a formal language based on first-order logic, for the purpose of our analysis. Alloy is supported by a software infrastructure that allows automated analysis of models and has been used to verify industrial applications. The results obtained by analyzing the spatio-temporal access control model will enable the users of the model to make informed decisions.