A Valid And Correct-By-Construction Formal Specification Of Rbac

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.