Spatio Temporal Access Control for Cyber-Physical Systems
Cyber-physical systems require access control mechanisms which take into consideration the location of users and the time of access. As adding extra information about the location and time increases the complexity of the specification of access control, in [1] we presented a formal approach to modelling and analysis of access control based on a popular model (STRBAC) developed by our co-authors. We have recently developed a tool AC2Alloy [2] for detecting inconsistencies in such models [3] via Alloy so that better access control specifications can be produced. To improve the analysis capability of AC2Alloy so that to deal with temporal logic statements, we have further extended the tool to use Timed Automata and UPPALL model checker. This research project is in collaboration with Indrakshi Ray and her colleagues at Colorado State University.
The model in [1]
is now extended to deal with physical access control and AC2Alloy is
used for the analysis of the specifications of physical access
control to sensitive areas and buildings in collaboration with BT.
Selected publications
-
Ensuring Spatio-Temporal Access Control for Real-World Applications, M. Toahchoodee, I. Ray, K. Anastasakis, G. Georg and B. Bordbar, Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, Stresa, Italy, June 2009.
-
Transformation of Spatio-Temporal Role Based Access Control Speci cation to Al-
loy, E. Geepalla, B. Bordbar and J. Last. Published in the 2nd International Con-
ference on Model and Data Engineering (MEDI2012). -
An Automated Approach to Detect Inconsistency and Semi-consistency Spatio-
Temporal Role Based Access Control Speci cation. E. Geepalla and B. Bordbar.
Journal of Data Processing, Vol 2., September 2012.
