Welcome to the InfoSci Platform
Reference Hub2
A Valid and Correct-by-Construction Formal Specification of RBAC

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

Hania Gadouche, Zoubeyr Farah, Abdelkamel Tari
Copyright: © 2020 |Volume: 14 |Issue: 2 |Pages: 21
ISSN: 1930-1650|EISSN: 1930-1669|EISBN13: 9781799805366|DOI: 10.4018/IJISP.2020040103
Cite Article Cite Article

MLA

Gadouche, Hania, et al. "A Valid and Correct-by-Construction Formal Specification of RBAC." IJISP vol.14, no.2 2020: pp.41-61. http://doi.org/10.4018/IJISP.2020040103

APA

Gadouche, H., Farah, Z., & Tari, A. (2020). A Valid and Correct-by-Construction Formal Specification of RBAC. International Journal of Information Security and Privacy (IJISP), 14(2), 41-61. http://doi.org/10.4018/IJISP.2020040103

Chicago

Gadouche, Hania, Zoubeyr Farah, and Abdelkamel Tari. "A Valid and Correct-by-Construction Formal Specification of RBAC," International Journal of Information Security and Privacy (IJISP) 14, no.2: 41-61. http://doi.org/10.4018/IJISP.2020040103

Export Reference

Mendeley
Favorite Full-Issue Download

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.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.