Title: Formalisation of access control based on observers automata

Authors: Mohammed Walid Krakallah; Safia Nait-Bahloul

Addresses: Laboratory of Pure and Applied Mathematics, Department of Computing and Mathematics, University of Abdelhamid Ibn Badis – Mostaganem, Mostaganem, 27000, Algeria ' LITIO Laboratory, University Oran1, Ahmed Ben Bella, BP 1524, El-M'Naouer, Oran, Algeria

Abstract: The modelling of access control (AC) policies aim to describe aspects of different security requirements at a higher level of abstraction. Once the AC policy has been modelled, the difficulty lies in the expression and formal verification of the properties of this policy. This paper proposes to develop a formal framework for the specification and validation of the hybrid AC policy. In order to increase the flexibility of AC, an extension of the UACML model to the emergency RBAC model (E-RBAC) is proposed. We start with the semiformal specification of AC rules using activity diagrams that we call E-UACML accompanied by AC constraints and spatio-temporal constraints. E-UACML is then translated into a formal specification expressed in the Fiacre language and the requirements in observer automata using the CDL language. The latter is used to formally verify the properties with OBP (model checking). We evaluate our approach with a case study.

Keywords: access control; observer automata; UML; unified modelling language; Fiacre; OBP/CDL; formal methods; model checking.

DOI: 10.1504/IJSSE.2021.116045

International Journal of System of Systems Engineering, 2021 Vol.11 No.2, pp.170 - 197

Received: 24 Mar 2020
Accepted: 31 Aug 2020
Published online: 06 Jul 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article