Title :
Comparison between Alloy and Timed Automata for modelling and analysing of access control specifications
Author :
Geepalla, Emsaieb
Author_Institution :
Sch. of Electr. & Comput. Eng., Sebha Univ., Brak Ashati, Libya
fDate :
April 29 2014-May 1 2014
Abstract :
This paper presents a comparative study between Alloy and Timed Automata for modelling and analysing of access control specifications. In particular, this paper compares Alloy and Timed Automata for modelling and analysing of Access Control specifications in the context of Spatio-Temporal Role Based Access Control (STRBAC) from capability and performance points of view. To conduct the comparison study the same case study (SECURE bank system) is specified using Alloy and Timed Automata. In order to transform the specification of the Secure Bank system into Alloy and Timed Automata this paper makes use of our earlier methods AC2Alloy and AC2Uppaal respectively. The paper then identifies the most important advantages and disadvantages of Alloy and Timed Automata for modelling and analysing of access control specifications.
Keywords :
authorisation; automata theory; bank data processing; directed graphs; formal specification; AC2Alloy method; AC2Uppaal method; SECURE bank system; STRBAC; access control specification analysis; access control specification modelling; directed graph; spatio-temporal role based access control; timed automata; Access control; Analytical models; Automata; Clocks; Computational modeling; Metals; Object oriented modeling;
Conference_Titel :
Cyber Security, Cyber Warfare and Digital Forensic (CyberSec), 2014 Third International Conference on
Conference_Location :
Beirut
Print_ISBN :
978-1-4799-3905-3
DOI :
10.1109/CyberSec.2014.6913965
