Keywords

1 Introduction

Enterprise data is a valuable target for malicious users and perpetrators. As the threats become higher nowadays, Access Control [1] is crucial to protect these sensitive resource and information in large scale information management system against unauthorized accesses by mediating every requests to resources and determining whether to grant or deny each individual access requests. Access Control Policy defines the high-level rules applying to Access Control process to regulate and control who has what kind of permissions to access which resources. Three main Access Control models are Discretionary Access Control (DAC) [2], Mandatory Access Control (MAC) [3] and Role-Based Access Control (RBAC) [4]. These model have been continuously developed, from DAC to MAC and RBAC in order to approach higher and higher level of Access Control. The RBAC model, which separate responsibilities in a system where multiple roles are fulfilled, is more suitable for nowadays organizations. The main power of RBAC comes from the Principle of Least Privilege and Separation of Duties, under which no one can take advantage of their granted accesses to perform malicious activities since no standalone individual has all permissions needed for an important operation.

Research works [5, 6] have been devoted to expand RBAC model to support higher level of security where the number of users and administrators keep increasing. Administrative Role-Based Access Control (ARBAC) [7] is proposed which specifies how RBAC policies may be changed by administrators and supports decentralized policy administration. In reality, RBAC policies may be changed occasionally when user changes their job or gets promoted. Thus, it needs to be modified, e.g., add or remove some tuples in the policies, by administrators. Managing changes is a complex task, which requires many administrators. Each administrator can make small changes to parts of the policies that, at first look, seems harmless. However, when in effect, the combination of all of these changes may lead to unsafe state which violates security properties of the policies. Therefore, it is paramount to have a solid change management solution which checks for vulnerabilities and violations in security before applying those changes to the policies. Analysis of these vulnerabilities in Administrative Role-Based Access Control (ARBAC97) [10] have been thoroughly done [17]. Over the last few year, many research have been focused on STRBAC [8] and the Administrative model of STRBAC [9]; however, there is no work focusing on the security analysis of the Administrative model of STRBAC. In order to overcome these shortcomings, in this paper, we propose a security analysis technique for STRBAC based on First Order Logic and Symbolic Model Checking [18]. The main idea is to adapt First Order Logic and Symbolic Model Checking to translate the security analysis problems of ASTRBAC policy to decidable reachability problems where total users and roles are finite but their exact number is not known in order to mechanize the analysis. This paper is the first research on security analysis of the ASTRBAC model. Based on the model checking proposed in [16], our research creates a framework to help security officer aware of the existence of vulnerabilities in the policies before applying those polices to production systems. This model can also return the group of actions which cause the vulnerability to help security officers in detecting and modifying security polices easier according to their needs and keep compliance with security requirements of the organization.

The rest of this paper is organized as follow. In Sect. 1, we introduce the RBAC, ARBAC and related security analysis problems. Section 2 briefly reviews the STRBAC, ASTRBAC models and demonstrates security issues related to these models. Section 3, we describe how we design a technique to analyze the problems. Section 4 summarizes our experiments and results, Sect. 5 is our conclusions.

2 Background

RBAC has been considered as an alternative to the well-known tradition access control such as DAC and MAC. In general, RBAC policy is a tuple (U, R, P, UA, PA) which consist of a set U of users, a set R of Roles, a set P of Permissions, a User-Role Assignment relation UA ⊆ U × R, a Role-Permission Assignment relation PA ⊆ R × P, and for simplicity, we ignore the role hierarchy (see [30] for more details). As stated in RBAC, a user u is a member of a role r if (u, r) ∈ UA; a role r is assigned permission p if (p, r) ∈ PA. Thus, a user is granted to permission p iff there exists a role r ∈ R such that (p, r) ∈ PA and u is the member of r. The UA relations in RBAC keep changing according to the growth and reduction of human resources in an organization while the PA will be less likely to change because of the fact that the change of this part means there is a change in organization structure and this may impact the entire system.

As RBAC expands to support hundreds of users and thousands of permissions in a large organization, several administrators are required to maintain the security policies, and thus, there is a high demand of both a consistent RBAC policy and an assurance that the policy can only be modified by administrators who are authorized to do so. The ARBAC is the most accepted administrative framework to control how RBAC policies might change through administrative actions by assigning or revoking user memberships into roles (URA model, a sub-model of ARBAC [7]). In URA model, administrators can only update the relation UA using the defined administrative actions while the relation PA keeps constant. The first administrative action is to assign users to roles and is defined using ternary relation can_assign(A,C,r) where A (called Administrative) and C (called Simple) are pre-conditions and r is a role (called target role). The second administrative action is to revoke users from roles and is defined using binary relation can_revoke(A,r) where A (called Administrative) is a pre-condition and r is a role (called target role). A pre-condition C is defined as a finite set of signed role, which expressed using +r or –r for r ∈ R. We can say that a user u ∈ U satisfied a pre-condition C (written as u ⊧ C) if for each c ∈ C, u is the member of r ∈ R when c is +r and u is not a member of r ∈ R when c is –r.

While this restriction can limit the administrative actions, research [11] has found that the change to RBAC policy by one administrator may interact in unintended or malicious ways with other administrator’s actions. This problem is well-known as the safety problem (also called the reachability problem), which the effects of these interactions may lead to an unintended role assignment to an untrusted user, and let that user have the ability to view or stole sensitive information or resources. In large organizations with thousands of roles, it is hard for policy designers to understand the ARBAC’s implications for those interactions.

In general, the safety problem is undecidable [19]. Several techniques have been introduced in [10, 12,13,14, 17] to solve the safety problem in administrative RBAC. The first research [10] uses state-transition system and logic programming but this approach faces the state space explosion problem and thus, it can only support a small and simple policies. The second [12] approaches the problem using model checking but its runtime is unacceptable with large policies. The third research [13] uses bounded model checking to check large policy but in some cases, it cannot decide whether a policy is safe or not. The forth research [14] simplifies the state space by reducing a policy to a smaller one that preserves the reachability of the target role, which requires limited users, and support only one role in the administrative pre-condition of administrative actions. The fifth research [17] has put forward to analysis and performs better than [14] but it still cannot specify “the reason” the policy is unsafe. Recently, the research [16] has improved from [17] with temporal support. To the best of our knowledge, ours is the first tool to solve the safety problem in STRBAC model.

3 Administrative Spatial Temporal RBAC

TRBAC.

In many scenarios, authorization depends on addition contextual information such as the location of user and the time of the day. In this case, an intern of an organization should only be authorized to access the information system of a company only in the branch he is working and during working hours such as between 7 am to 11 am. In order to understand the authorization conditions that depend on spatial temporal constrains, we need to introduce the model of location and time.

In [20, 21], the TRBAC model of time is usually specified by means of intervals periodically repeating time intervals, such as day and night-time (two intervals repeating daily), each hour per day (twenty-four intervals repeating daily), or each day per week (seven intervals repeating weekly). Let TMax be a positive integer and a is a non-negative integer such that a + 1 ≤ TMAX, A time slot is a pair (a; a + 1); to ease the readability, we will use (8am; 4pm), (4pm; 12am), and (12am; 8am) to denote time slots (0; 1), (1; 2), and (2; 3), respectively. The set of all time slots is TSTMAX = {(a; a + 1) | 0 ≤ a < TMAX}. We will usually write TS in place of TSTMAX when TMAX is clear from context and in this paper, we assume TMAX to be given so that the set TS is fixed. A time instant is a non-negative real number. A time instant t belongs to a time slot (a; a + 1), written as t ∈ (a; a + 1), iff a ≤ (t mod TMAX) < a + 1 where mod is the usual modulo operator, i.e., t0 = t mod TMAX iff there exists a non-negative integer k such that t = t0 + k · TMAX.

The location of a user proposed in [22] should be updated automatically using position determination system (PDS). GPS is one of the most well-known methods to get locations using satellite. Another method requires infrared sensors base station, infrared transponders and active infrared badges that can respond to the sensors to detect and inform user location to base station in small organizations. Other methods use wireless signal strength information from multiple stations to estimate the locations more accurately, which is usually found on mobile devices. In order to make RBAC spatially capable, the authors want to express location in a convenient way that can be interpreted by humans easily and to have a standard way of representing location in raw format, as stored by the system. They define two levels of locations, namely Primitive Location and Logical Location. A Primitive Location Lp is either the volume associated with basic unit of position that is returned by the PDS, or an artificially created volume defined by the administrator for PDSs that have high resolution. These may be created using Constructive Solid Geometry from basic geometric shapes defined by their coordinates. A logical location Ll is a combination of one or more logical or raw locations joined by a ∪, ∩ and / or \ operator combined with other primitive locations to form a logical location. In this paper, for the sake of simplicity, we will focus on logical location and assume that the location Ll to be updated by the PDS.

An enhanced version of STRBAC is ESTRBAC [23], this model proposes new concepts of role extent and permission extent to define the spatiotemporal access control policies. ESTARBAC still consists components of RBAC, namely, users, roles and permissions but they are associated with either spatial extents or spatial temporal extents. In ESTRBAC model, a set I of intervals is a set of all time slots that participate in at least one spatial temporal access control policy specification (e.g., I is a subset of TS. For simplicity, we consider I = TS in this paper, i.e., every time slots participates in policy specifiacation). Roles and permissions can be available only at specific locations and during specific time intervals, namely, Role Extents (RE) and Permission Extents (PE). In this paper, we will use these RE and PE to support our analysis.

We are now ready to formalize a simplified version of the Enhanced Spatial Temporal RBAC model based on ESTARBAC. The idea is to make RBAC policies depend on constraints based on the notion of both location and time introduced above.

Spatial Temporal RBAC.

From now on, we assume that both Ll and TMAX is given so that the set TS of all time slots is fixed and the set UL of all user logical locations UL ⊆ U × L is updated from the PDS. STRBAC extends RBAC by adding the Role Extents relation RE ⊆ R × L × TS, the Permission Extends PE ⊆ P × L × TS and replacing the user-role assignment UA with its spatial temporal user-role assignment relation UA ⊆ U × R × L × TS. For the sake of simplicity, following [24], we exclude role hierarchies.

An extent is a pair (l, ts) which associates spatial- temporal extent to roles or permissions. A role r is enabled at logical location l and time instant t iff there exists a time interval ts such that t belongs to ts and ts ∈ TS and (r, l, ts) ∈ RE. A user u is a member of role r at location l and interval ts iff r is enabled at location l and interval ts and (u; r; l, ts) ∈ UA. A user u can activate role r at location l and interval ts iff u is a member of role r within extent (l, ts) and u is at location l: (u, l) ∈ UL and the current time-slot is ts. Similarly, a permission p is enabled at location l and interval ts iff (p; l, ts) ∈ PE. A user u has permission p at location l and interval ts iff there exists role r such that (p; r) ∈ PA and p is enabled within extent (l, ts) and u is a member of r within extent (l, ts). A user u can access permission p at location l and interval ts iff u has permission p within extent (l, ts) and u is at location l: (u, l) ∈ UL and the current time-slot is ts. Our STRBAC policy is a tuple (U; R; P; UA; PA; L; TS; UL; RE; PE).

ASTRBAC.

One of the Administrative model designed to manage the change of STRBAC policy named ADMINESTAR [9], which allows multiple administrators to modify the STRBAC policy while ensures they cannot abuse the system using their powers. An administrative action consists two components, administrative policies and administrative operation, to define which administrators are allowed to modify ESTRBAC policy. Administrative Policies governs a set of administrative rules to specific which administrative role is authorized to modify ESTARBAC entities of which regular role range. From now on, we focus on the set of administrative rules. All ESTARBAC entities together define the system state, which changes when one or more of the entities change. Administrative Operations are the change of the system state upon their completion only if the administrative policies allow. Administrative Policies and Administrative Operations become more complex if their access control has more attributes.

Our promoted ASTRBAC model.

Our model based on ADMINESTAR [9], has more constraints in administrative rule. In ADMINESTAR, administrator condition only have one role so it cannot express actions that require administrator to have more than one role. In our ASTRBAC model, administrator rule is a set of roles so that administrative actions can describe more administrative scenario. ASTRBAC focuses on managing data of these entities: UA, RE, PE, PA by providing actions on them. These actions are divided into four groups depend on their target, can_assign_UA and can_revoke_UA are designed to manage entity UA; can_assign_PA and can_revoke_PA are designed to manage entity PA; can_add_RE and can_delete_RE are designed to manage entity RE; and can_add_PE and can_delete_PE are designed to manage entity PE.

We assume that entity UL is automatically managed by PDS so there is no actions to manage UL in this paper; that the basic entities R, P, L, and TS are finite and constant; and that entity U is infinite. Thus, a STRBAC policy depends on the entities UA, RE, PE, PA. If one of those entities is modified, the STRBAC status will be changed. Hence, the administrative actions need to be examined carefully as these actions can lead the STRBAC policies to a state in which the security requirement of the system is violated. Such problem is well-known as the reachability problem [10, 11].

In the following, let α = (U; R; P; UA; PA; L; TS; UL; RE; PE) be a STRBAC policy. A signed role is an expression of the form +r or –r. A role condition is a finite set of signed roles. A signed role σ in a condition C is positive when there exists a role r such that σ = + r, a condition C is negative when there exists a role r such that σ = −r. An administrative action is a tuple ({Arule, la, tsa}, {Rrule, lu, tsu}, Ud) where tuple {Arule, la, tsa} is called admin pre-conditon, Arule is a role condition, (la, tsa) are location and time-slot that together describe spatial temporal constraint on Arule; Tuple {Rrule, lu, tsu} is called user pre-condition where Rrule is a role condition; (lu, tsu) are location and time-slot that express spatial temporal constraint on Rrule that are used together to limit the users whose extents can be modified by the administrator; the Ud element can be an element or many elements depend on each actions. The user pre-condition is optional while admin pre-condition is compulsory for all actions.

Pre-condition.

We will discuss the way our system checks these pre-condition.

The admin pre-condition is passed if at least, one administrator satisfies tuple {Arule, la, tsa}, the positive roles +r in Arule specify the roles administrators must activate at location la during time slot tsa, the negative roles –r in Arule describe the roles administrators cannot activate within the extent (la, tsa). Administrator a can activate role r within the extent (l, ts) iff the formula ∃ tscur: [(ad,l) ∈ UL ∧ (ad, r, l, ts) ∈ UA ∧ (r, l, ts) ∈ RE ∧ (tscur = ts)] returns true, where tscur is the current time-slot determined by system. The following check_role_admin formula ensures the admin pre-condition is checked, if it returns true, there exist an administrator can perform the corresponding action, otherwise, the action is rejected since there is no administrator who can satisfy admin pre-condition.

\( \begin{aligned} & {\text{check}}\_{\text{role}}\_{\text{admin}}\,\left( {{\text{A}}_{\text{rule}} ,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right)\,:\,\exists \,{\text{ad}},\,{\text{ts }}[\left( {\left( {{\text{ad}},\,{\text{l}}_{\text{a}} } \right) \in {\text{UL}}} \right) \wedge \left( {{\text{ts}}_{\text{cur}} = {\text{ ts}}_{\text{a}} } \right) \wedge \\ & \wedge_{{({\text{role}}\, \in \,{\text{Arule}})}} \left( {\left( {{\text{ad}},\,{\text{r}},\,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right) \in {\text{UA}} \wedge \left( {{\text{r}},\,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right) \in {\text{RE}}} \right)\,if \, role\, = \, + r \\ & \wedge_{{({\text{role}}\, \in \,{\text{Arule}})}} \left( {\left( {{\text{ad}},\,{\text{r}},\,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right) \notin {\text{UA}} \vee \left( {{\text{r}},\,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right) \notin {\text{RE}}} \right)\,if\,role\, = - r] \\ \end{aligned} \)

The user pre-condition {Rrule, lu, tsu} limits which users whose extents can be modified by administrators. The positive roles +r in Rrule specify the roles user must be assigned within extent (lu, tsu), negative roles –r specify the roles users must not be assigned within extent (lu,tsu). The User Role Assignment relation UA needs to be checked if user u satisfies (Rrule, lu, tsu) using check_role_user formula

\( \begin{aligned} & {\text{check}}\_{\text{role}}\_{\text{user}}\,\left( {{\text{u}},\,{\text{R}}_{\text{rule}} ,\,{\text{l}}_{\text{u}} ,\,{\text{ts}}_{\text{u}} } \right):{\bigwedge }_{{({\text{role}} \in \,\,{\text{Rrule}})}} \left( {\left( {{\text{u}},\,{\text{r}},\,{\text{l}}_{\text{u}} ,\,{\text{ts}}_{\text{u}} } \right) \in {\text{UA}}\,if\,role = + r} \right) \\ & \wedge_{{({\text{role}} \in \,{\text{Rrule}})}} \left( {\left( {{\text{u}},\,{\text{r}},\,{\text{l}}_{\text{u}} ,\,{\text{ts}}_{\text{u}} } \right) \notin {\text{UA}}\,if\,role\, = \, - r} \right) \\ \end{aligned} \)

If check_role_user returns true, extents (role or permission extents) of user u can be updated, otherwise, it cannot be updated with this action. In conclusion for these pre-condition, an action can be performed iff admin pre-condition is passed and there exist an user can be updated (in some actions).

Administrative Actions.

An STRBAC policy has 4 main sets, set UA, RE, PE and PA. The corresponding action for these sets are listed below.

  • Can_Assign_UA (Arule, la,tsa, Rrule, lu, tsu, r)

  • Can_Revoke_UA (Arule, la, tsa, Rrule, lu, tsu, r)

  • Can_Add_RE (Arule, la, tsa, r, l, ts)

  • Can_Delete_RE (Arule, la, tsa, r, l, ts)

  • Can_Assign_PA (Arule, la, tsa, rt, pt)

  • Can_Revoke_PA (Arule, la, tsa, rt, pt)

  • Can_Add_PE (Arule, la, tsa, p, l, ts)

  • Can_Delete_PE (Arule, la, tsa, p, l, ts)

User-Assignment actions:

such actions are designed to manage the actions add or delete tuples in relation UA using role assignment and role revocation actions of users within certain spatial-temporal extents.

  • Can_Assign_UA (Arule, la, tsa, Rrule, lu, tsu, r), where {Arule, la, tsa} is admin pre-condition, [Rrule, lu, tsu] is user pre-condition, (lu, tsu,r) is the update tuple. Arule and Rrule can contain positive roles +r in companion within extent (lu, tsu), negative roles is −r conflict within extent (lu, tsu). Notice that, this action can assign (lu, tsu, r) to any users that satisfy user pre-condtion. Can_Assign_UA is enabled if admin pre-condtion is satisfied and there exist a user u satisfy user pre-condition Rrule.

    $$ \exists \,{\text{u}}\left( {{\text{check}}\_{\text{role}}\_{\text{admin}}\,\left( {{\text{A}}_{\text{rule}} ,\,{\text{l}}_{\text{a}} ,\,{\text{ts}}_{\text{a}} } \right)\,{\bigwedge }\,{\text{check}}\_{\text{role}}\_{\text{user}}\left( {{\text{u}},\,{\text{R}}_{{{\text{rule}},}} {\text{l}}_{\text{u}} ,\,{\text{ts}}_{\text{u}} } \right)} \right) $$

    Once this rule is passed, the tuple (u, r, lu, tsu) is added to UA using \( {\text{UA}}^{\prime } = {\text{UA}}\,{\bigcup }\,\left( {{\text{u}},{\text{ r}},{\text{ l}}_{\text{u}} ,{\text{ ts}}_{\text{u}} } \right) \) where u is the user need to assign new roles.

  • Can_Revoke_UA (Arule, la, tsa, Rrule, lu, tsu, r) where (Arule, la, tsa) is admin pre-condition, (lu, tsu,r) is update tuple. Rrule can contain positive roles +r in companion within extent (lu, tsu), negative roles is −r conflict within extent (lu, tsu). Can_Revoke_UA revoke (lu, tsu, r) from any users. Administrator need to satisfy the admin pre-condition to enable this rule and there exist a user u satisfy user pre-condition Rrule, this check uses formula check_role_admin(Arule, la, tsa). Once this rule is passed, the tuple (u, lu, tsu, r)) is removed from \( {\text{UA}}:\exists \,{\text{u UA}}^{\prime } = {\text{UA}}\backslash \left( {{\text{u}},{\text{ r}},{\text{ l}}_{\text{t}} ,{\text{ ts}}_{\text{t}} } \right) \) where u is the user need to revoke user roles.

RoleExtent actions:

such actions are designed to manage the actions add or delete tuples in relation RE using adding and deleting actions of role within certain spatial-temporal extents. Role extents that are registered in RE can be assigned to users in entity UA. In order to activate a role within a spatial-temporal extent, that role must be assigned to user in UA and enable within that extent in RE.

  • Can_Add_RE (Arule, la, tsa, r, l, ts) where (Arule, la, tsa) is admin pre-condition, (r,l,ts) is the update tuple. The admin pre-condition must be checked using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the spatial-temporal extent of role r is added with tuple (l, ts): \( {\text{RE}}^{\prime } = {\text{RE}}\,{\bigcup }\,\left( {{\text{r}},{\text{ l}},{\text{ ts}}} \right) \)

  • Can_Delete_RE (Arule, la, tsa, r, l, ts) where (Arule, la, tsa) is admin pre-condition, (r, l, ts) is the update tuple. The admin pre-condition must be checked to enable this action using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the spatial-temporal extent of role r is deleted with tuple (l, ts): \( {\text{RE}}^{\prime } = {\text{RE}}\backslash \left( {{\text{r}},{\text{ l}},{\text{ ts}}} \right) \)

Permission-Assignment actions:

such actions are designed to manage the actions add or delete tuples in relation PA using permission assignment and permission revocation actions of roles.

  • Can_Assign_PA (Arule, la, tsa, rt, pt) where {Arule, la, tsa} is admin pre-condition, the (rt, pt) is the update tuple. The admin pre-condition must be checked using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the role rt and permission pt is added \( {\text{PA}}^{\prime } = {\text{PA}}\,{\bigcup }\,\left( {{\text{r}}_{\text{t}} ,{\text{ p}}_{\text{t}} } \right) \)

  • Can_Revoke_PA (Arule, la, tsa, rt, pt) where (Arule, la, tsa) is admin pre-condition, (rt, pt) is the update tuple. The admin pre-condition must be checked to enable this action using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the role rt and permission pt is r is deleted \( {\text{PA}}^{\prime } = {\text{PA}}\backslash \left( {{\text{r}}_{\text{t}} ,{\text{ p}}_{\text{t}} } \right) \)

PermissionExtent actions: such actions are designed to manage the actions add or delete tuples in realtion PE using Can Add and Can Delete actions of permissions within certain spatial-temporal extents.

  • Can_Add_PE (Arule, la, tsa, p, l, ts) where {Arule, la, tsa} is admin pre-condition, (p, l, ts) is the update tuple. The admin pre-condition must be checked using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the permission p and its spatial temporal is added \( {\text{PE}}^{\prime } = {\text{PE}}\,{\bigcup }\,\left( {{\text{p}},{\text{ l}},{\text{ ts}}} \right) \)

  • Can_Delete_PE (Arule, la, tsa, p, l, ts) where (Arule, la, tsa) is admin pre-condition, (p, l, ts) is the update tuple. The admin pre-condition must be checked to enable this action using formula: check_role_admin (Arule, la, tsa). Once this rule is passed, the permission p and its spatial temporal is deleted \( {\text{PE}}^{\prime } = {\text{PE}}\backslash \left( {{\text{r}}_{\text{t}} ,{\text{ p}}_{\text{t}} } \right) \)

A run of an ASTRBAC system \( \left( {{\alpha_0},\upvarphi } \right) \) is a (possibly infinite) sequence (α0; 0)… (αi; ti); (αi+1; ti + 1), … of states such that (αi; ti) → (αi+1; ti+1) and ti ≤ ti+1 for i = 1… n − 1 with n > 1. If the run is finite, i.e. it is of the form (α0; 0) … (αn; tn) for some n ≥ 0, we say that (αn; tn) is the final state of the run.

Even if administrators can only execute a given set of administrative actions mentioned above, it is still very difficult to foresee all possible interleaving of actions when many administrators perform their administrative actions together with their effect on an initial STRBAC policy. Therefore, in some cases, an untrusted user can gain, in some spatial temporal, a permission which that person should not gain. In order to identify this situation, we need to solve the next analysis problem.

A reachability problem for an ASTRBAC system \( (\upalpha_{0} ;{\upvarphi }) \) is identified by a tuple (u; Cf; lf, tsf) and amounts to checking if there exists a finite run of the ASTRBAC system whose final state (αf; lf, tsf) is such that user u, location ls and timeslot tsf satisfy condition Cf under UAf and ls, tsf satisfies Cf under REf, and ls, tsf satisfies Cf under PEf where αf = (UAf; REf; PEf).

Example 1.

Consider an STRBAC policy below.

  • Let U = {Alice; Bob; Peter; Shan; Mary}

  • R = {Manager; Engineer; Technician; Tester; Developer}

  • L = {A1 building; A2 building; A3 building}

  • TS = {Morning: [8:00am – 12:00pm]; Afternoon: (12:00pm – 18:00pm); Night: [18:00pm – 8:00am]}

  • P = {Write_O1; Write_O2; Read_O2; Write_O2}

  • UA = {(Alice, Manager, A1 building, Morning); (Bob, Engineer, A2 building, Morning); (Peter, Technician, A3 Building, Afternoon); (Shan, Engineer, A1 building, Afternoon); (Mary, Engineer, A1 Building, Afternoon); (Shan, Tester, A1 building, Afternoon); (Bob, Developer, A2 building, Morning)}

  • PA = {(Manger, Write_O1); (Engineer, Write_O2); (Technician, Read_O2); (Manager; Read_O2); (Manager, Write_O2)}

  • RE = {(Manager, A2 building, Morning); (Engineer, A1 building, Morning); (Engineer, A2 building, Morning); (Manager, A1 building, Morning); (Technician, A3 building, Afternoon); (Tester, A1 building, Afternoon); (Engineer, A1 building, Afternoon)}

  • PE = {(Read_O2, A3 building, Afternoon); (Write_O2, A2 building, Morning); (Write_O1, A1 building, Afternoon)}

  • UL = {(Alice, A1 building); (Bob, A2 building); (Shan, A1 building); (Peter, A3 building), (Mary, A1 building)}

The ASTRBAC rule contains these rule.

  1. 1.

    Can_Assign_PA ({Manager}, A1 building, Morning, Engineer, Write_O1)

  2. 2.

    Can_Assign_UA({Manager}, A1 building, Morning, {Engineer, -Technician, -Manager}, A2 building, Afternoon, Tester)

  3. 3.

    Can_Add_RE ({Manager}, A1 building, Morning, Engineer, A1, Afternoon)

  4. 4.

    Can_Add_RE({Manager, A1 building, Morning, Tester, A2, Afternoon)

  5. 5.

    Can_Add_PA({Engineer}, A1 building, Morning, Tester, Read_O2)

  6. 6.

    Can_Assign_UA({Engineer, -Tester}, A1, Afternoon, {Engineer, -Tester}, A2 building, Morning, Tester)

In check_role_admin, consider actions (6), the admin pre-condition is tuple ({Engineer, -Tester}, A1 building, Afternoon) and pretends that our current time slots tscur is Afternoon. The check_role_admin ({Engineer, -Tester}, A1 building, Afternoon) returns true because there exists admin “Mary” satisfied [((Mary, A1 building) ∈ UL) ∧ (tscur = Afternoon) ∧ ((Mary, Engineer, A1 building, Afternoon) ∈ UA) ∧ ((Engineer, A1 building, Afternoon) ∈ RE) ∧ [((Mary, Tester, A1 building, Afternoon) ∉ UA ∨ ((Tester, A2 building, Afternoon) ∉ RE)]. Since check_role_admin returns true, user Mary can perform corresponding administrative action (6). In this example, user Shan can activate both role Engineer and Tester within extents (A1 building, Afternoon) but Tester is a negative role in (6) so Shan is not allowed to perform administrative action (6). Similarly, the formula check_role_user (Bob; {Engineer, -Tester}, A2 building, Morning) returns true since it satisfied ((Bob, Engineer, A2 building, Morning) ∈ UA ∧ ((Bob, Tester, A2 building, Morning) ∉ UA). User Mary can assign a new role Tester for Bob in location “A2 building” at the interval “Morning”.

Now, we consider the reachability problems in ASTRBAC and a safety attribute (Write_O1, A1 building, Afternoon) and our current timeslot tscur is Morning. We assume that the initial state is α0 = (UA0, RE0, PE0, PA0). It is easy to check that user Alice can use actions (1) and (3), because ULAlice = {Alice, A1 building} ∈ UA can satisfy administrative condition Arule(1) = {Manager, A1 building, Morning} under RE = {Manager, A1 building, Morning}. After actions (1), our STRBAC state will change from α0 to α1 which adds new information to PA where PA1 = PA0 ⋃ (Engineer, Write_O1) since Alice. Similarly, Alice can use action (3) to change our STRBAC state from α1 to α2 to adds new information to RE where RE2 = RE1 ⋃ (Engineer, A1 building, Afternoon). In state α2, when our current timeslot change tscur = Afternoon, user Shan can satisfy conditions [((Shan, A1 building) ∈ UL) ∧ (tscur = Afternoon) ∧ ((Shan, Engineer, A1 building, Afternoon) ∈ UA) ∧ ((Engineer, A1 building, Afternoon) ∈ RE) ∧ ((Write_O1, A1 building, Afternoon) ∈ PE) ∧ ((Engineer, Write_O1) ∈ PA)]. In the end, user Shan can Write_O1 in location A1 building and timeslot Afternoon, which violate our security attributes.

4 Implementation and Evaluation

The reachability problem analysis.

In [30], the reachability problem analysis can be separated into two main parts: User-Role Reachability Analysis (URRA) and Permission-Role Reachability Analysis (PRRA). As seen in Example 1, in order to check the reachability problem of ASTRBAC, we need to check the both of them in the tuple (UA, RE) and (PE, PA). However, just like ASTRBAC, the tuple (PE, PA) of STRBAC are less likely to change as mentioned in Sect. 2. In our techniques, we will focus on implementing a tool to check the User-Role Reachability Analysis since the Permission-Role Reachability Analysis can be implemented similarly.

Implementing the Translator.

We implement our technique which will be discussed below in a tool called ASASPSPACETIME. As in Fig. 1 this tool has two main parts, the Translator, implemented in Python, will get the input of our ASTRBAC reachability problem (u; C; l; ts) as reachability problem for STRBAC policies \( (\upalpha_{0} ;{\upvarphi }) \), answer our problem with statement “reachable” or “unreachable” and show the sequence of actions which changed our STRBAC policies from αo to αn where αn can satisfy (u; C; l; ts). The second part for analysis of ASTRBAC policies uses SMT-based model checker named MCMT [25] to solve our problem. According to [28], we try to reduce our reachability problems for ASTRBAC model to a (finite) sequence of constraint satisfaction problems.

Fig. 1.
figure 1

Our technique to solve the reachability problem for ASTRBAC

Full size image

At first, we translate ASTRBAC policies to First Order Logic formula which belongs to Bernays-Schonfinkel-Ramsey (BSR) [28] class to determine the satisfy-ability of formula, which has the form ∃x.∀y.\( {\upvarphi } \)(x; y) where \( {\upvarphi } \) is a quantifier-free formula, x and y are (disjoint and possible empty) tuples of variable. Then, we use Model Checking Modulo Theories (MCMT) [25], which is a framework to solve reachability problems for infinite state systems that can be represented by transition systems whose set of states and transitions are encoded as constraints in First-Order Logic. MCMT framework uses a backward reachability procedure to solve a particular class of constraint satisfy-ability problems, called Satisfy-ability Modulo Theories (SMT) problems. According to [26], MCMT framework is a scalable and efficient SMT solver currently available.

Here is how we translate the ASTRBAC to First Order Logic in BSR class. We need to translate an initial state, the administrative actions, time passing, and the goal.

Our state variable in ASTRBAC contains re, ua, loc, and at where re is a variable of for the current role extent RE, similarly, ua for UA, loc for UL and at is current system time.

Our initial state contains the tuple α0 = (RE, UA, UL, ts0) where ts is timeslot, which can be translated as below.

$$ \begin{aligned} \forall {\text{x}},{\text{y}},{\text{z}},{\text{t}}.{\text{ ua}}\left( {{\text{x}},{\text{y}},{\text{z}},{\text{t}}} \right) & \Leftrightarrow \vee_{{\left( {{\text{u}},{\text{r}},{\text{l}},{\text{ts}}} \right)\, \in {\text{UA}}}} ({\text{x}} = {\text{u}} \wedge {\text{y}} = {\text{r}} \wedge {\text{z}} = {\text{l}} \wedge {\text{t}} = {\text{ts}}) \wedge \\ {\text{re}}\left( {{\text{y}},\,{\text{z}},\,{\text{t}}} \right) & \Leftrightarrow \vee_{{\left( {{\text{r}},{\text{l}},{\text{ts}}} \right)\, \in {\text{RE}}}} \left( {{\text{y }} = {\text{r}},\,{\text{z}} = {\text{l}},\,{\text{t}} = {\text{ts}}} \right) \wedge \\ {\text{at}}\left( {\text{z}} \right) & \Leftrightarrow {\text{z}} = {\text{ts}}_{\text{o}} \\ \end{aligned} $$

Example 2.

We analyze a simple example of ASTRBAC

  • Let U = {Alice; Bob; Peter}

  • R = {Manager; Engineer; Technician; Tester; Developer}

  • L = {A1 building; A2 building}

  • I = {Morning: [8:00am – 12:00pm]; Afternoon: (12:00pm – 18:00pm)}

  • UA = {(Alice, Manager, A1 building, Morning); (Bob, Engineer, A2 building, Morning);}

  • RE = {(Engineer, A1 building, Morning: [8:00am – 12:00pm]), (Technician, A2 building, Afternoon: [12:00pm – 18:00pm])}

  • UL = {(Alice, A1 building); (Bob, A2 building)}

  • Current time = 8am;

The ASTRBAC rule contains these rule.

  1. 1.

    Can_Assign_UA({Manager}, A1 building, Morning, {Engineer}, A2 building, Afternoon, Tester)

  2. 2.

    Can_Revoke_UA({Manager}, A1 building, Morning, {Engineer}, A2 building, Afternoon, Tester)

  3. 3.

    Can_Add_RE ({Manager}, A1 building, Morning, Engineer, A1 building, Afternoon)

  4. 4.

    Can_Delete_RE ({Manager}, A1 building, Morning, Engineer, A1 building, Afternoon)

According the example above, the current time belongs to time slots Morning, so our initial state will be

$$ \begin{aligned} &\forall {\text{x}},{\text{y}},{\text{z}},{\text{t}}.{\text{ ua}}\left( {{\text{x}},{\text{y}},{\text{z}},{\text{t}}} \right) \Leftrightarrow \nonumber\\ &(({\text{x}} = {\text{Alice}} \wedge {\text{y}} = {\text{Manager}} \wedge {\text{z}} = {\text{A1 building}} \wedge {\text{t}} = {\text{Morning}}) \vee ({\text{x}} = {\text{Bob}} \wedge {\text{y}} = {\text{Engineer}} \nonumber\\ & \wedge {\text{z}} = {\text{A2}}\,{\text{building}} \wedge {\text{t}} = {\text{Afternoon}})) \wedge \nonumber\\ &\qquad\; {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow (({\text{y }} = {\text{Engineer}},{\text{ z}} = {\text{A1 building}},{\text{ t}} = {\text{Morning}}) \, \vee \, ({\text{y }} = {\text{Technician}},\nonumber\\ &{\text{z}} = {\text{A2}}\,{\text{building}},{\text{ t}} = {\text{Afternoon}})) \wedge \nonumber\\ &\qquad\;{\text{at}}\left( {\text{z}} \right) \Leftrightarrow {\text{z}} = {\text{Morning}}\nonumber \end{aligned} $$

Our ASTRBAC now contains 4 actions (Can_Assign_UA, Can_Revoke_UA, Can_Add_RE, Can_Delete_RE) and a goal. We translate each of them as follow.

  • Can_Assign_UA (A, la, tsa, Ru, lu, tsu, ru)

    $$ \begin{array}{*{20}l} { \Leftrightarrow \exists {\text{u}}_{\text{a}} ,{\text{ u}},{\text{ ts}}.{\text{ at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ ts}}_{\text{a}} \wedge } \hfill \\ {\quad \quad \,\,{\text{Loc}}\left( {{\text{u}}_{\text{a}} ,{\text{ l}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \, \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \, \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \, \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{R}}}} \,{\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}}_{{{\text{u}},}} {\text{t}}_{\text{u}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{R}}}} \neg {\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}}_{{{\text{u}},}} {\text{t}}_{\text{u}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right)\, \vee ({\text{x }} = {\text{ u}} \wedge {\text{y }} = {\text{ r}}_{\text{u}} \wedge {\text{z }} = {\text{ l}}_{\text{u}} \wedge {\text{t }} = {\text{ ts}}_{\text{u}} )) \wedge } \hfill \\ {\quad \quad \quad \quad \,\,(\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

Example 3.

According to Example 2, the Can_Assign_UA({Manager}, A1 building, Morning, {Engineer}, A2 building, Afternoon, Tester) can be translated as

$$ \begin{array}{*{20}l} {\exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.{\text{ at}}\left( {\text{ts}} \right)} \hfill \\ {\quad \quad \quad {\text{at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ Morning}} \wedge } \hfill \\ {\quad \quad \quad {\text{Loc}}\left( {{\text{Manager}},\,{\text{A1 building}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{re}}({\text{Manager}},\,{\text{A1 building,}}\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{ua}}({\text{u}}_{\text{a}} ,\,{\text{Manager}},\,{\text{A1}}\,{\text{building}},{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{ua}}({\text{u}},{\text{Engineer}},{\text{ A2}}\,{\text{building,}}\,{\text{Afternoon}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} {\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \vee ({\text{x = u}} \wedge {\text{y }} = {\text{Tester}} \wedge {\text{z }} = {\text{A2 building}} \wedge {\text{t }} = {\text{Afternoon}})) \wedge } \hfill \\ {\quad \quad \quad \quad \,\,(\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},{\text{ t}}}} {\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} {\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

  • Can_Revoke_UA (A, la, tsa, R, lu, tsu, ru)

    $$ \begin{array}{*{20}l} { \Leftrightarrow \exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.\,{\text{at}}\left( {\text{ts}} \right) \wedge {\text{ts}}\, = \,{\text{ts}}_{\text{a}} \wedge } \hfill \\ {\quad \quad \,{\text{Loc}}\left( {{\text{u}}_{\text{a}} ,\,{\text{l}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{R}}}} \,{\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}}_{{{\text{u}},}} {\text{t}}_{\text{u}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{R}}}} \neg {\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}}_{{{\text{u}},}} {\text{t}}_{\text{u}} } \right) \wedge } \hfill \\ {\quad \quad \quad (\forall_{{{\text{x}},\,{\text{y}},\,{\text{z}}\,,{\text{ t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge \neg ({\text{x }} = {\text{ u}} \wedge {\text{y }} = {\text{ r}}_{\text{u}} \wedge {\text{z }} = {\text{ l}}_{\text{u}} \wedge {\text{t }} = {\text{ ts}}_{\text{u}} )) \wedge } \hfill \\ {\quad \quad \quad \,(\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},{\text{ t}}\,}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \wedge } \hfill \\ {\quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},{\text{ t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

Example 4.

According to Example 2, the Can_Revoke_UA({Manager}, A1 building, Morning, {Engineer}, A2 building, Afternoon, Tester) can be translated as

$$ \begin{array}{*{20}l} {\exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.\,{\text{at}}\left( {\text{ts}} \right)} \hfill \\ {\quad \quad \quad {\text{at}}\left( {\text{ts}} \right) \wedge {\text{ts = Morning}} \wedge } \hfill \\ {\quad \quad \quad {\text{Loc}}\left( {{\text{Manager}},\,{\text{A1 building}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{re}}({\text{Manager}},{\text{A1 building}},\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{ua}}({\text{u}}_{\text{a}} ,{\text{Manager}},{\text{A1 building}},\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,{\text{ua}}({\text{u}},{\text{Engineer}},{\text{ A2}}\,{\text{building,}}\,{\text{Afternoon}}) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},\,{\text{y}},\,{\text{z}},\,{\text{t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge \neg ({\text{x }} = {\text{ u}} \wedge {\text{y }} = {\text{Tester}} \wedge {\text{z }} = {\text{A2 building}} \wedge {\text{t }} = {\text{Afternoon}})) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},\,{\text{y}},\,{\text{z}},\,{\text{t}}}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},\,{\text{y}},\,{\text{z}},\,{\text{t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

  • Can_Add_RE (A, la, tsa, ru, lu, tsu)

    $$ \begin{array}{*{20}l} { \Leftrightarrow \exists {\text{u}}_{\text{a}} ,{\text{ u}},{\text{ ts}}.{\text{ at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ ts}}_{\text{a}} \wedge } \hfill \\ {\quad \quad \,{\text{Loc}}\left( {{\text{u}}_{\text{a}} ,{\text{ l}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{re}}\left( {{\text{r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}}\, \in \,{\text{A}}}} \,{\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r}}\, \in \,{\text{A}}}} \neg {\text{ua}}\left( {{\text{u}}_{\text{a}} ,{\text{ r}},{\text{ l}}_{{{\text{a}},}} {\text{t}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \vee ({\text{y }} = {\text{ r}}_{\text{u}} \wedge {\text{z }} = {\text{ l}}_{\text{u}} \wedge {\text{t }} = {\text{ ts}}_{\text{u}} )) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

Example 5.

According to Example 2, the Can_Add_RE ({Manager}, A1 building, Morning, Engineer, A1 building, Afternoon) can be translated as

$$ \begin{array}{*{20}l} {\exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.{\text{ at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ Manager}} \wedge } \hfill \\ {\quad \quad \quad {\text{Loc}}\left( {{\text{A1 building}},{\text{ Morning}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad {\text{re}}({\text{Manager}},\,{\text{A1 building,}}\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad {\text{ua}}({\text{u}}_{\text{a}} ,\,{\text{Manager}},\,{\text{A1 building,}}\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{yz}},{\text{ t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \vee ({\text{y }} = {\text{Engineer}} \wedge {\text{z }} = {\text{A1 building}} \wedge {\text{t }} = {\text{Afternoon}})) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},{\text{ t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

  • Can_Delete_RE (A, la, tsa, ru, lu, tsu)

    $$ \begin{array}{*{20}l} { \Leftrightarrow \exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.{\text{ at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ ts}}_{\text{a}} \wedge } \hfill \\ {\quad \quad \quad {\text{Loc}}\left( {{\text{u}}_{\text{a}} ,{\text{ l}}_{\text{a}} } \right) \wedge } \hfill \\ {\quad \quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r}} \in {\text{ A}}}} \,{\text{re}}\left( {{\text{r}},{\text{ l}}_{\text{a}} ,{\text{ t}}_{\text{a}} } \right) {\wedge}{\wedge}_{{{\text{ -r }} \in {\text{ A}}}} \neg {\text{re}}\left( {{\text{r}},{\text{ la}},{\text{ ta}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad \mathop{\bigwedge}\nolimits_{{ + {\text{r }} \in {\text{ A}}}} \,{\text{ua}}\left( {{\text{ua}},{\text{ r}},{\text{ la}},{\text{ ta}}} \right) {\wedge}{\wedge}_{{{\text{ -r }} \in {\text{ A}}}} \neg {\text{ua}}\left( {{\text{ua}},{\text{ r}},{\text{ la}},{\text{ ta}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} \,{\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad \,(\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} \,{\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \, \wedge \, \neg \left( {{\text{y }} = {\text{ ru }} \wedge {\text{ z }} = {\text{ lu }} \wedge {\text{ t }} = {\text{ tsu}}} \right)) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}}} \,{\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

Example 6.

According to Example 2, the Can_Delete_RE ({Manager}, A1 building, Morning, Engineer, A1 building, Afternoon) can be translated as

$$ \begin{array}{*{20}l} {\exists {\text{u}}_{\text{a}} ,\,{\text{u}},\,{\text{ts}}.{\text{ at}}\left( {\text{ts}} \right) \wedge {\text{ts }} = {\text{ Manager}} \wedge } \hfill \\ {\quad \quad \quad {\text{Loc}}\left( {{\text{A1 building}},{\text{ Morning}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad {\text{re}}({\text{Manager}},{\text{A1 building,}}\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad {\text{ua}}({\text{u}}_{\text{a}} ,{\text{ Manager}},{\text{A1 building,}}\,{\text{Morning}}) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} {\text{ua}}^{\prime } \left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{ua}}\left( {{\text{x}},{\text{ y}},{\text{ z}},{\text{ t}}} \right) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} {\text{re}}^{\prime } \left( {{\text{y}},{\text{ z}},{\text{ t}}} \right) \Leftrightarrow {\text{re}}\left( {{\text{y}},{\text{ z}},{\text{ t}}} \right)) \wedge \, \neg ({\text{y }} = {\text{Engineer}} \wedge {\text{z }} = {\text{A1 building}} \wedge {\text{t }} = {\text{Afternoon}})) \wedge } \hfill \\ {\quad \quad \quad \quad (\forall_{{{\text{x,}}\,{\text{y,}}\,{\text{z}},\,{\text{t}}}} {\text{loc}}^{\prime } \left( {{\text{x}},{\text{ z}}} \right) \Leftrightarrow {\text{loc}}\left( {{\text{x}},{\text{ z}}} \right))} \hfill \\ \end{array} $$

  • Time passing: as mentioned in Sect. 3, the following formula means that every time the state of time change, we will move to the next time slots.

If j + 1 < T max , then

$$ \left[ {\begin{array}{*{20}l} {\quad \quad \quad \quad \quad \quad \quad \quad at\,(ts) \wedge ts = (j,j + 1) \wedge } \hfill \\ {\forall y,z,t.re^{\prime } (y,z,t)\,(re(y,z,t) \wedge \forall x,y,z,t.ua^{\prime } \left( {x,y,z,t} \right)(ua(x,y,z,t) \wedge } \hfill \\ {\quad \quad \quad \quad \forall z.L^{\prime } (z)\,(L(z) \wedge \forall t.at^{\prime } (t)\,(\left( {t = (j + 1,\,j + 2)} \right)} \hfill \\ \end{array} } \right] $$

Otherwise:

$$ \left[ {\begin{array}{*{20}c} {at\,(ts) \wedge ts = (j,j + 1) \wedge } \\ {\forall y,z,t.re^{\prime } (y,z,t)\,(re(y,z,t) \wedge \forall x,y,z,t.ua^{\prime } \left( {x,y,z,t} \right)(ua(x,y,z,t) \wedge } \\ {\forall z.L^{\prime } (z)\,(L(z) \wedge \forall t.at^{\prime } (t)((t = (0,1))} \\ \end{array} } \right] $$

  • Goal state:

    $$ \begin{array}{*{20}l} {\left( {{\text{u}}_{{{\text{g}},}} {\text{r}}_{{{\text{g}},}} {\text{l}}_{\text{g}} ,{\text{ ts}}_{\text{g}} } \right) \Leftrightarrow } \hfill \\ {\exists {\text{u}},{\text{ r}},{\text{ l}},{\text{ ts}}.{\text{ re}}\left( {{\text{r}},{\text{ l}},{\text{ ts}}} \right) \wedge {\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}},{\text{ ts}}} \right) \wedge {\text{u}} = {\text{u}}_{\text{g}} \wedge {\text{r }} = {\text{r}}_{\text{g}} \wedge {\text{l}} = {\text{l}}_{\text{g}} \wedge {\text{ts}} = {\text{ts}}_{\text{g}} } \hfill \\ \end{array} $$

Example 7.

Our goal (Alice, Write_O1, A1 building, Afternoon) can be translated as

$$ \exists {\text{u}},{\text{ r}},{\text{ l}},{\text{ ts}}.{\text{ re}}\left( {{\text{r}},{\text{ l}},{\text{ ts}}} \right) \wedge {\text{ua}}\left( {{\text{u}},{\text{ r}},{\text{ l}},{\text{ ts}}} \right) \wedge {\text{u }} = {\text{ Alice}} \wedge {\text{r }} = {\text{ Write}}\_{\text{O1}} \wedge {\text{l }} = {\text{ A1 building}} \wedge {\text{ts }} = {\text{ Afternoon}} $$

After translating all the ASTRBAC policy to BSR, we need to do an AND operator on all the translated formula. If the result return true, then our goal is reachable, otherwise, it is unreachable. If the state is reachable, we know that our system is unsafe, otherwise, it is safe.

Evaluations.

We use real scenario test cases synthesized from [27], which contains university and hospital benchmark, and are widely used in security analysis community. For our testing, we randomly adding temporal and spatial to the test cases. Since this is the first analysis tool of ASTRBAC model, we cannot compare it with any previous tool. All our experiments performs on an Intel Core i7 CPU with 4 GB Ram running Ubuntu 12.04 LTS 32 bit. We run 2 experiments with our test cases. Our first experiments run 15 times with different goals and calculate the average time for each test cases, the results is in Table 1. The first column shows our test case names; test cases 1 to 6 is our simple test cases created to test this program, test cases from 7 to 12 is taken from hospitals sets, test cases from 13 to 16 were taken from university sets. Each config contains 3 number representing max roles, max locations and max time slots in our STRBAC. The number of actions contain the number of administrative actions in ASTRBAC policies. We configure our experiment with maximum number of roles, locations and time slots.

Table 1. Our first experimental results
Full size table

In our second experiments, we use a simple test cases without spatial temporal constrains, set 16 for the maximum number of roles and 10 for the maximum number of time slots. Then, we run these test with randomly added locations each time to the test cases to get their average run time in Table 2 and Fig. 2.

Table 2. Our second experimental results with different locations
Full size table
Fig. 2.
figure 2

Our average run time with different locations

Full size image

After that, we create others test cases, set 16 for the maximum number of roles, set 5 for maximum number of locations. We run these test cases 5 times and add random time slots each time to the test cases to get their average run time shows in Table 3 and Fig. 3.

Table 3. Our second experimental results with different time slots
Full size table
Fig. 3.
figure 3

Our average run time with different time slots

Full size image

In our first experiments, we can assume that as the number of actions in ASTRBAC keep increasing, the runtime is affected and increased too. In our second experiments, we can assume that the increase in the number of time slots and the location does not affect the run time of our system. According to this result, we can conclude that more works need to be done for our solutions to get the answer faster when the number of actions keep increasing. We plan to improve this version in future works using some heuristics and functions supported in MCMT.

5 Conclusion

In this paper, we propose techniques using SMT-based model checker approach to solve the reachability problem in ASTRBAC. We also design a translation technique for ASTRBAC policies using First Order Logic.

As future works, we plan to design and apply heuristics to reduce the state exploration problem and speed up our approach in STRBAC by focusing only on the actions that may lead STRBAC to an unsafe state and using some functions provided in our SMT-based model checker such as the capability of tracking the visited states for later use.