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

fYear

2014

fDate

April 29 2014-May 1 2014

Firstpage

16

Lastpage

21

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/CyberSec.2014.6913965

Filename

6913965