1 Introduction

In safety-critical systems, serious vulnerabilities can result from incorrect access definition to sensitive data. Access control policies (ACP) are a common solution for controlling access to resources. Hence, several access control models have been proposed in the literature [10, 18, 21, 26], namely the mandatory access control (MAC), the discretionary access control (DAC), the role based access control (RBAC) and the attribute based access control (ABAC). Each access model has been designed to meet specific security requirements. Moreover, research on the MAC, DAC, RBAC and ABAC has proven that an access control model, which can express the RBAC policies is also capable of enforcing both MAC and DAC policies, as long as ABAC can express RBAC policies. The ABAC model improves RBAC since it enables fine-grained access control by defining the notion of attributes. The additional use of attributes when defining access control rules may enforce the met shortcomings and make the handled objects more reachable in a secured way.

Validating and ensuring correctness of ACP specifications generally involve the use of systematic verification [11] which consists of checking absence of inconsistency and incompleteness in the built model. Regardless of used formalism, many specification and verification approaches are based on testing, simulation or model checking. These latter implement an a posteriori verification techniques [7] but are generally restricted to the following limitations:

  • The state-space explosion problem,

  • The checking is performed when the model instantiation is achieved.

Most of the existing literature approaches have used the eXtensible Access Control Markup Language (XACML) [4] which is a standard for specifying ABAC policies. XACML as a practical standard of OASIS has been covered in many testing and verification researches. However, these testing and verification methods are limited by the XACML complexity. To overcome this, we propose by construction, an Event-B based approach to build a valid ABAC model free from specification inconsistencies and errors. Specification approaches that are based on formal methods, such as Event-B [1], are widely used to model faultless critical systems. The use of formal methods requires understanding the system behavior and the relations between its components. Several works in the literature have used the Event-B method to specify the RBAC standard [13], but to the best of our knowledge, no work has addressed ABAC using the Event-B method.

We use the Event-B formal method, since it allows the specification of systems according to a correct-by-construction methodology, additionally, it provides a large selection of tools and techniques for specifying, validating and checking properties of systems. The proposed specification approach is based on refinement and gives a multilevel view of the access control model. The refinement starts from a high abstract level of specification to the most concrete one. The specification consistency is preserved through all its levels as the model properties are linked to the behavior. Indeed, defining properties of the model according to its behavior allows to get an a priori verification of the specification correctness. Thus, our approach is based on an a priori formal verification process, similarly to the one proposed to validate communicating systems in [5, 6]. When the model is instantiated, all proved properties of the generic model remain valid thanks to the correct-by-construction approach. RODIN platform [2] is used to develop and validate the model.

The key features of our proposal are as follows :

  • The approach is progressive and based on proving refinement, accordingly it avoids the combinatorial explosion.

  • The behavior and properties of the model are correctly specified following a correct-by-construction approach, consequently the consistency of the specification is proved in its overall refinement levels.

  • The approach allows specific views of the model rather than a global integrated one which simplifies the model analysis.

The remainder of the paper is organized as follows: Sect. 2 gives a presentation of the ABAC standard. Section 3 describes the Event-B formal method. Section 4 gives a browse of each level of the proposed Event-B specification approach. Section 5 details the generated Proof obligations of the model. An illustration of the specified model for web-based healthcare services is given in Sect. 6. Related works are discussed in Sect. 7. Finally, the conclusion and some research perspectives are given in Sect. 8.

2 Attribute-based access control

In this section, an overview of ABAC is given. In the special publication [9] the NIST gives the following official definition of ABAC: An access control method where subject requests to perform operations on objects are granted or denied based on assigned attributes of the subject, assigned attributes of the object, environment conditions, and a set of policies that are specified in terms of those attributes and conditions. Accordingly, we identify the following components for ABAC (Fig. 1):

  • Policy: is a set of rules that determine if a requested access should be allowed, given the values of the attributes of the subject, object, and probably environment conditions or other constraints. A policy is created and owned by the resource administrator and plays a crucial role in the operation of ABAC.

  • Subjects: is a set of entities requesting to perform actions upon objects. Subjects are characterized by a set of attributes.

  • Objects: is a set of services or system resources, such as devices, files, records, tables, processes, programs, networks . . . etc. Objects are the entities to be protected from unauthorized use. The objects attributes are provided by their owners.

  • Permissions: known as authorizations or access rights. A permission consists of granting rights to a subject request on an object according to policy rules.

  • Attributes: are characteristics of subjects, objects, or environment conditions. Attributes allow administrators to apply access control policies for unlimited number of subjects that might require access without prior knowledge of them. Thus, new subjects can join the system without modifying the rules and objects. Each attribute can be either atomic or set of values.

  • Environmental conditions: consist of the situation context in which access requests to objects are formulated. Environmental conditions are characterized by a set of attributes.

Fig. 1
figure 1

ABAC basic architecture

Full size image

3 Event-B method

Event-B is a formal method used to model and analyze systems. An Event-B development model [1] is based on components of two kinds: Contexts and Machines. Contexts contain the static parts (axiomatization and theories) of the model, whereas the Machines implement the dynamic parts (states and transitions). Machines and contexts have various relations: a machine can be refined by another one, and a context can be extended by another one. Moreover, a machine can see one or several contexts. A Context is defined by a set of clauses as follows:

  • CONTEXT represents the name of the component that should be unique in a model.

  • EXTENDS declares the Context(s) extended by the described Context.

  • SETS describes a set of abstract and enumerated types.

  • CONSTANTS represents the constants used by a model.

  • AXIOMS describes, in first-order logic expressions, the properties of the defined elements in the CONSTANTS and SETS clauses. Types and constraints are described in this clause as well.

  • THEOREMS are logical expressions that can be deduced from the axioms.

Similarly to Contexts, Machines are defined by a set of clauses:

  • MACHINE represents the unique name of the component in an Event-B model.

  • REFINES declares the Machine that is refined by the described Machine.

  • SEES gives the list of Contexts imported by the described Machine.

  • VARIABLES represents the state variables of the model. Refinement may introduce new variables in order to enrich the described system.

  • INVARIANTS describes, using first-order logic expressions, the properties of the variables defined in the VARIABLES clause. Typing information, functional and safety properties are usually described in this clause. These properties must remain true in the whole model. Invariants need to be preserved by events. It also expresses the gluing invariant required by each refinement.

  • THEOREMS defines a set of logical expressions that can be deduced from the invariants.

  • VARIANT introduces a natural number or a finite set that the convergent events must strictly make smaller at every execution.

The general structure of an Event-B development is illustrated in the Table 1, where s denotes sets, c denotes constants and v denotes the declared variables of the machine. Axioms are denoted by \(A\left( s,c\right) \) and theorems by \(T\left( s,c \right) \) , whereas invariants are denoted by \(I\left( s,c,v \right) \) and local theorems by \(T\left( s,c,v \right) \). For an event evt, its guards are denoted by \(G\left( s,c,v,x \right) \) and its actions by the before-after predicate \(BA\left( s,c,v,x,v^{'} \right) \).

Table 1 Structure of an Event-B development
Full size table

The EVENTS clause defines a list of events (transitions) that can occur in a given model. Each event is characterized by its guards and is described by a set of actions (substitutions). Each machine must contain an initialization event. The events occurring in an Event-B model affect the state described in clause. An event consists of the following clauses:

  • Refines: declares a list of events refined by the described event.

  • Any: lists a set of the event parameters.

  • Where: expresses a set of guards for the event. An event can be fired when its guard turns to true. If several guards of events become true, only a single event is fired.

  • Then: contains a set of actions of the event that are used to modify variables.

Event-B is based on a refinement methodology, it allows the system developer to start with an abstract model of the system considering its context, and gradually add details to the model. This process leads to a sequence of concrete models until the final implementation is reached. A number of proof obligations are generated through this process, which guarantees the correctness of the model as well as any desired invariants (properties) that the model should preserve. Proof obligations can then be proved by automatic or interactive theorem provers or model-checking tools and the model itself can be simulated in runtime. Proving obligations, checking invariants and model simulating are functions that are supported by tools such as ProB [17] which is available in RODIN platform. The latter, made for the Rodin project, supplies a set of tools to support Event-B development. It also provides effective support for refinement and mathematical proofs.

4 Event-B specification of ABAC

Fig. 2
figure 2

Event-B structure of ABAC

Full size image

The proposed ABAC specification is detailed in this section. In the suggested approach, properties of the model are given in conjunction with the behavior specification. The model is developed in a way to link up between behavior and properties of ABAC components. We define a correct-by-construction approach following an a priori verification. Consequently, the validity and the correctness of the ABAC model are guaranteed through the specification steps. The developed Event-B model contains a context that forms the static part of the specification, an application context for the instantiation of ABAC components values, and five machines that form the dynamic part. Each machine expresses a level of the ABAC properties specification. Figure 2 gives the structure of the proposed Event-B model. We extend the Basic ABAC by introducing authentication and purpose of access. The authentication consists of providing credentials to a set of subjects to verify their authorization to use the requested data. The purpose is the reason that makes the subject requesting access to a specific service. If the purpose do not match with the privacy level of a resource or a service, the subject will not be authorized to access it. TheABAC_Abstract_Level machine gives the general authorization structure to be provided by the access model. The subjects and the requested services are introduced in the ABAC_Components_Level which refines theABAC_Abstract_Level. Attributes of subjects and requested services are introduced in the ABAC_Attributes_Level in order to decide the appropriate privileges to assign since access decisions are granted based on attribute values, their level of privacy and the purpose of requesting access to the services. The access rules, defined in the ABAC_Rules_Level, manage access to resources and the authorized privileges to act on a resource according to ABAC entities attributes (subjects, services, environment conditions,. . . etc.) We detail each specification level in the following:

  • ABAC_Context: The basic elements of ABAC are introduced in the static part of the specification. These elements are reported in the CONTEXT named ABAC_Context. All the required static definitions to operate the dynamic part of the model are declared in this context(see Table 2). In ABAC_Context , the declared working sets are: SUBJECTS, SERVICES, attributes of subjects(ATTR_SUBJECTS ), attributes of services (ATTR_SERVICES),system environment conditions (ENV_COND) and PRIVILEGES of the access model. The required conditions when defining these sets are stated as axioms: The sets must be finite and not empty.

  • ABAC_Context_Application: where are defined the values of ABAC entities to be instantiated to generate a set of licit traces that correspond to the fired events of the model.

  • ABAC_Abstract_Level: The dynamic specification starts with a level that gives a global and high view of ABAC. It is expressed by the machine \(Abstract\_Level\) as depicted in the Table 3. The considered properties in this level are about the typing of authorizations and the definition of relationships between the ABAC components. Authorizations are manipulated in the event \(Abstract\_Usage\) that generates abstract view of the access model. To preserve the abstraction, non-deterministic assignment \((:\in )\) is used. This affectation will gradually be determined in the refinement process.

    In this level, details are not important, the ABAC structure has just to be in a brief and perceivable view. The ABAC policy is expressed by the variable Authorizations.

  • ABAC_Components_Level: This level provides more precision on the subjects and the requested services. Subjects and Services are introduced in the model in the events depicted in the Table 4. The subjects and the services involved in the authorization are precised in this level by the refinement of the event Abstract_Usage as depicted in the Table 5.

  • ABAC_Attributes_Level: The key feature of ABAC is the use of attributes to decide the suitable authorizations to grant. In this level, subject and service attributes are introduced to define the rules composing the concrete authorizations in the next refinement level. Attributes of subjects are introduced by refining the event \(Set\_Subjects\) in the event \(Set\_Subject\_Attributes\) as depicted in the Table 6. In the refinement of the \(Set\_Subjects\) event, a witness relation is used to ensure that every Subject is given its own attributes. In the same way, the event \(Set\_Services\) is refined in \(Set\_Service\_Attributes\).

    To preserve consistency between the introduction of subjects and services attributes, some invariants are given in the Table 7.

    To specify the authentication process, a subject is given credentials with the event \(Set\_Subject\_Credentials\), depicted in the Table 8.

  • ABAC_Rules_Level: In this level, the defined rules are used to concretize the authorizations variable. A rule matches attributes of subjects to requested services attributes, as well as the system environment attributes, to establish a privilege assignment. The event \(Set \_Rules\) is given in the Table 9. To preserve consistency between the subjects and services attributes and their definition in the context of a rule, three invariants are added (see Table 10). The set of \(Authenticated\_Subjects\) is defined in the event of Table 11.

  • ABAC_Access_Decision_Level: In this level, the purpose of access to a service is defined. In order to strengthen the ABAC access control mechanism, authorizations are granted considering the purpose and the privacy level of each service data, defined in the events \(Service\_Use\_Purpose\) and \(Set\_Privacy\_Level\), detailed in Tables 12 and 13 respectively.

    In the Table 14 is detailed the final concrete \(Access\_Decision\) event which involves a set of attributes of an authenticated subject, authorized to access a service in some environments conditions and privileges defined in rules, for a specific purpose and with the respect of the privacy level of the service data.

Table 2 ABAC_Context
Full size table
Table 3 ABAC_Abstract_Level machine
Full size table
Table 4 Set_Subjects and Set_Services event
Full size table
Table 5 Refinement of the Abstract_Usage event
Full size table
Table 6 Set_Subjects and Set_Services Attributes event
Full size table
Table 7 Invariants of the ABAC_Attributes_Level
Full size table
Table 8 Set_Subjects_Credentials event
Full size table
Table 9 Set_Rules event
Full size table
Table 10 Invariants of ABAC_Rules_Level
Full size table
Table 11 Set_Authenticated_Subjects event
Full size table
Table 12 Service_Use_Purpose event
Full size table
Table 13 Set_Privacy_Level event
Full size table
Table 14 The Access_Decision event
Full size table

5 Proof obligations

The initial Event-B model presented above has been developed within the Rodin platform. This latter generates automatically Proof Obligations (POs) in the form of sequences [1]. The automatic Prover of RODIN can discharge automatically many of the POs, the remainder of non-discharged POs can be tackled by the interactive Prover. The developed model led to 39 proof obligations: 12 were proved automatically (APO) and 17 needed few interactive proof steps(IPO). Table 15 details the statistic proofs of the initial model. The adopted specification approach engendered a reduced number of POs since the properties of the ABAC were expressed with the model behavior as events properties (guards). Accordingly, many POs were automatically proved.

Table 15 Statistic of proofs
Full size table

6 Instantiation of the model: healthcare web services

Fig. 3
figure 3

ABAC architecture for Web-based healhcare services

Full size image

Web services are software components that support interaction between heterogeneous systems and networks. Flexible and easy to access, they are widely used in the medical field, to simplify to patients and health professionals the access and manipulation of data. Since the sensitive handled data requires rigorous access control definition, we illustrate the proposed approach for healthcare web services. Figure 3 shows the proposed ABAC architecture for healthcare service. The goal is to make and grant access decisions to subjects to medical services and patients’ data. The request can be sent through a web application or a browser. In this paper, we deal only with the specification and validation of the access model correctness before any implementation.

The first step is the authentication of the subject using its credentials. Once authenticated, he requests access to a healthcare service precising the needed data and the purpose of using it. The Policy Enforcement Point, an ABAC module, receives the access requests and send them to the Policy Decision Point, where all the access decisions are made, by retrieving the attributes of subjects, services and environment conditions and the rules that define the privileges of each subject attributes.

The \(ABAC\_Context\_Application\) sets are defined as follows:

  • \(SUBJECTS=\{Patient, Doctor,Nurse, Physician\_pathologist, Radiologist\}\).

  • \(SERVICES =\{Patient\_ManageSys, Laboratory\_Analysis ,Hospital\_Administration, Remote\_Imaging\}\).

  • \(ATTR\_SUBJECTS =\{ID\_number,Name, Birthdate, Address, Department\}\).

  • \(ATTR\_SERVICES =\{Patient\_data, Patient\_MRI\_scan, Patient\_blood\_test, Patient\_allergic\_test\}\).

  • \(EN\_COND =\{Hospital\_name, Hospital\_location,Hospital\_department, Network\}\).

  • \(PRIVILEGES =\{Search, Register, Read, Modify, Delete, Upload, Download\}\).

  • \(ACCESS\_PURPOSES=\{Registration, Personal, Routine\_CheckUp, Surgery, Medicine\_Prescription, Scientific\_research\}\).

  • \(PRIVACY\_LEVELS=\{Private,Public\}\).

  • \(CREDENTIALS=\{c1,c2\}\).

Given the ABAC component values, we consider the following scenario:

  • \(\bullet subject = ``Patient''\)

  • identified by \(subject\_attribute=``ID\_number''\)

  • Having the authentication \(credential=``c1''\)

Requests access to:

  • \(service=``Patient\_ManageSys''\)

  • \(service\_attribute=``Patient\_data''\)

  • in \(env\_cond =``Hospital\_name''\)

  • having the \(privilege= ``Read''\)

  • \(\bullet subject = ``Radiologist''\)

  • identified by \(subject\_attribute=``Department''\)

  • Having the authentication \(credential=``c2''\)

Requests access to:

  • \(service=``Remote\_Imaging''\)

  • \(service\_attribute=``Patient\_MRI\_scan''\)

  • in \(env\_cond =``Hospital\_Department''\)

  • having the \(privilege= ``Download''\)

  • ABAC_Components_Level:

    In the first level, the sets of Subjects and Services are defined as :

    \(Subjects =\{Patient,Radiologist\}\).

    \(Services= \{Patient\_ManageSys, Remote\_Imaging\}\).

  • ABAC_Attributes_Level:

    In the second level, the attributes are added to Subjects and Services:

    \(Subject\_Attributes=\{(Patient \mapsto ID\_number), (Radiologist \mapsto Department)\}\).

    \(Service\_Attributes=\{ (Remote\_Imaging \mapsto Patient\_MRI\_scan),(Patient\_ManageSys \mapsto Patient\_data) \}\).

    The subjects are assigned specific credentials for further authentication :

    \(Subjects\_Credentials =\{(Patient\mapsto c1), (Radiologist \mapsto c2)\}\).

  • ABAC_Rules_Level:

    Before any access request, a subject must be authenticated. The set of authenticated subjects is used when defining the final access decision.

    \(Authenticated\_Subjects= \{Patient,Radiologist\}\) .

    For each service data, we define a privacy level.

    \(Service\_Privacy\_Level= \{(Patient\_ManageSys\mapsto Patient\_data \mapsto Private), (Remote\_Imaging \mapsto Patient\_MRI\_scan \mapsto Private)\}\).

    The rules define the access policies that combine the subject, the requested service, the environment condition and the privilege.

    \(Rules= \{(Patient \mapsto ID\_number \mapsto Patient\_ManageSys \mapsto Patient\_data \mapsto Hospital\_name \mapsto Read), (Radiologist \mapsto Department \mapsto Patient\_MRI\_scan \mapsto Hospital\_Department \mapsto Upload)\}\).

  • ABAC_Access_Decision_Level:

    For requesting access to the \(Remote\_Imaging\) service, the Radiologist must precise the purpose, for example, for scientific research purpose to be authorized to download the \(Patient\_MRI\_scan\).

    \(Access\_Purpose= \{(Patient\_ManageSys \mapsto Personal), Remote\_Imaging \mapsto Scientific\_Research)\}\).

    The authorizations are defined and the final access decision is made as follows: The Patient can access the \(Patient\_ManageSys\) to Read \(Patient\_data\) precising the \(Hospital\_name\).

    \(Authorizations=\{(Patient \mapsto Patient\_ManageSys \mapsto Hospital\_name \mapsto Read), (Radiologist \mapsto Remote\_Imaging \mapsto Hospital\_Department \mapsto Upload\}.\)

    \(Access\_Decision = \{(Patient \mapsto Patient\_ManageSys \mapsto Personal), (Radiologist \mapsto Remote\_Imaging \mapsto Scientific\_Research)\}\).

7 Related works

Several approaches in the literature address the ABAC model specification and verification; most of them have used XACML. A work that addresses the logic programming is presented in [25], where a stratified framework for ABAC is defined based on computable and hereditarily set theory to represent policies making them consistent, complete and transformable to perform faster runtimes.

The authors in [27] present a model-checking algorithm for the access control policies evaluation. It consists of ensuring that the authorized users are granted enough permissions to achieve their goal, also, to avoid the achievement of malicious goals from unauthorized users. The algorithm consists of two modes: the assessing mode and the intrusion detection mode.

In [12] the authors define a formal model to specify access to resources using XACML. Their approach define access control properties in many ordering relations and translate them into Boolean satisfiability problems. To grant access decisions and verify automatically the access control properties, the authors used the SAT solver. However, they admit that their approach has some limitations in terms of correctness of the access decisions issued from the Boolean problems.

The authors in [19] propose an approach based on mutation for the assessment of policy properties quality and its verification. A policy mutate into several variants called mutant policies with a single fault for each one. The verification process identifies the fault of the mutant policy when properties are not preserved.

Authors in [8] investigate a two-step approach to validate a non-specific ACP using Event-B. The first step constructs the secured system from combining the unsecured system and the desired security. The second step performs a verification on the resulting combined system against safety temporal properties. The combination is based on many levels of abstraction and refinement where each level expresses a class of properties. For illustration, they apply the approach on a banking system. Although the specification of the two parts of the system is done by design, the combination step includes a verification process to ensure absence of combining specification errors.

Shu et al. [23] define a method to efficiently detect the conflicts in ABAC policies using the formal notions of semantically equivalent policies and statically conflicting rules. The proposed method is based on two optimization techniques: the first technique reduces the semantically equivalent rules into a set of compact, then the binary-research technique is applied to detect conflicts in the set of the reduced rules.

In [14] the authors develop a tool named Access Control Policy Testing (ACPT) for the correct modeling, implementation and verification of XACML access control policies. The developed tool supports both of the static and the dynamic verification in order to decrease policies faults.

Authors in [16] present an abstraction-refinement-based approach to verify ACP. The principle is to define a bounded model-checker by computing an approximate size of the policy to be verified, then, fix a bound of checking operations to perform where any error can be detected. This allows to reduce verification complexity since the access errors research is not exhaustive. They demonstrate that the proposed approach scales better when input policies increase in size. They apply their approach on ARBAC model, which is a variant of ABAC. Although this technique scales well, the detection of all possible errors is not always assured and the correctness of the specification model is not fully guaranteed.

Authors in [22] propose a cloud-based Electronic-Health Record System based on ABAC with XML encryption and digital signature to guarantee the privacy of the patient data.

In [3] is proposed an Event-B approach for Data Integration Systems design using RBAC and formal methods.The approach considers trust and privacy properties for the specification. The consistency and correctness of the model are verified with model-checking.

The authors in [24] define an approach to design privacy-aware healthcare web services. They use encryption to preserve the data privacy but do not consider the authentication process and the access control policies.

Méry et al. [20] propose a refinement based approach for designing high-confidence medical devices. They use model checking for the validation and verification of the approach and illustrate it in a cardiac pacemaker system.

In [15], a specification platform (B4MSecure) is proposed to model access control policies. The defined tool translates SecureUML diagrams into Event-B specifications to validate and verify the behavioral security features of the model.

Most of the specification and verification of ABAC models follow an a posteriori verification technique. Whether it is testing, simulation or model-checking based, the use of the a posteriori verification becomes inappropriate when the access model increases in size and functionality. Indeed, testing techniques can be performed when an implementation of the model is available, furthermore, they can only be used to prove the existence of some specific errors, for the simulation and model-checking techniques they are limited by the state explosion problem. In this paper, a correct-by- construction specification approach is proposed to overcome the aforementioned limitations. Indeed, unlike existing approaches defined to specify and validate ABAC models, the correctness of the model behavior is ensured by proofs during the specification steps, which means that we define an a priori approach to specify a correct behavior in a stepwise manner. Additionally, we adopt a specification methodology where ABAC components are progressively introduced by refinement. Consequently, the specification process is simplified and will not be affected when the system scales in size and functionality.

8 Conclusion

In this paper an Event-B formal specification approach for ABAC is presented. Due to the limitation of the a a posteriori based specification and verification of ABAC and in order to deal with large-scale systems, an a priori formal approach is proposed. Accordingly, an Event-B model of ABAC is constructed, where all the properties are validated and the correct behavior is proved. The approach concerns an ABAC specification for web services and instantiated in the healthcare field where it is of paramount importance to define correct access control policies. The ABAC basic model has been extended by adding notions such as: access purpose and privacy level. The main advantages of the solution are:

  • The model complexity of the system is decreased since the model is built step-by-step with refinements and proving based specification.

  • The approach generates a model with different abstraction views which simplify the observation and analysis of the specified model.

  • All the validated properties of the generic model remain valid after instantiation independently of the size of the model component instances.

As future work, the aim would be to complete the model in order to support access system reconfigurations and provide an implementation for composite web services and connected devices (IoT).