A Valid and Correct-by-Construction Formal Specification of RBAC

Hania Gadouche, Zoubeyr Farah and Abdelkamel Tari
Additional contact information
Hania Gadouche: LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria
Zoubeyr Farah: LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria
Abdelkamel Tari: LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria

International Journal of Information Security and Privacy (IJISP), 2020, vol. 14, issue 2, 41-61

Abstract: Controlling access to data is one of the primary purposes of security, especially when it comes to dealing with safety critical systems. In such systems, it is of paramount importance to rigorously define access control models. In this article, a correct-by-construction specification of RBAC using the Event-B formal method is proposed. The specification defines closely the model properties with the behavior aspect of RBAC as guards of events, which allows applying a priori verifications. Accordingly, the resulted specification is correct-by-construction and avoids the combinatorial explosion problem. As well, a number of refinement operations are performed leading to a specification with several abstraction levels, where each level implements selected RBAC entities. The approach is illustrated by an instantiation of a healthcare system.

Date: 2020
References: Add references at CitEc
Citations:

Downloads: (external link)
http://services.igi-global.com/resolvedoi/resolve. ... 018/IJISP.2020040103 (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:igg:jisp00:v:14:y:2020:i:2:p:41-61

Access Statistics for this article

International Journal of Information Security and Privacy (IJISP) is currently edited by Yassine Maleh

More articles in International Journal of Information Security and Privacy (IJISP) from IGI Global
Bibliographic data for series maintained by Journal Editor ().