Formalisation of access control based on observers automata Online publication date: Tue, 06-Jul-2021
by Mohammed Walid Krakallah; Safia Nait-Bahloul
International Journal of System of Systems Engineering (IJSSE), Vol. 11, No. 2, 2021
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of System of Systems Engineering (IJSSE):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook