Automated and efficient analysis of administrative temporal RBAC policies with role hierarchies

Abstract

Temporal role-based access control models support the specification and enforcement of several temporal constraints on role enabling, role activation, and temporal role hierarchies among others. In this paper, we define three mappings that preserve the solutions to a class of policy problems: they map security analysis problems in presence of static temporal role hierarchies to problems without them. We show how our mappings can be used to extend the capabilities of a tool for the analysis of administrative temporal role-based access control policies to reason in presence of temporal role hierarchies. We carried out an experimental evaluation with a prototype implementation, which highlighted that one of the proposed mappings behaves better than the other two. To the best of our knowledge, ours is the first tool capable of reasoning with (static) temporal role hierarchies.

Keywords

Safety analysis administrative temporal RBAC static role hierarchies access control scheme security mapping

1. Introduction

Modern information systems hold sensitive information that authorized users need to access in order to do their work and unauthorized users want to access for personal profit. The most important mechanism to prevent unintended disclosure of sensitive information is Access Control (AC) [13], which is the process of mediating every request to data and services maintained by a system and determining whether the request should be granted or denied. By doing this, AC supports the protection of data and services (generically called resources) against unauthorised disclosure (confidentiality) and intentional or accidental unauthorised changes (integrity), while – at the same time – ensuring their accessibility by authorised users when needed (availability).

Once security policies are defined, they need to be maintained and updated according to evolving protection requirements dictated by the rapidly changing environments in which organizations operate. Usually, a policy changes as an organization modifies its structure or in order to correct some discrepancies that have been detected between the intended protection requirements and those that are actually supported by the policies. The actions that modify the policies are called administrative actions and are usually carried out by a selected sub-set of the members of the organization, called administrators or security officers. The fact that the vast majority of today’s IT systems is distributed further complicates the problem of policy administration. Large and heterogeneous IT systems include several administrators, and thus the goal is not only to have a policy that corresponds to the intended protection requirements, but also to ensure that the policy is only modified by the administrators who are allowed to do so. Indeed, permissions to perform administrative actions must be restricted since security officers can only be partially trusted. Some of them may collude to, inadvertently or maliciously, modify an access control policy P to a new one $P^{'}$ so that a permission p to perform some sensitive action is leaked to a user u (i.e., u was not in possession of p under policy P but u has permission p under policy $P^{'}$ ).

Taking into consideration the effect of all possible sequences of administrative actions transforming P into $P^{'}$ is a computationally expensive task. Thus, push-button analysis techniques are needed to identify safety issues, i.e., whether permissions can be leaked to users. This is known as the safety problem [17], which amounts to establishing whether there exists a (finite) sequence of administrative actions, selected from a set of available ones, that, applied to a given initial policy, yield a policy in which a certain permission is leaked. Several important policy analysis problems can be reduced to the safety problem, e.g., deciding if the set of users having a given permission is a subset of that having another permission (containment), computing the minimal sets of permissions that a user should have so as to make another policy reachable by means of a finite sequence of administrative actions (weakest preconditions), and other problems (see, e.g., [15] for reductions). This makes automated techniques capable of solving safety problems even more valuable so as to be able to understand the subtle interplay among the actions performed by several administrators.

Unfortunately, the safety problem is – in general – undecidable [17]. To overcome this issue, two alternative approaches are available: either (a) identify a fragment of the access control policies admitting a decision procedure for a restricted version of the safety problem or (b) consider unrestricted policies and design heuristic (albeit incomplete) methods capable of solving practically relevant instances of the general safety problem. For instance, several techniques for alternative (a) have been proposed for administrative models of Role-Based Access Control (RBAC) policies [33] as witnessed by a long stream of papers, e.g., [1,3,6,7,15,18,21,24,28,31,37,38,43]; whereas alternative (b) has been less investigated (see, e.g., [4,5]).

In this work, we take alternative (a) to study the safety analysis problem for an extension of RBAC with temporal constraints [9,20]. We do not consider alternative (b) because of two reasons. First, the expressiveness of the access control policies in [9,20] greatly complicates the task of designing heuristics capable of solving practical instances of the generic safety problem. Second, three proposals [29,35,40] have been recently put forward to automatically solve restricted versions of the safety problems for administrative temporal RBAC policies; these proposals strike a good balance between expressiveness and automation by defining a simplified version of the temporal RBAC model in [20]. Indeed, such a simplified model – while taking into consideration periodicity constraints on role enabling and role activation – disregards other features of the model in [20], such as duration constraints and role hierarchies. As a consequence, none of the works [29,35,40] can deal with these core features, thereby limiting the scope of applicability of the proposed techniques for safety analysis.

1.1. Contributions

In this paper, we alleviate this limitation by extending available automated techniques for the safety analysis of temporal RBAC policies to take into account temporal role hierarchies. We achieve this by making the following three contributions.

We propose a formal model of administrative temporal RBAC policies with static temporal role hierarchies as an extension of the one proposed in [29] (which, as observed in [35], is a syntactic extension of the one proposed in [40]). The starting point of our extension is the notion of role hierarchy in RBAC [33], formalized as a partial order. The idea is to extend it to a collection of partial orders indexed over time intervals during which the hierarchies are assumed to hold. It is then possible to extend the temporal constraints on role activation and role enabling to take into account a temporal role hierarchy.

Modelling temporal role hierarchies as an extension of role hierarchies in RBAC allows us to extend a well-known technique [38] for eliminating role hierarchies from RBAC policies to temporal RBAC policies. The idea is to modify the administrative actions so as to make explicit any reference to the roles left implicit in a hierarchy and eliminate the need to consider the hierarchy. As a consequence, available techniques for safety analysis of administrative temporal RBAC policies without role hierarchies (such as [29]) can be used. We elaborate this idea further and present two additional translations that address the computational overhead introduced by the first translation.

Finally, we integrate a prototype of the three translations defined above in the tool asaspTIME [29] and carry out an experimental comparison of its performance. For the latter, we use synthetic benchmarks obtained by adding randomly generated temporal role hierarchies to the administrative temporal policies used in previous work [29] and based on realistic policies. This way of creating benchmarks is current practice for the evaluation of the scalability of tools for safety analysis.1

¹
As in many other papers in the literature (see, e.g., [1,15,18,38,40,43]), the evaluation is based on benchmarks derived from synthetic policies. In many cases, these are generated by identifying a realistic policy (e.g., for a bank or a hospital) together with some parameters that can be increased so that larger and larger instances of the same policy can be generated. Indeed, the goal is to evaluate the scalability of the proposed techniques. Unfortunately, the significance of the experimental results obtained in this way is debatable. The results reported in this paper suffer from the same problem. We believe that a community effort is needed to build up a common database of benchmarks, derived from real-world policies, that can be used to evaluate and compare old and new analysis techniques. Similar initiative in other fields (e.g., SAT/SMT solving (http://www.satlive.org and http://www.smtlib.org), Planning (http://ipc.icaps-conference.org) and Verification (http://sv-comp.sosy-lab.org/2014)) have greatly contributed to their advance. We believe this is a great opportunity also for increasing the impact of the safety analysis of access control policies in security. We hope that these remarks will stimulate further discussion and work in the community.

The extended version of asaspTIME is the first tool capable of reasoning in presence of temporal role hierarchies striking a good trade-off between scalability and precision with which the semantics of the temporal RBAC model is considered.

We develop our results in the framework of access control schemes proposed in [39]. In this context, the three translations that we define to eliminate temporal role hierarchies correspond to particular security mappings between access control schemes in terms of [39], and their correctness can be shown by standard techniques discussed in that paper.2

This paper is an extended version of [30]. Highlights of the extension include:

the complete formalization of the model for administrative temporal RBAC policies with static temporal role hierarchies (Section 3),

several examples illustrating the formal notions that we introduce,

the proofs of the correctness of the three translations to eliminate temporal role hierarchies (in Section 4.1.3, Section 4.2.3 and Section 4.3), and

a description of the architecture of the asaspTIME tool extended with the three security mappings (Section 5.1),

a discussion about the application of our approach to the analysis of policies with dynamic temporal role hierarchies (Section 7).

Plan of the paper. In Section 2, we introduce the notions of access control schemes and security mappings between them (adapted from [39]). We illustrate these notions by formalizing standard administrative RBAC (ARBAC) policies with and without role hierarchies. In Section 2.1, we define ARBAC Flat and then, in Section 2.2, we recast a known technique to pre-process away role hierarchies as a security mapping. In Section 3, we define administrative temporal RBAC policies (ATRBAC) with Static Temporal Hierarchies as the access control scheme $ATRBACH$ . In Section 4, we define three translations to eliminate temporal role hierarchies as three security mappings from $ATRBACH$ and show their correctness by proving how safety problems for $ATRBACH$ can be transformed (preserving solutions) to safety problems for temporal RBAC policies without role hierarchies. The main difficulty in these proofs is to show that the mappings correctly take into account the interplay among temporal role hierarchies, role enabling constraints, and role activation constraints. In Section 5, we summarize the technique on which asaspTIME is based, how it has been extended to integrate an implementation of the mappings introduced in Section 4, and we present an experimental evaluation of the prototype on a set of synthetic benchmarks. In Section 6, we discuss related work and, finally, in Section 7, we draw conclusions and discuss future work (in particular, we explain how to extend the approach proposed in this work to handle the dynamic temporal role hierarchies considered in [41]).

To ease reading, in Table 1 we give a roadmap for the main notions considered in the paper.

Table 1

A roadmap for the main notions considered in the paper

Notion	Description	Location
Access control scheme	$⟨ Γ, Q, ⊢, Ψ ⟩$ , where Γ is the set of states, Q is a set of queries, $⊢ : Γ \times Q \to {true, false}$ is the query answering relation, and Ψ is a set of transition rules	Definition 1, Section 2
Access control system	$(γ, ψ)$ , where $γ \in Γ$ and $ψ \subseteq Ψ$	Definition 2, Section 2
SAI: Security analysis instance	$⟨ γ, q, ψ ⟩$ , where $γ \in Γ$ , $q \in Q$ and $ψ \subseteq Ψ$ ; asks whether there exists $γ^{'} \in Γ$ such that $γ^{'}$ is ψ-reachable from γ and $γ^{'} ⊢ q$	Definition 2, Section 2
RBAC policy	$(U, R, P, UA, PA)$ , where $UA \subseteq U \times R$ associated users to roles and $PA \subseteq R \times P$ associates roles to permissions	Definition 3, Section 2.1
Pre-condition C	A finite set of signed roles of the forms $+ r$ or $- r$ for $r \in R$	Definition 4, Section 2.1
Pre-condition C	$u ⊧_{γ} C$	Definition 5, Section 2.1
RBAC policy with hierarchy	$(U, R, P, UA, PA, RH)$	Definition 10, Section 2.2.1
Hierarchical TRBAC policy	$π = (U, R, P, RS, TUA, PA, TRH)$ , where $RS$ is the role status relation, $TUA$ is the temporal user-role assignment relation and $TRH$ is a temporal role hierarchy	Definition 14, Section 3.1
(Temporal) administrative action	$(ty, C_{a}, s_{rule}, C, s_{r}, r)$ , where $ty$ is the type of the action, $C_{a}$ is the administrative pre-condition and C is the simple pre-condition, $s_{rule}$ and $s_{r}$ are schedules, and r is the target role	Definition 16, Section 3.2
ARBAC Flat: administrative RBAC without role hierarchy	$ARBACF = ⟨ Γ_{ARBACF}, Q_{ARBACF}, ⊢_{ARBACF}, Ψ_{ARBACF} ⟩$	Section 2.1
ARBAC with role hierarchy	$ARBACH = ⟨ Γ_{ARBACH}, Q_{ARBACH}, ⊢_{ARBACH}, Ψ_{ARBACH} ⟩$	Section 2.2.1
Administrative Temporal RBAC with Static Role Hierarchies	$ATRBACH = ⟨ Γ_{ATRBACH}, Q_{ATRBACH}, ⊢_{ATRBACH}, Ψ_{ATRBACH} ⟩$	Section 3
ATRBAC Flat: Administrative Temporal RBAC without Static Role Hierarchies	$ATRBACF = ⟨ Γ_{ATRBACF}, Q_{ATRBACF}, ⊢_{ATRBACF}, Ψ_{ATRBACF} ⟩$	Section 4.1.1
$ican_assign$ actions simulating temporal role hierarchies	$(ican_assign, r^{'}, ts, r)$ where $r^{'}$ and r are roles, $ts$ is a time slot	Section 4.2
Administrative Temporal RBAC with using $ican_assign$ actions	$ATRBACL = ⟨ Γ_{ATRBACL}, Q_{ATRBACL}, ⊢_{ATRBACL}, Ψ_{ATRBACL} ⟩$	Section 4.2.1
$mican_assign$ actions simulating the execution of a sequence of $ican_assign$ actions in one shot	$(mican_assign, r, ts, {Junior}_{t s} (r))$ where r is a role, ${Junior}_{t s} (r)$ is the set of junior roles of r, and $ts$ is a time slot	Section 4.3
Administrative Temporal RBAC with using $mican_assign$ actions	$ATRBACM = ⟨ Γ_{ATRBACM}, Q_{ATRBACM}, ⊢_{ATRBACM}, Ψ_{ATRBACM} ⟩$	Section 4.3
Security mappings	$σ : (Γ_{A} \times Ψ_{A}) \cup Q_{A} \to (Γ_{B} \times Ψ_{B}) \cup Q_{B}$ from $A = ⟨ Γ_{A}, Q_{A}, ⊢_{A}, Ψ_{A} ⟩$ to $B = ⟨ Γ_{B}, Q_{B}, ⊢_{B}, Ψ_{B} ⟩$ maps every $(γ_{A}, ψ_{A})$ to a $(γ_{B}, ψ_{B})$ and every $q_{A}$ to a $q_{B}$	Definition 8, Section 2.2
	$σ_{H 2 F} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = ⟨ γ_{F}, q_{F}, ψ_{F} ⟩$	Definition 11, Section 2.2.1
	$τ_{H 2 F} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = (⟨ γ_{F}, q_{F}, ψ_{F} ⟩)$ (temporalized version of $σ_{H 2 F}$ )	Section 4.1.2
	$τ_{H 2 L} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = ⟨ γ_{L}, q_{L}, ψ_{L} ⟩$ (linear mapping)	Section 4.2.2
	$τ_{H 2 M}$ (multi-target mapping)	Section 4.3

2. Access control schemes

We introduce the notions of access control schemes, access control systems, and security analysis instances by adapting them from [39].

Definition 1.
An access control scheme is a state-transition system $⟨ Γ, Q, ⊢, Ψ ⟩$ , where Γ is the set of states, Q is a set of queries, $⊢ : Γ \times Q \to {true, false}$ is the query answering relation, and Ψ is a set of transition rules.

We write $γ \mapsto_{ψ} γ^{'}$ when a transition from $γ \in Γ$ to $γ^{'} \in Γ$ is allowed by a rule in $ψ \subseteq Ψ$ . We use $\mapsto_{ψ}^{}$ to denote the reflexive and transitive closure* of $\mapsto_{ψ}$ , and when $γ \mapsto_{ψ}^{} γ^{'}$ we say that $γ^{'}$ is ψ-reachable* from γ (or simply “reachable from γ” when ψ is clear from the context).
Definition 2.
Consider an access control scheme $⟨ Γ, Q, ⊢, Ψ ⟩$ .
An access control system is a pair $(γ, ψ)$ , where $γ \in Γ$ and $ψ \subseteq Ψ$ .

A security analysis instance (SAI) is the triple $⟨ γ, q, ψ ⟩$ , where $γ \in Γ$ , $q \in Q$ and $ψ \subseteq Ψ$ , and asks whether there exists $γ^{'} \in Γ$ such that $γ^{'}$ is ψ-reachable from γ and $γ^{'} ⊢ q$ .
When the answer to the query encoded by a SAI is positive, we say that it is solvable; otherwise, it is unsolvable.

In the following, we focus on role-based access control schemes with and without role hierarchies. To clarify which case we are considering, we append at the end of the name of an access control scheme
the letter “F” to denote the scheme for the standard (flat) model without role hierarchies,

the letter “H” to denote the scheme for the standard model with role hierarchies.

2.1. Administrative RBAC without role hierarchy: ARBAC flat

We now formalize the access control scheme $\begin{matrix} ARBACF = ⟨ Γ_{ARBACF}, Q_{ARBACF}, ⊢_{ARBACF}, Ψ_{ARBACF} ⟩ \end{matrix}$ corresponding to the ARBAC model without role hierarchy in [38].

Definition 3.
Let U, R and P respectively be sets of users, roles and permissions.

An RBAC policy is a tuple $(U, R, P, UA, PA)$ , where users are associated to roles by a binary relation $UA \subseteq U \times R$ and roles are associated to permissions by a binary relation $PA \subseteq R \times P$ .

If $(u, r) \in UA$ , then we say that a user u is a member of role r in the RBAC policy $γ = (U, R, P, UA, PA)$ , and if there exists a role $r \in R$ such that $(r, p) \in PA$ and u is a member of r, then we say that u has permission p in γ.

We define $Γ_{ARBACF}$ to be the set of all RBAC policies.

RBAC policies need to be maintained according to the evolving needs of organizations. For flexibility and scalability, large systems usually require several administrators, and thus there is a need not only to have a consistent RBAC policy, but also to ensure that the policy is only modified by administrators who are authorized to do so. One of the most popular administrative frameworks is Administrative RBAC (ARBAC) [11], which controls how RBAC policies may evolve through administrative actions that assign or revoke user memberships into roles, i.e., they can only update the relation $UA$ while $PA$ is constant. Since administrators can be only partially trusted, administration privileges must be limited to selected parts of the RBAC policies, called administrative domains. An administrative domain is specified by a pre-condition defined as follows.
Definition 4.
A pre-condition is a finite set of signed roles of the forms $+ r$ or $- r$ for $r \in R$ .

Permission to assign users to roles is specified by a ternary relation $can_assign$ containing tuples of the form $(C_{a}, C, r)$ , where $C_{a}$ (called administrative) and C (called simple) are pre-conditions, and r is a role (called target). Permission to revoke users from roles is then specified by a binary relation $can_revoke$ containing pairs $(C_{a}, r)$ . Note that $can_revoke$ is only binary because simple pre-conditions are useless when revoking roles (see, e.g., [38]).
Definition 5.
A user $u \in U$ satisfies a pre-condition C with respect to a given policy $γ = (U, R, P, UA, PA)$ , written as $u ⊧_{γ} C$ , if for each $ℓ \in C$ ,
u is a member of $r \in R$ when ℓ is $+ r$ , or

u is not a member of $r \in R$ when ℓ is $- r$ .
We omit the policy γ when it is clear from the context.

Let $Ψ_{ARBACF}$ be the disjoint union of the administrative actions in $can_assign$ and $can_revoke$ (in the following, we abbreviate RBAC policies by the $UA$ relation since all other sets and relations remain constant). The effect of the administrative actions in $ψ \subseteq Ψ_{ARBACF}$ is given by the binary relation $\mapsto_{ψ}$ , which is defined as follows.
Definition 6.
$UA \mapsto_{ψ} {UA}^{'}$ iff there exist users $a, u \in U$ such that either
there exists $δ = (C_{a}, C, r_{t})$ in ψ with $a ⊧ C_{a}$ , $u ⊧ C$ , and ${UA}^{'} = UA \cup {(u, r_{t})}$ , or

there exists $δ = (C_{a}, r_{t})$ in ψ with $a ⊧ C_{a}$ , $u ⊧ {+ r_{t}}$ , and ${UA}^{'} = UA ∖ {(u, r_{t})}$ .

Note that in both cases in Definition 6 we also write $UA \mapsto_{δ} {UA}^{'}$ to emphasize that action $δ \in ψ$ causes the effect. We illustrate the definitions with an example inspired by the hospital scenario in [29].
Example 1.
Let $U = {u_{1}, u_{2}, u_{3}}$ , $R = {EMP (Employee), DDR (Day Doctor), NDR (Night Doctor), PRC (Practitioner), NRS (Nurse), HED (head), SEC (Secretary), CHR (Chairman)}$ , and let the set ψ contain the actions $\begin{array}{l} (1) & (CHR, {EMP, - NRS}, DDR) \in can_assign, \\ (2) & (CHR, {EMP}, NRS) \in can_assign, \\ (3) & (CHR, {NRS}, PRC) \in can_assign, \\ (4) & (CHR, SEC) \in can_revoke . \end{array}$ Assume that the current policy is $UA = {(u_{1}, CHR), (u_{2}, EMP), (u_{3}, DDR)}$ . Let us consider action (1): the administrative pre-condition is $C_{a} = {CHR}$ , the simple pre-condition is $C = {EMP, - NRS}$ , and the target role is $DDR$ . It is easy to check that:
User $u_{1}$ satisfies the administrative pre-condition $C_{a}$ since $(u_{1}, CHR) \in UA$ .

User $u_{2}$ satisfies the simple pre-condition C since $(u_{2}, EMP) \in UA$ and $(u_{2}, NRS) \notin UA$ .
Action (1) can be executed by administrator $u_{1}$ because of (i) and (ii). The effect of executing action (1) on the current state is that $UA \mapsto_{ψ} {UA}^{'}$ with ${UA}^{'} = UA \cup {(u_{2}, DDR)}$ .

Despite the restrictions imposed on administrative actions, it is very difficult to foresee if a subset of the security officers can maliciously (or inadvertently) assign to an untrusted user a role that enables the user to get access to security-sensitive resources. To understand if this is the case, we define the set $Q_{ARBACF}$ to contain queries of the form $(u_{g}, {R_{g}^{1}, \dots, R_{g}^{r}})$ , where $u_{g} \in U$ and $R_{g}^{i} \subseteq R$ for $i = 1, \dots, r ⩾ 1$ .
Definition 7.
For $γ \in Γ_{ARBACF}$ and $q = (u_{g}, {R_{g}^{1}, \dots, R_{g}^{r}}) \in Q_{ARBACF}$ , the query answering relation $⊢_{ARBACF}$ is defined as follows: $γ ⊢_{ARBACF} q$ iff $u_{g}$ is a member of each role of $R_{g}^{i}$ in the RBAC policy γ for some $i = 1, \dots, r$ .

A Security Analysis Instance (SAI) $⟨ γ, q, ψ ⟩$ for $γ \in Γ_{ARBACF}$ , $q \in Q_{ARBACF}$ , and $ψ \subseteq Ψ_{ARBACF}$ is the formalization in the framework of access control schemes (adapted from [39]) of the user-role reachability problem (for RBAC policies without role hierarchy) considered in [38], which amounts to checking if there exists $γ^{'} \in Γ_{ARBACF}$ such that $γ \mapsto_{ψ}^{*} γ^{'}$ and $γ^{'} ⊢_{ARBACF} q$ .
Example 2.
Let us consider again Example 1 and a query $q = (u_{2}, {{DDR, PRC}})$ ; note that we have only one set $R_{g}^{1} = {DDR, PRC}$ in the query. A SAI $(UA, q, ψ)$ is solvable by a sequence of actions $ω = (1), (2), (3)$ such that $\begin{matrix} UA \mapsto_{(1)} {UA}^{'} \mapsto_{(2)} {UA}^{″} \mapsto_{(3)} {UA}^{‴}, \end{matrix}$ where ${UA}^{'} = UA \cup {(u_{2}, DDR)}$ , ${UA}^{″} = {UA}^{'} \cup {(u_{2}, NRS)}$ and ${UA}^{‴} = {UA}^{″} \cup {(u_{2}, PRC)}$ .

We do not use the original formulation of the user-role reachability problem in [38] but rather rephrase it as a SAI since this allows for the use of the notion of security mapping (introduced below), following the approach proposed in [39]. We can then show that searching for the solutions of a SAI $sai$ is equivalent to searching for the solutions of a SAI obtained by applying a security mapping to $sai$ . To illustrate this, below we show how user-role reachability problems for ARBAC policies with role hierarchies can be solved by transforming these into user-role reachability problems for ARBAC policies without role hierarchies.
2.2. Security mappings

Definition 8.
Given two access control schemes $A = ⟨ Γ_{A}, Q_{A}, ⊢_{A}, Ψ_{A} ⟩$ and $B = ⟨ Γ_{B}, Q_{B}, ⊢_{B}, Ψ_{B} ⟩$ , a security mapping $σ : (Γ_{A} \times Ψ_{A}) \cup Q_{A} \to (Γ_{B} \times Ψ_{B}) \cup Q_{B}$ from A to B is a function that maps every access control system $(γ_{A}, ψ_{A})$ in A to a $(γ_{B}, ψ_{B})$ in B, and every query $q_{A}$ in A to a $q_{B}$ in B.

The mapping σ from A to B extends to SAIs as follows. Definition 9.
$σ (⟨ γ_{A}, q_{A}, ψ_{A} ⟩) = ⟨ γ_{B}, q_{B}, ψ_{B} ⟩$ , where $σ (γ_{A}, ψ_{A}) = ⟨ γ_{B}, ψ_{B} ⟩$ and $σ (q_{A}) = q_{B}$ , for every $⟨ γ_{A}, q_{A}, ψ_{A} ⟩$ in A. The mapping σ is security-preserving whenever every SAI $⟨ γ_{A}, q_{A}, ψ_{A} ⟩$ in A is solvable iff $σ (⟨ γ_{A}, q_{A}, ψ_{A} ⟩)$ is so.

2.2.1. From ARBAC with role hierarchy ( $ARBACH$ ) to ARBAC without role hierarchy ( $ARBACF$ )

We now formalize the access control scheme $\begin{matrix} ARBACH = ⟨ Γ_{ARBACH}, Q_{ARBACH}, ⊢_{ARBACH}, Ψ_{ARBACH} ⟩ \end{matrix}$ corresponding to the ARBAC model with role hierarchy in [38]. $ARBACH$ extends $ARBACF$ by considering a role hierarchy $RH$ in the RBAC policy to reflect the natural structure of an organization, and makes the specification of policies more compact by requiring that one role may implicitly include the permissions that are associated with other roles that are less senior according to $RH$ . Formally, $RH$ is a partial order on R, where $(r_{1}, r_{2}) \in RH$ means that $r_{1} \in R$ is more senior than $r_{2} \in R$ .

Definition 10.
An RBAC policy with hierarchy is a tuple $(U, R, P, UA, PA, RH)$ .

We say that a user u is a member of role r in $(U, R, P, UA, PA, RH)$ when there exists role $r^{'} \in R$ such that $(r^{'}, r) \in RH$ and $(u, r^{'}) \in UA$ ; note that this is different from the role membership in $ARBACF$ in which we do not take into consideration the role hierarchy.

User u has permission p in $(U, R, P, UA, PA, RH)$ if there exists a role $r \in R$ such that $(r, p) \in PA$ and u is a member of r.

We are now ready to define $ARBACH$ :
$Γ_{ARBACH}$ is the set of all RBAC policies with hierarchy;

$⊢_{ARBACH} = ⊢_{ARBACF}$ ;

$Ψ_{ARBACH} = Ψ_{ARBACF}$ with the proviso that the role membership relation is interpreted by taking into account the role hierarchy;

$Q_{ARBACH}$ is the set of queries of the form $(u_{g}, R_{g})$ with $u_{g} \in U$ and $R_{g} \subseteq R$ .
The definition of $\mapsto_{ARBACH}$ is the same as that of $\mapsto_{ARBACF}$ (cf. Definition 6) with the difference that, in the definition of $u ⊧ C$ , the fact that u is a member or not of a signed role in C is interpreted with respect to the role hierarchy $RH$ in the RBAC policy.
Example 3.
Consider again the sets U, R, ψ, and the current policy $UA$ in Example 1. Assume a role hierarchy $RH$ obtained by taking the closure of the set ${(HED, DDR), (DDR, NRS), (NDR, EMP), (CHR, SEC)}$ under reflexivity, antisymmetry, and transitivity. It is easy to see that:
User $u_{3}$ is an explicit member of role $DDR$ since $(u_{3}, DDR) \in UA$ .

User $u_{3}$ is an implicit member of role $NRS$ since $(u_{3}, DDR) \in UA$ and $(DDR, NRS) \in RH$ .

User $u_{3}$ does not satisfy the simple pre-condition $C = {EMP, - NRS}$ in action (1) in ψ because $u_{3}$ is a member of role $NRS$ with respect to the role hierarchy $RH$ .

Like for $ARBACF$ , a SAI $⟨ γ, q, ψ ⟩$ for $γ \in Γ_{ARBACH}$ , $q \in Q_{ARBACH}$ and $ψ \subseteq Ψ_{ARBACH}$ is the formalization in the framework of access control schemes (adapted from [39]) of the user-role reachability problem (for RBAC policies with role hierarchy) considered in [38]. As anticipated above, the motivation for doing this is the possibility to define and reason about a security mapping relating the SAIs based on $ARBACH$ with those based on $ARBACF$ . Note that the set $Q_{ARBACH}$ of queries can be seen as a sub-set of $Q_{ARBACF}$ in which only one set of roles is given.

In fact, every SAI for $ARBACH$ can be transformed into one for $ARBACF$ such that the latter is solvable iff the former is so. For this, based on a transformation proposed in [34], we define a security-preserving mapping $σ_{H 2 F}$ whose aim is to make the effects of inherited role membership explicit. We will use the abbreviations $\begin{array}{l} {Senior}_{RH} (r) = {r^{'} \in R ∣ (r^{'}, r) \in RH}, \\ {Senior}_{RH} ({r_{1}, \dots, r_{n}}) = {Senior}_{RH} (r_{1}) \times \dots \times {Senior}_{RH} (r_{n}), \end{array}$ where $r_{i} \in R$ for $i = 1, \dots, n$ . We also introduce the notation $C^{+}$ ( $C^{-}$ , respectively) for the set of positive (negative, respectively) roles in a set $C \subseteq R$ .
Definition 11.
We define $σ_{H 2 F}$ that transforms a SAI $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ into $ARBACH$ to a SAI $⟨ γ_{F}, q_{F}, ψ_{F} ⟩$ in $ARBACF$ , in symbols $\begin{matrix} σ_{H 2 F} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = ⟨ γ_{F}, q_{F}, ψ_{F} ⟩, \end{matrix}$ as follows:
$γ_{F} = (U, R, P, UA, PA)$ for $γ_{H} = (U, R, P, UA, PA, RH)$ ,

$q_{F} = (u_{g}, {{r_{g}^{1}, \dots, r_{g}^{m}} ∣ (r_{g}^{1}, \dots, r_{g}^{m}) \in {Senior}_{RH} (R_{g})})$ for $q_{H} = (u_{g}, R_{g})$ ,

$ψ_{F}$ is obtained from $ψ_{H}$ by applying the following two transformations, one after the other, with the proviso that $ψ_{H}^{'}$ and $ψ_{F}$ are the smallest relation such that

for each $(C_{a}, C, r_{t}) \in ψ_{H}$ : $(C_{a} \cup {- r_{a}^{'} ∣ - r_{a} \in C_{a} and r_{a}^{'} \in {Senior}_{RH} (r_{a})}, C \cup {- r^{'} ∣ - r \in C and r^{'} \in {Senior}_{RH} (r)}, r_{t}) \in ψ_{H}^{'}$ , and for each $(C_{a}, r_{t}) \in ψ_{H}$ : $(C_{a} \cup {- r_{a}^{'} ∣ - r_{a} \in C_{a} and r_{a}^{'} \in {Senior}_{RH} (r_{a})}, r_{t}) \in ψ_{H}^{'}$ ,

for each $(C_{a}^{+} \cup C_{a}^{-}, C^{+} \cup C^{-}, r_{t}) \in ψ_{H}^{'}$ : $({r_{a}^{1}, \dots, r_{a}^{k}} \cup C_{a}^{-}, {r^{1}, \dots, r^{l}} \cup C^{-}, r_{t}) \in ψ_{F}$ for $(r_{a}^{1}, \dots, r_{a}^{k}) \in {Senior}_{RH} (C_{a}^{+})$ and $(r^{1}, \dots, r^{l}) \in {Senior}_{RH} (C^{+})$ , and for each $(C_{a}^{+} \cup C_{a}^{-}, r_{t}) \in ψ_{H}^{'}$ : $({r_{a}^{1}, \dots, r_{a}^{k}} \cup C_{a}^{-}, r_{t}) \in ψ_{F}$ for $(r_{a}^{1}, \dots, r_{a}^{k}) \in {Senior}_{RH} (C_{a}^{+})$ .

Note that every SAI $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ in $ARBACH$ with $q_{H} = (u_{g}, R_{g})$ is mapped to one $⟨ γ_{F}, q_{F}, ψ_{F} ⟩$ in $ARBACF$ with $q_{F} = (u_{g}, {R_{g}^{1}, \dots, R_{g}^{r}})$ and $r ⩾ 1$ according to how many elements are in ${Senior}_{RH} (R_{g})$ . The idea is to ensure that if a role senior to $r_{g} \in R_{g}$ is reachable, then also $r_{g}$ is reachable. As a consequence, there is no need to transform also the target roles in the administrative actions. It is easy to show that any sequence of administrative actions for $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ can be transformed into one for $⟨ γ_{F}, q_{F}, ψ_{F} ⟩$ and vice versa as suggested in [34]. This entails the following theorem.
Theorem 1.
$σ_{H 2 F}$ is a security mapping.

Note that, in the worst case, $σ_{H 2 F}$ can increase the size of the SAI (cf. the transformation of the query and the conditions of administrative actions) by an exponential factor.
Example 4.
Consider the query $q_{H} = (u_{2}, {DDR, PRC})$ in Example 2, the role hierarchy $RH$ as in Example 3, the set $ψ_{H} = ψ$ and the current policy $UA$ as in Example 1. We illustrate how the security mapping $σ_{H 2 F}$ works as follows:
$q_{H}$ is transformed into $q_{F} = (u_{2}, {{DDR, PRC}, {HED, PRC}})$ because $HED$ is a senior role of $DDR$ with respect to $RH$ .

$ψ_{F}$ is obtained by transforming actions in $ψ_{H}$ as follows:

Action (1) is transformed into two actions:
(1′) $(CHR, {EMP, - NRS, - DDR}, DDR)$ and

(1″) $(CHR, {NDR, - NRS, - DDR}, DDR)$
since tuple $(NDR, EMP) \in RH$ .

Action (2) is transformed into two actions:
(2′) $(CHR, {EMP}, NRS)$ and

(2″) $(CHR, {NDR}, NRS)$
since tuple $(NDR, EMP) \in RH$ .

Action (3) is transformed into three actions:
(3′) $(CHR, {NRS}, PRC)$ ,

(3″) $(CHR, {DDR}, PRC)$ and

(3 $^{‴}$ ) $(CHR, {HED}, PRC)$
since tuples $(HED, DDR), (DDR, NRS) \in RH$ .
A SAI $⟨ UA, q_{F}, ψ_{F} ⟩$ is solvable by a sequence of actions $ω_{F} = (1^{'}), (2^{'}), (3^{'})$ such that $\begin{matrix} UA \mapsto_{(1^{'})} {UA}^{'} \mapsto_{(2^{'})} {UA}^{″} \mapsto_{(3^{'})} {UA}^{‴}, \end{matrix}$ where ${UA}^{'} = UA \cup {(u_{2}, DDR)}$ , ${UA}^{″} = {UA}^{'} \cup {(u_{2}, NRS)}$ , ${UA}^{‴} = {UA}^{″} \cup {(u_{2}, PRC)}$ .

We conclude this section by observing that Theorem 1 is a formalization in the framework of access control schemes of a result from [34]. This allows us not only to illustrate the main notions introduced above but also to prepare the ground for the definition of the first security mapping relating administrative temporal RBAC policies with and without temporal role hierarchies (cf. Section 4.1) that is inspired to $σ_{H 2 F}$ .
3. Administrative temporal RBAC with static role hierarchies: ATRBACH

We extend the ATRBAC model in [29] with static temporal role hierarchies to define the access control scheme $\begin{matrix} ATRBACH = ⟨ Γ_{ATRBACH}, Q_{ATRBACH}, ⊢_{ATRBACH}, Ψ_{ATRBACH} ⟩ . \end{matrix}$ We do this in several steps. First, we introduce a temporal extension to RBAC policies with role hierarchies (Section 3.1). Then, we define administrative actions for the temporal RBAC policies previously introduced (Section 3.2) together with their SAI (Section 3.3).

3.1. Temporal RBAC with static role hierarchies

Preliminarily, we introduce a simple model of time. The goal is to express authorization conditions that depend on temporal constraints, which are usually specified by means of periodically repeating time intervals, such as day/night-time intervals (two intervals repeating daily), hourly intervals (twenty-four intervals again repeating daily), or daily intervals (seven intervals repeating weekly).

Definition 12.
Let $T_{MAX}$ be a positive integer and a a non-negative integer such that $a + 1 ⩽ T_{MAX}$ . A time slot is a pair $(a, a + 1)$ and the set of all time slots is ${TS}_{T_{MAX}} = {(a, a + 1) ∣ 0 ⩽ a < T_{MAX}}$ . We write $TS$ in place of ${TS}_{T_{MAX}}$ when $T_{MAX}$ is clear from context.

To ease readability, we will use concrete time intervals, e.g., $(8 am, 4 pm)$ , $(4 pm, 12 am)$ and $(12 am, 8 am)$ to denote respectively the time slots $(0, 1)$ , $(1, 2)$ and $(2, 3)$ , where, in general, such time intervals need not have the same length.
Definition 13.
A time instant is a non-negative real number. A time instant t belongs to a time slot $(a, a + 1)$ , written as $t \in (a, a + 1)$ , iff $a ⩽ (t mod T_{MAX}) < a + 1$ .3
³
In the definition, we employ the usual modulo operator $mod$ , i.e., $t^{'} = t mod T_{MAX}$ iff there exists a non-negative integer k such that $t = t^{'} + k \cdot T_{MAX}$ .

Below, we assume $T_{MAX}$ to be given so that the set $TS$ of all time slots is fixed.

A Temporal RBAC policy γ with static temporal role hierarchies extends an RBAC policy in three respects:

TRBAC adds the role status relation $RS \subseteq R \times TS$ , which is such that $(r, ts) \in RS$ iff role r becomes enabled (i.e., a user can acquire the permissions associated to r, via $PA$ ) during time slot $ts$ ; we then say that r is enabled at all time instants in $ts$ .

The user-role assignment relation $UA$ is replaced by the temporal user-role assignment $TUA \subseteq U \times R \times TS$ , which makes the association of users with roles dependent on time slots so that (enabled) roles become active when users acquire the permissions assigned to roles in a session.

We consider temporal constraints on the role hierarchy that restrict the time during which the hierarchy is valid but cannot change its structure by modifying the relative positions of roles. In other words, we assume static role hierarchies in which the temporal constraints on role enabling determine whether the role hierarchy will provide inheritance for a role at a given time. This type of role inheritance is called activation-semantics in, e.g., [20], and can be formalized as follows. A relation $TRH \subseteq R \times R \times TS$ is a (static) temporal role hierarchy iff ${TRH}_{ts}$ is a partial order on the set R of roles for each time slot $ts$ in $TS$ , where ${TRH}_{ts} = {(r^{'}, r) ∣ (r^{'}, r, ts) \in TRH}$ . Intuitively, $(r^{'}, r, ts) \in TRH$ means that $r^{'}$ is more senior than r during time slot $ts$ .
Definition 14.
A hierarchical TRBAC policy is a tuple $π = (U, R, P, RS, TUA, PA, TRH)$ , where U, R, P, and $PA$ are as for RBAC policies, $RS$ is the role status relation, $TUA$ is the temporal user-role assignment relation and $TRH$ is a temporal role hierarchy.

We say that user u is a member of role r (with respect to the TRBAC policy π) in time slot $ts$ when there exists $r^{'} \in R$ such that $(r^{'}, r, ts) \in TRH$ and $(u, r^{'}, ts) \in TUA$ . User u has permission p in π if there exists a role $r \in R$ such that $(r, p) \in PA$ and u is a member of role r in a certain time slot $ts$ .

We define $Γ_{ATRBACH}$ to be the set of all hierarchical TRBAC policies.

We illustrate the definitions by extending the hospital scenario considered in Example 1 with time constraints. Example 5.
We assume that the hospital in Example 1 works for 24 hours (i.e., $T_{MAX} = 24$ ) with the set $TS$ containing three time slots: ${ts}_{1}$ contains time instants from 8 am to 4 pm; ${ts}_{2}$ is from 4 pm to 12 am; and ${ts}_{3}$ is from 12 am to 8 am. Let us consider the TRBAC policy $(U, R, P, {RS}_{0}, {TUA}_{0}, PA, TRH)$ , where $\begin{array}{l} {RS}_{0} = \{\begin{matrix} (CHR, {ts}_{1}), (CHR, {ts}_{2}), (DDR, {ts}_{2}), (NDR, {ts}_{3}) \end{matrix}\}, \\ {TUA}_{0} = \{\begin{matrix} (u_{1}, CHR, {ts}_{1}), (u_{1}, CHR, {ts}_{2}), (u_{1}, CHR, {ts}_{3}), (u_{2}, NRS, {ts}_{3}) \end{matrix}\}, \\ TRH = \{\begin{matrix} (CHR, SEC, {ts}_{1}), (CHR, SEC, {ts}_{2}), (NRS, EMP, {ts}_{3}), (CHR, SEC, {ts}_{3}), \\ (NDR, PRC, {ts}_{3}), (HED, NDR, {ts}_{3}) \end{matrix}\} . \end{array}$ It is easy to see that:
Role $CHR$ is enabled during time slot ${ts}_{1}$ since $(CHR, {ts}_{1}) \in {RS}_{0}$ .

User $u_{1}$ is an (explicit) member of role $CHR$ during time slot ${ts}_{1}$ since $(u_{1}, CHR, {ts}_{1}) \in {TUA}_{0}$ .

Role $CHR$ is more senior than role $SEC$ during time slot ${ts}_{1}$ since $(CHR, SEC, {ts}_{1}) \in TRH$ .

User $u_{1}$ is an implicit member of role $SEC$ during time slot ${ts}_{1}$ since he is an explicit member of role $CHR$ during ${ts}_{1}$ and $(CHR, SEC, {ts}_{1}) \in TRH$ .

3.2. Administrative actions for temporal RBAC policies with static role hierarchies

In the following, we assume the definition of pre-condition given in Section 2 for ARBAC actions (cf. Definition 4). We introduce the notion of a schedule as a set of time slots and say that a time instant t belongs to schedule s (in symbols, $t \in s$ ) iff there exists a time slot $ts$ in s such that t belongs to $ts$ .

Definition 15.
Let $π = (U, R, P, RS, TUA, PA, TRH)$ be a hierarchical TRBAC policy, $ts$ a time slot, C a pre-condition, u a user, t a time instant and s a schedule.
Time slot $ts$ satisfies C under $RS$ (in symbols, $ts ⊧_{RS} C$ ) iff r is enabled at $ts$ for each $+ r \in C$ , and r is not enabled at $ts$ for each $- r \in C$ .

Schedule s satisfies C under $RS$ (in symbols, $s ⊧_{RS} C$ ) iff $ts ⊧_{RS} C$ for each $ts \in s$ .

User u and time slot $ts$ satisfy C under $TUA$ (in symbols, $u, ts ⊧_{TUA} C$ ) iff u is a member of r in $ts$ for each $+ r \in C$ , and u is not a member of r in $ts$ for each $- r \in C$ .

User u and schedule s satisfy C under $TUA$ (in symbols, $u, s ⊧_{TUA} C$ ) iff $u, ts ⊧_{TUA} C$ for each $ts \in s$ .

u and $ts$ satisfy C under $RS$ and $TUA$ at time instant t (in symbols, $u, ts ⊧_{RS, TUA}^{@ t} C$ ) iff $t \in ts$ , $ts ⊧_{RS} C$ and $u, ts ⊧_{TUA} C$ .

u and s satisfy C under $RS$ and $TUA$ at time instant t (in symbols, $u, s ⊧_{RS, TUA}^{@ t} C$ ) iff $t \in s$ , $s ⊧_{RS} C$ , and $u, s ⊧_{TUA} C$ .

We introduce two kinds of possible administrative actions: those that enable or disable a role r by modifying the time slots associated to r in $RS$ , and those that change the time slots constraining a user-role association in $TUA$ .
Definition 16.
A (temporal) administrative action has the form $(ty, C_{a}, s_{rule}, C, s_{r}, r)$ , where $ty$ is the type of the action (i.e., $can_enable$ , $can_disable$ , $can_assign$ or $can_revoke$ ), $C_{a}$ is the administrative pre-condition and C is the simple pre-condition, $s_{rule}$ and $s_{r}$ are schedules, and r is the target role.

An administrative action of type $can_enable$ (respectively, $can_disable$ ) enables (respectively, disables) a role associated to some time slot in $RS$ , while leaving unchanged $TUA$ . An administrative action of type $can_assign$ (respectively, $can_revoke$ ) assigns (respectively, revokes) a role associated to a user for some time slot in $TUA$ , while leaving $RS$ unchanged. We define $Ψ_{ATRBACH}$ to be the set of all (temporal) administrative actions.

Administrative actions are executed instantaneously and are interleaved with time-passing transitions for incrementing time. Formally, the effect of the administrative actions in $ψ \subseteq Ψ_{ATRBACH}$ is given by the binary relation $\mapsto_{ATRBACH}$ , which is defined as follows, where – since actions affect only relations $RS$ and $TUA$ together with the time instant t – we write $(RS, TUA, t)$ to abbreviate a state $((U, R, P, RS, TUA, PA), t)$ in $Γ_{ATRBACH}$ :
Definition 17.
$(RS, TUA, t) \mapsto_{ψ} ({RS}^{'}, {TUA}^{'}, t^{'})$ iff either
${RS}^{'} = RS$ , $TUA = TUA$ , and $t^{'} > t$ or

there exist $ac = (ty, C_{a}, s_{rule}, C, s_{r}, r) \in ψ$ , $a \in U$ and $s_{a} \subseteq s_{rule}$ such that $a, s_{a} ⊧_{RS, TUA}^{@ t} C_{a}$ and either

there exists $\hat{s} \subseteq s_{r}$ such that $\hat{s} ⊧_{RS} C$ , ${TUA}^{'} = TUA$ , and either
$ty = can_enable$ , and ${RS}^{'} = RS \cup {(r, \hat{ts}) ∣ \hat{ts} \in \hat{s}}$ , or

$ty = can_disable$ , and ${RS}^{'} = RS ∖ {(r, \hat{ts}) ∣ \hat{ts} \in \hat{s}}$ ,
or

there exist $u \in U$ , $\hat{s} \subseteq s_{r}$ such that $u, \hat{s} ⊧_{TUA} C$ , ${RS}^{'} = RS$ , and either

$ty = can_assign$ , and ${TUA}^{'} = TUA \cup {(u, r, \hat{ts}) ∣ \hat{ts} \in \hat{s}}$ , or

$ty = can_revoke$ , and ${TUA}^{'} = TUA ∖ {(u, r, \hat{ts}) ∣ \hat{ts} \in \hat{s}}$ .

In case 2, we also write $(RS, TUA, t) \mapsto_{ac} ({RS}^{'}, {TUA}^{'}, t)$ to emphasize that action $ac \in ψ$ causes the effect.

The intuition underlying the long definition above is the following. Case 1 models time passing in which only the time instant t is updated whereas $RS$ and $TUA$ are left unchanged. Case 2 is divided in four sub-cases corresponding to the application of one of the four types of administrative action in $Ψ_{ATRBACH}$ . All sub-cases share the fact that, at a given time instant t belonging to a sub-schedule $s_{a}$ of $s_{rule}$ , the action is executed under the responsibility of an administrator a satisfying the administrative condition $C_{a}$ , i.e., positive and negative roles in the pre-condition are, respectively, enabled and disabled according to $RS$ and a is a member of positive roles and not a member of negative roles according to both $TUA$ and $TRH$ (cf. the definition of $⊧_{RS, TUA}^{@ t}$ ). An action of type $can_enable$ or $can_disable$ (sub-cases 2.a.i and 2.a.ii, respectively) can be executed provided that the simple condition C is satisfied by the current $RS$ relation, i.e., when the positive roles in C are enabled and the negative ones are disabled in some sub-schedule $\hat{s}$ of $s_{r}$ . For actions of type $can_assign$ or $can_revoke$ (sub-cases 2.b.i and 2.b.ii, respectively), the target role $r_{t}$ is assigned to or revoked from the user u satisfying the simple condition C with respect to $TUA$ and $TRH$ , i.e., the positive roles in C are active for u while the negative ones are not active for u. Note that the definition of $⊧_{RS}$ above is not affected by the temporal role hierarchy $TRH$ since enabling (or disabling) a role does not imply that all its junior roles are also enabled (or disabled). Example 6.
Consider again the TRBAC policy in Example 5 and an ATRBAC system with the following set ψ of temporal administrative actions: $\begin{array}{l} (5) & (can_enable, + CHR, {{ts}_{1}}, {+ CHR}, {{ts}_{2}}, SEC), \\ (6) & (can_assign, + SEC, {t s_{2}}, {+ EMP, - NDR}, {t s_{3}}, PRC) . \end{array}$ For action (5), we can easily check that:
${ts}_{1} ⊧_{{RS}_{0}} {+ CHR}$ since $(CHR, t s_{1}) \in {RS}_{0}$ ;

$u_{1}, {ts}_{1} ⊧_{{TUA}_{0}} {+ CHR}$ since $(u_{1}, CHR, t s_{1}) \in {TUA}_{0}$ ;

$u_{1}, {ts}_{1} ⊧_{{RS}_{0}, {TUA}_{0}}^{@ 9 am} {+ CHR}$ because $9 a m \in {ts}_{1}$ and (i) and (ii);

${ts}_{2} ⊧_{{RS}_{0}} {+ CHR}$ since $(CHR, t s_{2}) \in {RS}_{0}$ .
Because of (i)–(iv), action (5) can be executed to change the status of the ATRBAC system as follows: $\begin{matrix} ({RS}_{0}, {TUA}_{0}, t) \mapsto_{(5)} ({RS}_{1}, {TUA}_{1}, t), \end{matrix}$ where ${TUA}_{1} = {TUA}_{0}$ and ${RS}_{1} = {RS}_{0} \cup {(SEC, {ts}_{2})}$ , i.e., role $SEC$ is set to be enabled during time slot ${ts}_{2}$ .

3.3. SAI for administrative temporal RBAC with static role hierarchies

We define $Q_{ATRBACH}$ to be the set of (temporal) queries of the form $(u_{g}, R_{g}, s_{g})$ , where $u_{g}$ is a user, $R_{g} \subseteq R$ is a set of roles and $s_{g}$ is a schedule. Moreover, we define $(RS, TUA, t) ⊢_{ATRBACH} (u, R, s)$ iff $u, s ⊧_{RS, TUA}^{@ t} {+ r ∣ r \in R}$ , i.e., t belongs to the schedule s, which is such that all roles in R are enabled in each time slot of s and u is a member of all roles in R in each time slot of s.

A SAI $⟨ γ, q, ψ ⟩$ for $γ \in Γ_{ATRBACH}$ , $q \in Q_{ATRBACH}$ , and $ψ \subseteq Ψ_{ATRBACH}$ generalizes the reachability problem for ATRBAC policies considered in [29,40] to take into account (static) temporal role hierarchies and amounts to checking if there exists a ψ-reachable state $({RS}_{f}, {TUA}_{f}, t_{f}) \in Γ_{ATRBACH}$ from the initial state γ such that $({RS}_{f}, {TUA}_{f}, t_{f}) ⊢_{ATRBACH} q$ .

Example 7.
Consider again the ATRBAC system in Example 6 and a temporal query $q = (u_{2}, PRC, {ts}_{3})$ . The SAI $⟨ ({RS}_{0}, {TUA}_{0}, 9 am), q, ψ ⟩$ is solvable because of the sequence of temporal actions $σ = (5), (6)$ , i.e., $\begin{matrix} ({RS}_{0}, {TUA}_{0}, t) \mapsto_{(5)} ({RS}_{1}, {TUA}_{1}, t) \mapsto_{(6)} ({RS}_{2}, {TUA}_{2}, t), \end{matrix}$ where ${RS}_{1}$ , ${TUA}_{1}$ are as in Example 6, ${RS}_{2} = {RS}_{1}$ , and ${TUA}_{2} = {TUA}_{1} \cup (u_{2}, PRC, t s_{3})$ .

4. Security mappings from ATRBACH

We describe three security mappings from $ATRBACH$ into three access control schemes whose SAIs can be easily translated to reachability problems that can be solved by available analysis techniques (see Section 5.1). The first security mapping $τ_{H 2 eF}$ is a temporalised version of $σ_{H 2 F}$ : this is not surprising since $ATRBACH$ generalizes the ATRBAC scheme without temporal role hierarchies in the same way in which $ARBACH$ generalizes $ARBACF$ . Similar to $σ_{H 2 F}$ , the goal of $τ_{H 2 F}$ is to make explicit the effects of inherited role membership. However, the fact that roles should be enabled to activate them complicates the definition of $τ_{H 2 F}$ with respect to that of $σ_{H 2 F}$ ; in fact, we need to keep track of the original administrative condition of any administrative action to check which roles must and must not be enabled.

The second security mapping $τ_{H 2 L}$ tries to overcome the exponential blow up in the size of the SAIs obtained by applying $τ_{H 2 F}$ . The idea to do this is to consider a new administrative action, say of type $ican_assign$ , for each role $r_{j}$ that is junior to a target role in an administrative action of type $can_assign$ , which can assign users to $r_{j}$ if they are already assigned to the target role. The problem then is the mapping of administrative actions of type $can_revoke$ , since we need to keep track of which roles have been assigned because of target roles of $can_assign$ actions or those that are assigned because of target roles of $ican_assign$ actions.

The third security mapping $τ_{H 2 M}$ is based on the same idea of $τ_{H 2 L}$ . The main difference is in the definition of $ican_assign$ : one such action assigns to a user all the roles that are junior to a target role in an administrative action of type $can_assign$ . So, if $r_{1}, \dots, r_{k}$ are the roles junior to a target role of an administrative action of type $ican_assign$ , the mapping $τ_{H 2 M}$ introduces just one action whose effect is the same of executing atomically (i.e., one after the other with no interleaving of other actions) k actions of type $ican_assign$ introduced by $τ_{H 2 L}$ .

Before we formally define the three security mappings above, let us observe that, as discussed in [40], any action $(ty, C_{a}, s_{rule}, C, s_{r}, r)$ can be reduced to a finite collection of actions of the form $(ty, C_{a}, {{ts}_{rule}}, C, {{ts}_{r}}, r)$ , where ${ts}_{rule} \in s_{rule}$ and ${ts}_{r} \in s_{r}$ (we will omit the curly braces around ${ts}_{rule}$ and ${ts}_{r}$ for simplicity). Thus, from now on, we assume that administrative actions are of this form to simplify the technical development.

4.1. $τ_{H 2 F}$ : A temporalised version of $σ_{H 2 F}$

We introduce the access control scheme that is the target of the security mapping (Section 4.1.1) and then define the security mapping itself (Section 4.1.2). We then show the correctness of the mapping (Section 4.1.3).

4.1.1. Definition of $ATRBACF$

First of all, we define the access control scheme $\begin{matrix} ATRBACF = ⟨ Γ_{ATRBACF}, Q_{ATRBACF}, ⊢_{ATRBACF}, Ψ_{ATRBACF} ⟩ \end{matrix}$ that is the target of the security mapping $τ_{H 2 F}$ . $ATRBACF$ is related to $ATRBACH$ as $ARBACF$ is related to $ARBACH$ (see Section 2).

We define $Γ_{ATRBACF}$ to contain all temporal RBAC policies of the form $π = (U, R, P, RS, TUA, PA)$ , where all components are as in Section 3. In practice, the elements of $Γ_{ATRBACF}$ are obtained from those in $Γ_{ATRBACH}$ by omitting the temporal role hierarchies.

We define $Ψ_{ATRBACF}$ to contain tuples of the form $(ty, C_{a}^{e}, C_{a}, s_{rule}, C, s_{r}, r)$ , where $ty$ , $C_{a}$ , $s_{rule}$ , C, $s_{r}$ and r are as in the actions of $Ψ_{ATRBACH}$ and $C_{a}^{e}$ is the (original) enabling condition. In practice, the elements of $Ψ_{ATRBACF}$ are obtained from those in $Ψ_{ATRBACH}$ by adding the original enabling condition $C_{a}^{e}$ to keep track of the roles that are enabled and that permit the execution of (certain) administrative actions. As we will see, this is crucial for defining the mapping $τ_{H 2 F}$ so as to preserve the meaning of the enabling condition in presence of a temporal role hierarchy.

We define $Q_{ATRBACF}$ to contain tuples of the form $(u_{g}, R_{g}, {R_{g}^{1}, \dots, R_{g}^{r}}, s_{g})$ with $u_{g} \in U$ , $R_{g}, R_{g}^{1}, \dots, R_{g}^{r}$ sub-sets of R, and $s_{g}$ a schedule. Note that the queries in $Q_{ATRBACF}$ have an additional component with respect to those of $Q_{ATRBACH}$ (which have only three components). This is so because the satisfaction relation $⊢_{ATRBACF}$ defined below checks the enabling condition by using the set $R_{g}$ of roles whereas it checks for role activation by using one of the sets $R_{g}^{1}, \dots, R_{g}^{r}$ in a query. The addition of $R_{g}$ to the fields composing a query is crucial for preserving the satisfiability of queries in presence of the temporal role hierarchy as it was the case for the addition of fields to actions in the previous item. This will be clear in the definition of $τ_{H 2 F}$ in Section 4.1.2 below.

We define $⊢_{ATRBACF}$ to be such that $(RS, TUA, t) ⊢_{ATRBACF} (u_{g}, R_{g}, {R_{g}^{1}, \dots, R_{g}^{r}}, s_{g})$ iff $s_{g} ⊧_{RS} R_{g}$ and $u_{g}, s_{g} ⊧_{TUA} R_{g}^{i}$ for some $i = 1, \dots, r$ .

Finally, the definition of the relation $\mapsto_{ATRBACF}$ can be derived from that of $\mapsto_{ATRBACH}$ in Section 3 by simply replacing the first two lines of case 2 with

there exist $(ty, C_{a}^{e}, C_{a}, s_{rule}, C, s_{r}, r) \in ψ$ , $a \in U$ , and $s_{a} \subseteq s_{rule}$ such that $t \in s$ , $s_{a} ⊧_{RS} C_{a}^{e}$ , and $a, s_{a} ⊧_{TUA} C_{a}$ and either…

Note that while case 2 in the definition of

\mapsto_{ATRBACH}

uses the same administrative condition

C_{a}

in the checks with

⊧_{RS}

and

⊧_{TUA}

, the definition of

\mapsto_{ATRBACF}

uses

C_{a}^{e}

in the enabling condition (cf. relation

⊧_{RS}

) and

C_{a}

in the activation condition (cf.

⊧_{TUA}

). This is crucial for mimicking the behaviour of administrative actions of

ATRBACH

with those of

ATRBACF

Example 8.
Let us consider again the hospital in Example 5 with $\begin{array}{l} {RS}_{0} = \{\begin{matrix} (CHR, t s_{1}), (CHR, t s_{2}), (DDR, t s_{2}), (NDR, t s_{3}) \end{matrix}\}, \\ {TUA}_{0} = \{\begin{matrix} (u_{1}, CHR, t s_{1}), (u_{1}, CHR, t s_{2}), (u_{1}, CHR, t s_{3}), (u_{2}, NRS, t s_{3}) \end{matrix}\} \end{array}$ and the following $ATRBACF$ administrative actions: $\begin{array}{l} (7) & (can_assign, SEC, CHR, {t s_{2}}, {NRS, - NDR}, {t s_{3}}, PRC), \\ (8) & (can_enable, SEC, CHR, {t s_{2}}, {NRS}, {t s_{3}}, PRC), \end{array}$ where $C_{a}^{e} = {SEC}$ and $C_{a} = {CHR}$ . For action (7), we have:
${ts}_{2} ⊭_{{RS}_{0}} {SEC}$ since $(SEC, t s_{2}) \notin {RS}_{0}$ ;

$u_{1}, {ts}_{2} ⊧_{{TUA}_{0}} {CHR}$ since $(u_{1}, CHR, t s_{2}) \in {TUA}_{0}$ ;

$u_{2}, {ts}_{3} ⊧_{{TUA}_{0}} {NRS, - NDR}$ since $(u_{2}, NRS, t s_{3}) \in {TUA}_{0}$ and $(u_{2}, NDR, {ts}_{3}) \notin {TUA}_{0}$ .
Action (7) cannot be executed at state $({RS}_{0}, {TUA}_{0}, 9 am)$ because role $SEC$ is not enabled during time slot ${ts}_{2}$ (cf. item (i)).

4.1.2. Definition of $τ_{H 2 F}$

Before defining the security mapping relating $ATRBACH$ and $ATRBACF$ , we introduce the following abbreviations: ${Senior}_{ts} (r)$ stands for ${Senior}_{{TRH}_{ts}} (r)$ and ${Senior}_{s} (r)$ for $⋂_{ts \in s} {Senior}_{ts} (r)$ , where s is a schedule, and ${Senior}_{s} (K) = {Senior}_{s} (r_{1}) \times \dots \times {Senior}_{s} (r_{n})$ , where $K = {r_{1}, \dots, r_{n}} \subseteq R$ .

We can now define $\begin{matrix} τ_{H 2 F} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = ⟨ γ_{F}, q_{F}, ψ_{F} ⟩ \end{matrix}$ to be such that

$γ_{H} = (RS, TUA, TRH, t)$ and $γ_{F} = (RS, TUA, t)$ ,

$q_{H} = (u_{g}, R_{g}, s_{g})$ and $q_{F} = (u_{g}, R_{g}, {{r_{g}^{1}, \dots, r_{g}^{m}} ∣ (r_{g}^{1}, \dots, r_{g}^{m}) \in {Senior}_{s_{g}} (R_{g})}, s_{g})$ , and

$ψ_{F}$ is obtained from $ψ_{H}$ by applying the following three transformations, one after the other, with the proviso that $ψ_{H}^{'}$ , $ψ_{H}^{″}$ , and $ψ_{F}$ below are the smallest relations such that

for each $(ty, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}$ : $(ty, C_{a}^{e}, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}^{'}$ for $C_{a}^{e} = C_{a}$ ;

for each $(ty, C_{a}^{e}, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}^{'}$ : $(ty, C_{a}^{e}, C_{a}^{'}, {ts}_{rule}, C^{'}, {ts}_{r}, r) \in ψ_{H}^{″}$ for $C_{a}^{'} = C_{a} \cup {- r_{a}^{'} ∣ - r_{a} \in C_{a}, r_{a}^{'} \in {Senior}_{t s_{rule}} (r_{a})}$ and:

$C^{'} = C$ if $ty \in {can_enable, can_disable}$ or

$C^{'} = C \cup {- r^{'} ∣ - r \in C, r^{'} \in {Senior}_{t s_{r}} (r)}$ if $ty \in {can_assign, can_revoke}$ ;

for each $(ty, C_{a}^{e}, C_{a}^{+} \cup C_{a}^{-}, {ts}_{rule}, C^{+} \cup C^{-}, {ts}_{r}, r) \in ψ_{H}^{″}$ :

$ty \in {can_enable, can_disable}$ and $(ty, C_{a}^{e}, {r_{a}^{1}, \dots, r_{a}^{k}} \cup C_{a}^{-}, {ts}_{rule}, C^{+} \cup C^{-}, {ts}_{r}, r) \in ψ_{F}$ for $(r_{a}^{1}, \dots, r_{a}^{k}) \in {Senior}_{t s_{rule}} (C_{a}^{+})$ , or

$ty \in {can_assign, can_revoke}$ and $(ty, C_{a}^{e}, {r_{a}^{1}, \dots, r_{a}^{k}} \cup C_{a}^{-}, {ts}_{rule}, {r^{1}, \dots, r^{l}} \cup C^{-}, {ts}_{r}, r) \in ψ_{F}$ for $(r_{a}^{1}, \dots, r_{a}^{k}) \in {Senior}_{t s_{rule}} (C_{a}^{+})$ and $(r^{1}, \dots, r^{l}) \in {Senior}_{t s_{r}} (C^{+})$ .

Similar to the security mapping

σ_{H 2 F}

, every SAI

⟨ γ_{H}, q_{H}, ψ_{H} ⟩

ATRBACH

with

q_{H} = (u_{g}, R_{g}, s_{g})

is mapped to one

⟨ γ_{F}, q_{F}, ψ_{F} ⟩

ATRBACF

τ_{H 2 F}

with

q_{F} = (u_{g}, R_{g}, {R_{g}^{1}, \dots, R_{g}^{r}}, s_{g})

and

r ⩾ 1

according to how many elements are in

{Senior}_{s_{g}} (R_{g})

. It is not difficult to see that any sequence of administrative actions for

⟨ γ_{H}, q_{H}, ψ_{H} ⟩

can be transformed into one for

⟨ γ_{F}, q_{F}, ψ_{F} ⟩

and vice versa.

There are two important points to highlight in the transformation above. First, in steps 2 and 3, the transformation does not affect the simple pre-condition C in actions of type $can_enable$ and $can_disable$ . The reason is that the fact that a role is enabled (disabled, respectively) does not imply that all its junior roles are also enabled (disabled, respectively). Second, the additional component $C_{a}^{e}$ of the state in $Γ_{ATRBACF}$ used in step 1 above to make a copy of the original administrative condition $C_{a}$ permits the precise encoding of the enabling condition. To understand this point, let us consider the administrative action $(ty, {+ r_{1}}, {ts}_{rule}, {+ r_{2}}, {ts}_{r}, r)$ with $ty \in {can_assign, can_revoke}$ and assume $(r_{3}, r_{1}, t s_{rule}) \in TRH$ . The action can be executed at time instant $t \in {ts}_{rule}$ if there exists a user a assigned to $r_{3}$ while $r_{1}$ (not $r_{3}$ !) must be enabled at t (the fact that $r_{3}$ is enabled does not imply that $r_{1}$ is also enabled). If we ignored the information stored in the additional field $C_{a}^{e} = {+ r_{1}}$ created in step 1 and considered only the field $C_{a} = {+ r_{3}}$ created after steps 2 and 3, then we would not be able to check that $r_{1}$ is enabled but only that $r_{3}$ is enabled. A similar observation justifies the use of queries with four fields in $ATRBACF$ instead of only three as in $ATRBACH$ .

Example 9.
Consider again the $ATRBACH$ scheme in Example 6. We illustrate how the security mapping $τ_{H 2 F}$ works by transforming:
Action $(can_assign, + SEC, {{ts}_{2}}, {+ EMP, - NDR}, {{ts}_{3}}, PRC)$ in ψ as follows:

Step (1) modifies the action to $(can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR}, {{ts}_{3}}, PRC)$ by adding $C_{a}^{e} = {+ SEC}$ .

Step (2) modifies the action to $(can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR, - HED}, {{ts}_{3}}, PRC)$ by processing negative roles in $C_{a}$ and C.

Step (3) transforms the actions to those in the following set: $\begin{array}{l} (9) & (can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR, - HED}, {{ts}_{3}}, PRC), \\ (10) & (can_assign, + SEC, + CHR, {{ts}_{2}}, {+ EMP, - NDR, - HED}, {{ts}_{3}}, PRC), \\ (11) & (can_assign, + SEC, + SEC, {{ts}_{2}}, {+ NRS, - NDR, - HED}, {{ts}_{3}}, PRC), \\ (12) & (can_assign, + SEC, + CHR, {{ts}_{2}}, {+ NRS, - NDR, - HED}, {{ts}_{3}}, PRC) . \end{array}$

The query $q_{H} = (u_{2}, PRC, {ts}_{3})$ in $ATRBACH$ to $q_{F} = (u_{2}, PRC, {{PRC}, {NDR}}, {ts}_{3})$ because $NDR$ , $PRC \in {Senior}_{{ts}_{3}} (PRC)$ .

The sequence $σ_{H} = (5), (6)$ in $ATRBACH$ to $σ_{F} = (5^{'}), (12)$ , where action (5′) denotes the transformed action of (5) in $ATRBACH$ by using $τ_{H 2 F}$ .

4.1.3. Correctness of $τ_{H 2 F}$

We now claim the correctness of $τ_{H 2 F}$ by showing that $τ_{H 2 F}$ is a security mapping. This is done by proving that every SAI $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ in $ATRBACH$ is solvable (i.e., there exists a sequence of administrative actions $σ_{H} = a_{H}, a_{H}^{'}, \dots, a_{H}^{″}$ such that $γ_{H} \mapsto_{σ_{H}} γ_{H}^{'}$ and $γ_{H}^{'} ⊢ q_{H}$ ) iff $⟨ γ_{F}, q_{F}, ψ_{F} ⟩$ is so in $ATRBACF$ , where $⟨ γ_{F}, q_{F}, ψ_{F} ⟩ = τ_{H 2 F} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩)$ . The main idea is to show that we can always construct a sequence of actions $σ_{F} = a_{F}, a_{F}^{'}, \dots, a_{F}^{″}$ in $ATRBACF$ based on $σ_{H}$ (and vice versa) such that $γ_{F} \mapsto_{σ_{F}} γ_{F}^{'}$ and $γ_{F}^{'} ⊢ q_{F}$ . To do this, the key point is to show that for each action $a_{H}$ in $ATRBACH$ , we can always find an ‘equivalent’ action $a_{F}$ in $ATRBACF$ and vice versa. The sequence $σ_{F}$ ( $σ_{H}$ , respectively) is then constructed by simply connecting all $a_{F}$ ( $a_{H}$ , respectively) found for each action in $σ_{H}$ ( $σ_{F}$ , respectively). This is stated by the following lemma:

Lemma 1.
There exist $a_{F} \in ψ_{F}$ and $a_{H} \in ψ_{H}$ such that $γ_{H} \mapsto_{a_{H}} γ_{H}^{'}$ iff $γ_{F} \mapsto_{a_{F}} γ_{F}^{'}$ , where $γ_{H} = (RS, TUA, TRH, t)$ , $γ_{H}^{'} = (R S^{'}, TU A^{'}, TRH, t)$ , $γ_{F} = (RS, TUA, t)$ and $γ_{F}^{'} = (R S^{'}, TU A^{'}, t)$ .

Before proving the lemma, the following remark is in order. Let u be a user, $ts$ be a time slot, $C = C^{+} \cup C^{-}$ be a pre-condition ( $C^{+}$ and $C^{-}$ contain the positive and negative roles of C, respectively), and recall that $u, ts ⊧_{TUA} C$ iff user u is a member (not a member, respectively) of r in $ts$ for each $+ r \in C^{+}$ ( $- r \in C^{-}$ , respectively) as shown in Definition 15. With respect to inheritance by the temporal hierarchy $TRH$ in $ATRBACH$ , this is formalized as follows:
for each role $- r_{j} \in C^{-}$ , all senior roles ${sr}_{j} \in {Senior}_{ts} (r_{j})$ are such that $(u, {sr}_{j}, ts) \notin TUA$ , and

for each role $+ r_{i} \in C^{+}$ , there exists a senior role ${sr}_{i}$ of $r_{i}$ in time slot $ts$ (i.e., $({sr}_{i}, r_{i}, ts) \in TRH$ ) such that $(u, {sr}_{i}, ts) \in TUA$ ,
where item (i) ((ii), respectively) means that all negative (positive, respectively) roles in C are satisfied. Now, we make the inheritance with respect to hierarchy $TRH$ explicit by forming a set ϕ of pre-conditions such that:
every pre-condition in ϕ contains $C^{' -} = {- {sr}_{j} | {sr}_{j} \in {Senior}_{ts} (r_{j})}$ for each $- r_{j} \in C$ , and

ϕ contains pre-condition $C^{' -} \cup C^{' +}$ for each $C^{' +} \in {Senior}_{ts} (C^{+})$ .
Then, it is not difficult to see that $u, ts ⊧_{TUA} C$ with respect to $TRH$ is equisatisfiable to $u, ts ⊧_{TUA} ϕ$ (without $TRH$ ), where the latter means that there exists a pre-condition $C^{'} \in ϕ$ such that $u, ts ⊧_{TUA} C^{'}$ . This is because ϕ, by the way it is constructed, contains all possible inheritances (with respect to $TRH$ ) from the original pre-condition C. We are now ready to prove Lemma 1.
Proof of Lemma 1.
For the left-to-right implication, let $a_{H} = (ty, C_{a}, {ts}_{rule}, C, {ts}_{r}, r)$ and $ty = can_assign$ .4
⁴
Without loss of generality, the following proof can be applied to any other type of $ty$ (namely, $can_enable$ , $can_disable$ or $can_revoke$ ) because they have the same form and because inheritances made by temporal hierarchy only affect relation $TUA$ .

Since $(RS, TUA, TRH, t) \mapsto_{a_{H}} (R S^{'}, TU A^{'}, TRH, t)$ and recalling Definition 17 of $\mapsto_{ATRBACH}$ , we have the following:

$t \in {ts}_{rule}$ and ${ts}_{rule} ⊧_{RS} C_{a}$ and $a, {ts}_{rule} ⊧_{TUA} C_{a}$ ,

$u, {ts}_{r} ⊧_{TUA} C$ ,
where $a, u \in U$ . Note that item 1 is equivalent to $a, {ts}_{rule} ⊧_{RS, TUA}^{@ t} C_{a}$ and $⊧_{TUA}$ is with respect to $TRH$ .

Now we form a set of actions χ of the form $(ty, C_{a}, ϕ_{a}, {ts}_{rule}, ϕ, {ts}_{r}, r)$ in $ATRBACF$ , where $ϕ_{a}$ and ϕ are created from $C_{a}$ and C, respectively, according to the remark above. It is easy to show that $\begin{matrix} there exists a_{F} \in χ such that (RS, TUA, t) \mapsto_{a_{F}} (R S^{'}, TU A^{'}, t) \end{matrix}$ since, as shown in the remark, we also have $a, {ts}_{rule} ⊧_{TUA} ϕ_{a}$ and $u, {ts}_{r} ⊧_{TUA} ϕ$ . (For enabling roles, we still have ${ts}_{rule} ⊧_{RS} C_{a}$ because temporal role hierarchies do not affect the relation $RS$ .)

We note that the reachable states $(R S^{'}, TU A^{'}, t)$ after executing $a_{F}$ and $a_{H}$ are the same because both actions have the same target role r (e.g., $a_{F}$ or $a_{H}$ adds tuple $(u, r, {ts}_{r})$ to $TUA$ ).

Finally, we show that $χ \subseteq ψ_{F}$ where $ψ_{F}$ is created by the security mapping $τ_{H 2 F}$ by observing that item (a) and (b) of the remark above are, respectively, exactly the steps (2) and (3) of the mapping $τ_{H 2 F}$ that explore all possible applications of tuples in hierarchy $TRH$ to roles in $C_{a}$ and C.

For the right-to-left implication, let $χ = {(ty, C_{a}, ϕ_{a}, {ts}_{rule}, ϕ, {ts}_{r}, r)}$ such that $ϕ_{a}$ and ϕ are generated from the pre-conditions $C_{a}$ and C of an action $a_{H} = (ty, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}$ by steps (2) and (3) of the mapping $τ_{H 2 F}$ . Assume that there exists an action $a_{F}$ in χ such that $(RS, TUA, t) \mapsto_{a_{F}} (R S^{'}, TU A^{'}, t)$ . This implies that there exists an administrator a and a user u such that $a, {ts}_{rule} ⊧_{TUA} ϕ_{a}$ and $u, {ts}_{r} ⊧_{TUA} ϕ$ (see the remark above).

Given that $a, {ts}_{rule} ⊧_{TUA} ϕ_{a}$ and $u, {ts}_{r} ⊧_{TUA} ϕ$ and that $ϕ_{a}$ and ϕ are generated from $C_{a}$ and C, respectively, by using tuples in hierarchy $TRH$ , we also have $a, {ts}_{rule} ⊧_{TUA} C_{a}$ and $u, {ts}_{r} ⊧_{TUA} C$ , where $⊧_{TUA}$ is now with respect to $TRH$ . As a consequence, we infer $\begin{matrix} (RS, TUA, TRH, t) \mapsto_{a_{H}} (R S^{'}, TU A^{'}, TRH, t) . \end{matrix}$ This concludes the proof of the lemma. □

By applying Lemma 1 to each action in the sequence $σ_{H}$ of $ATRBACH$ and then connecting them in the order as in $σ_{H}$ , we can always construct a sequence of actions $σ_{F}$ in $ATRBACF$ and vice versa. Note that actions modelling time passing in sequences $σ_{H}$ and $σ_{F}$ do not have effect on $RS$ or $TUA$ and thus, we simply keep such actions as they are in the constructed sequence. Again, we emphasize that executing $σ_{H}$ or $σ_{F}$ will reach the same last state because, as mentioned above, the reachable states after executing an action $a_{H}$ and its “equivalent” action $a_{F}$ are the same.

Finally, we show that the queries $q_{F} = (u_{g}, R_{g}, {R_{g}^{'} ∣ R_{g}^{'} \in {Senior}_{s_{g}} (R_{g})}, s_{g})$ and $q_{H} = (u_{g}, R_{g}, s_{g})$ are equisatisfiable at the last state $γ = (RS, TUA, t)$ , i.e., $u_{g}, s_{g} ⊧_{TUA} R_{g} \Leftrightarrow u_{g}, s_{g} ⊧_{TUA} {R_{g}^{'}}$ . Indeed, ${R_{g}^{'}}$ is generated from $R_{g}$ in the same way as ϕ from C as in the remark; as a consequence, we can easily conclude their equisatisfiability. This and Lemma 1 allow us to conclude that every SAI $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ in $ATRBACH$ is solvable iff $⟨ γ_{F}, q_{F}, ψ_{F} ⟩$ is so in $ATRBACF$ . This entails the following theorem. Theorem 2.
$τ_{H 2 F}$ is a security mapping.

4.2. $τ_{H 2 L}$ : Linear mapping

In the worst case, similar to $σ_{H 2 F}$ , the security mapping $τ_{H 2 F}$ defined in Section 4.1 can increase the size of the SAI (cf. the transformation of the query and the conditions of administrative actions) by an exponential factor. The crucial observation to avoid this problem is the following: if a user is assigned to a role $r_{1}$ during time slot ${ts}_{1}$ and $(r_{1}, r_{2}, {ts}_{1}) \in TRH$ , then we can assume that the user is also assigned to role $r_{2}$ during ${ts}_{1}$ . In this case, we say that the user is implicitly assigned to role $r_{2}$ during ${ts}_{1}$ .

This suggests transforming each tuple in the temporal role hierarchy $TRH$ into a new administrative action of type $ican_assign$ (similar to those of type $can_assign$ ) such that when a user is assigned to a role r, he/she can be “implicitly” assigned to any junior role by executing the newly introduced actions. As we need to introduce a new action of type $ican_assign$ per junior role, it is easy to see that the number of such actions is linear in the cardinality of $TRH$ , i.e., the number of tuples in the temporal hierarchy.

Care must be put in handling standard and implicit role membership. In fact, when a user u is assigned to a role r by a $can_assign$ action (standard/explicit role membership), it can also be implicitly assigned to any role junior to r by an $ican_assign$ action (implicit role membership). Now, if u is revoked from r, then also all the junior roles that have been implicitly assigned to u must be revoked. By using actions of type $can_assign$ in $ATRBAC$ to simulate the hierarchies, we seem to explicitly assign the user to the junior roles when the actions are executed. Thus, we need to keep track of such junior roles for every user such that a $can_revoke$ action executed after that can know which junior roles will also be revoked from u if u is revoked from r, which is a computationally heavy task! We avoid this problem by adding a relation $iTUA \subseteq U \times R \times TS$ to temporal RBAC policies and require $TUA$ to record only explicit role memberships (i.e., those resulting from the application of $can_assign$ actions), whereas $iTUA$ records both explicit and implicit ones.

To do this, we consider a new type of administrative action $ican_assign$ specified by tuples of the form $\begin{matrix} (ican_assign, r^{'}, ts, r) \end{matrix}$ for $(r^{'}, r, ts) \in TRH$ . These actions can be executed without the supervision of administrators once an administrative action (e.g., one of type $can_assign$ ) has given a user some (senior) role. Basically, such actions will modify (add/delete some tuple to/from) the new relation $iTUA$ introduced above.

As in Section 4.1, we first introduce the target access control scheme (Section 4.2.1), then define the security mapping (Section 4.2.2), and finally prove its correctness (Section 4.2.3).

4.2.1. Definition of $ATRBACL$

We define the access control scheme $\begin{matrix} ATRBACL = ⟨ Γ_{ATRBACL}, Q_{ATRBACL}, ⊢_{ATRBACL}, Ψ_{ATRBACL} ⟩ \end{matrix}$ as follows:

$Γ_{ATRBACL}$ contains all pairs of the form $(π, t)$ , where t is a time instant and $π = (U, R, P, RS, TUA, iTUA, PA)$ with U, R, P, $RS$ , $TUA$ and $PA$ as in $ATRBACF$ , and $iTUA \subseteq U \times R \times TS$ .

$Q_{ATRBACL}$ contains all tuples of the form $(u_{g}, R_{g}, s_{g})$ , where $u_{g}$ is a user, $R_{g}$ is a sub-set of roles and $s_{g}$ is a schedule.

$⊢_{ATRBACL}$ is such that $(RS, TUA, iTUA, t) ⊢_{ATRBACL} (u, R, s)$ iff $u, s ⊧_{RS, iTUA}^{@ t} {+ r ∣ r \in R}$ ; note that we replace $TUA$ by the new relation $iTUA$ in the definition of $⊧_{RS, TUA}^{@ t}$ in Section 3.

$Ψ_{ATRBACL}$ contains $Ψ_{ATRBACF}$ plus all tuples of the form $(ican_assign, r^{'}, ts, r)$ for $r, r^{'} \in R$ and $ts \in TS$ , i.e., contains actions of types $can_enable$ , $can_disable$ , $can_assign$ , $can_revoke$ or $i_can_assign$ .

Finally, the definition of $\mapsto_{ATRBACL}$ can be derived from that of $\mapsto_{ATRBACF}$ in Section 4.1.1 by the following observations (we refrain from giving a formal definition since it is very similar to that of $\mapsto_{ATRBACH}$ from which $\mapsto_{ATRBACF}$ is derived):

An action of type either $can_enable$ or $can_disable$ modifies only $RS$ (following case 2.a.i and 2.a.ii of the definition of $\mapsto_{ATRBACH}$ , respectively) and leaves unchanged both $TUA$ and $iTUA$ .

An action of type $can_assign$ adds a tuple to $TUA$ (following case 2.b.i of the definition of $\mapsto_{ATRBACH}$ ) and does the same to $iTUA$ while leaving unchanged $RS$ .

An action of type $can_revoke$ removes a tuple from $TUA$ (following case 2.b.ii of the definition of $\mapsto_{ATRBACH}$ ) and then sets $iTUA$ to the updated value (i.e., after the removal of the tuple) of $TUA$ . The need of resetting $iTUA$ to $TUA$ after removing a tuple in the second case arises from the observation that removing an explicit role membership invalidates all the implicit ones in $iTUA$ related to it.

An action $(ican_assign, r^{'}, ts, r)$ does not require an administrator in order to be executed; it only requires a check that there exists a user u who is member of role $r^{'}$ at time slot $ts$ to add the tuple $(u, r, ts)$ to $iTUA$ while leaving both $TUA$ and $RS$ unchanged.

4.2.2. Definition of $τ_{H 2 L}$

We can now define the following security mapping $\begin{matrix} τ_{H 2 L} (⟨ γ_{H}, q_{H}, ψ_{H} ⟩) = ⟨ γ_{L}, q_{L}, ψ_{L} ⟩ \end{matrix}$ to be such that:

$γ_{H} = (RS, TUA, TRH, t)$ and $γ_{L} = (RS, TUA, iTUA, t)$ ,

$q_{H} = (u_{g}, R_{g}, s_{g})$ and $q_{L} = (u_{g}, R_{g}, s_{g})$ , and

$ψ_{L}$ is the smallest relation obtained from $ψ_{H}$ as follows:

for each $(ty, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}$ : $(ty, C_{a}^{e}, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{L}$ where $C_{a}^{e} = C_{a}$ ,

for each $(ty, C_{a}^{e}, C_{a}, {ts}_{rule}, C, {ts}_{r}, r) \in ψ_{H}$ : $(ty, C_{a}^{e}, C_{a}^{'}, {ts}_{rule}, C^{'}, {ts}_{r}, r) \in ψ_{L}$ where $C_{a}^{'} = C_{a} \cup {- r_{a}^{'} ∣ - r_{a} \in C_{a} and r_{a}^{'} \in {Senior}_{t s_{rule}} (r_{a})}$ ,

$C^{'} = C$ if $ty \in {can_enable, can_disable}$ ,

$C^{'} = C \cup {- r^{'} ∣ - r \in C and r^{'} \in {Senior}_{t s_{r}} (r)}$ if $ty \in {can_assign, can_revoke}$ ,

for each $(r_{1}, r_{2}, ts) \in TRH$ , $(ican_assign, r_{1}, ts, r_{2}) \in ψ_{L}$ .

Note that step (1) adds the original enabling condition $C_{a}^{e}$ to every administrative action as in the mapping $τ_{H 2 F}$ . The reason to do this is to keep track of information about the roles that must be enabled/disabled when checking whether an action can be executed or not (cf. the explanation in Section 4.1). Step (2) processes negative roles in conditions $C_{a}$ and C and step (3) adds $ican_assign$ actions with respect to the hierarchy $TRH$ to the set of actions ψ.

Contrary to the mapping $τ_{H 2 F}$ , every SAI $⟨ γ_{H}, q_{H}, ψ_{H} ⟩$ in $ATRBACH$ with $q_{H} = (u_{g}, R_{g}, s_{g})$ is mapped to only one $⟨ γ_{L}, q_{L}, ψ_{L} ⟩$ in $ATRBACL$ by $τ_{H 2 L}$ with $q_{L} = (u_{g}, R_{g}, s_{g})$ , thereby avoiding the exponential blow up in the size of the resulting SAI. In particular, the number of administrative actions resulting from the application of $τ_{H 2 L}$ is much lower than those resulting from the application of $τ_{H 2 F}$ .

4.2.3. Correctness of $τ_{H 2 L}$

We show the correctness of $τ_{H 2 L}$ by proving that $τ_{H 2 L}$ is a security mapping. The main argument of the proof, which we give below, is the following. The application of an administrative action $a_{H}$ of type $can_assign$ in $Ψ_{ATRBACH}$ can be simulated (in $ATRBACL$ ) by a sequence of actions of type $ican_assign$ that assign an administrator and a regular user to junior roles, then followed by executing the action $a_{H}$ itself. This is illustrated in Lemma 2 below.

Lemma 2.
Let $ρ_{L}$ be a sequence of actions of the form ${ia}_{L}, {ia}_{L}^{'}, {ia}_{L}^{″}, \dots, a_{L}$ in $ATRBACL$ , where $a_{L}$ is an action of type $ca = can_assign$ 5
⁵
Similar to Section 4.1, the following proof can be applied to other types of administrative action.

and the other actions are of type $ican_assign$ . Then $\begin{matrix} there exist a_{H} \in ψ_{H} and σ_{L} \subseteq ψ_{L} such that γ_{H} \mapsto_{a_{H}} γ_{H}^{'} iff γ_{L} \mapsto_{ρ_{L}} γ_{L}^{'}, \end{matrix}$ where $γ_{H} = (RS, TUA, TRH, t)$ , $γ_{H}^{'} = (R S^{'}, TU A^{'}, TRH, t)$ , $γ_{L} = (RS, TUA, iTUA, t)$ and $γ_{L}^{'} = (R S^{'}, TU A^{'}, iTU A^{'}, t)$ .

Before proving the lemma, we observe that the execution of an action $(ican_assign, r_{1}, ts, r_{2})$ in $ATRBACL$ is “equivalent” to the application of a tuple $(r_{1}, r_{2}, ts)$ in hierarchy $TRH$ in $ATRBACH$ . Indeed, $ican_assign$ actions can be executed anytime without any constraint to assign a user u having a senior role $r_{1}$ to the junior role $r_{2}$ . In $ATRBACH$ , this is simulated by using the tuple $(r_{1}, r_{2}, ts)$ to make role $r_{2}$ inheritable by a user u anytime provided that u currently has role $r_{1}$ (i.e., u is implicitly assigned to role $r_{2}$ ). The execution of a sequence of $ican_assign$ actions, e.g., $(ican_assign, r_{1}, ts, r_{2})$ and then $(ican_assign, r_{2}, ts, r_{3})$ to assign u to the most junior role $r_{3}$ , is “equivalent” to the use of a sequence of tuples $(r_{1}, r_{2}, ts)$ and $(r_{2}, r_{3}, ts)$ in $ATRBACH$ . Proof of Lemma 2.
Let $a_{H} = (ca, C_{a}, {ts}_{rule}, C, {ts}_{r}, r)$ and $a_{L} = (ca, C_{a}, C_{a}^{'}, {ts}_{rule}, C^{'}, {ts}_{r}, r)$ be obtained by applying $τ_{H 2 L}$ on $a_{H}$ . For the left-to-right implication, we assume that $a_{H}$ is executed on user u satisfying the pre-condition C (e.g., $u, {ts}_{r} ⊧_{TUA} C$ ). That is, u is a (implicit or explicit) member of positive roles and not a (implicit or explicit) member of negative roles according to both $TUA$ and $TRH$ . As observed above, to (implicitly) assign u to each role $+ r \in C$ , we may have used a sequence σ of tuples in the hierarchy $TRH$ (in a certain order) given that user u is currently assumed to play in a certain senior role of r. In $ATRBACL$ , we can get the same effect by executing a sequence of $ican_assign$ actions on user u such that the first $ican_assign$ action corresponds to the first tuple of the sequence σ in $ATRBACH$ and so on. This is because each $ican_assign$ simulates exactly the effect of a tuple in the hierarchy $TRH$ as in the observation above. After executing the sequence of $ican_assign$ actions, u is also assigned to $+ r \in C$ in $ATRBACL$ , i.e., $(u, r, {ts}_{r}) \in iTUA$ (recall that $ican_assign$ actions update only $iTUA$ ).

Now, the sequence $ρ_{L}$ in $ATRBACL$ is constructed by collecting all the sequences of $ican_assign$ actions generated for each $+ r \in C$ as described above. Clearly, after executing $ρ_{L}$ , u satisfies the pre-condition $C^{'}$ in $a_{L}$ since u, by executing a certain sequence of $ican_assign$ actions in $ρ_{L}$ , satisfies every role $+ r$ in $C^{'}$ . Note that we do not consider negative roles because they are processed as in $τ_{H 2 F}$ (cf. Step (2) in $τ_{H 2 L}$ ).

We can generate a sequence of $ican_assign$ actions for each role in administrative condition $C_{a}$ in the same way as for C and this sequence is also added to $ρ_{L}$ . At this point, it is not difficult to see that action $a_{L}$ is now executable because $C_{a}^{'}$ and $C^{'}$ are satisfied (after executing sequences of $ican_assign$ actions in $ρ_{L}$ ). Then, the final step is to add the action $a_{L}$ to the end of the sequence $ρ_{L}$ .

Finally, we emphasize that final states $γ_{H}^{'}$ (after executing $a_{H}$ ) and $γ_{L}^{'}$ (after executing the sequence $ρ_{L}$ ) have the same $R S^{'}$ and $TU A^{'}$ . Indeed, given that $a_{H}$ and $a_{L}$ contain the same target roles and given the definition of $\mapsto_{ATRBACL}$ (i.e., keep all effects to $RS$ and $TUA$ as in $\mapsto_{ATRBACH}$ ), executing $a_{H}$ in $ATRBACH$ updates $RS$ and $TUA$ of $γ_{H}$ in the same way as executing $a_{L}$ on $γ_{L}$ in $ATRBACL$ . This implies that the executions of $a_{H}$ and $ρ_{L}$ have the same effect on current state $γ_{H}$ and $γ_{L}$ , respectively, since all $ican_assign$ actions in $ρ_{L}$ only have effect on $iTUA$ while leaving $RS$ and $TUA$ unchanged (cf. the definition of $\mapsto_{ATRBACL}$ ).

For the right-to-left direction, we argue that an executable sequence $ρ_{L} = \dots, a_{L}$ in $ATRBACL$ , where “…” stands for any sequence of $ican_assign$ , implies that $a_{H}$ in $ATRBACH$ is also executable. We assume that $a_{L} = (ca, C_{a}, C_{a}^{'}, {ts}_{rule}, C^{'}, {ts}_{r}, r)$ is executable in $ATRBACL$ on user u satisfying the pre-condition $C^{'}$ , i.e.:
$(u, r, {ts}_{r}) \in iTUA$ for each $+ r \in C^{'}$ , and

$(u, r, {ts}_{r}) \notin iTUA$ for each $- r \in C^{'}$ .
Note that $iTUA$ is always obtained from $TUA$ by executing actions of type $ican_assign$ simulating the temporal hierarchy. Thus, $(u, r, {ts}_{r}) \in iTUA$ iff either (i) $(u, r, {ts}_{r})$ is also in $TUA$ or (ii) there exists $(u, r^{'}, {ts}_{r}) \in TUA$ , where $r^{'}$ is a senior role of r and executing a certain sequence of $ican_assign$ actions to “implicitly” assign u to r (this sequence can be seen as a part of “…” in $ρ_{L}$ above). In the context of $ATRBACH$ , this means that we have to use a set of tuples in hierarchy $TRH$ (those corresponding to the $ican_assign$ actions used) in a certain order to implicitly assign u to one more junior role and then to another junior role and so on until we reach the most junior role $+ r \in C$ . We do not consider negative roles $- r$ in C because, as argued in the proof of the left-to-right direction, $τ_{H 2 L}$ processes them as in $τ_{H 2 F}$ . A similar explanation can be applied to roles in $C_{a}^{'}$ and $C_{a}$ of $a_{L}$ and $a_{H}$ , respectively. As a consequence, the fact that $a_{L}$ is executable (since both $C_{a}^{'}$ and $C^{'}$ are satisfied after executing $ρ_{L}$ ) implies that the action $a_{H}$ is also executable. Additionally, as argued above, $a_{H}$ and $a_{L}$ have the same target roles. Thus, the executions of $a_{H}$ and $a_{L}$ (or, in general $ρ_{L}$ ) have the same effects on $RS$ and $TUA$ . □
Example 10.
Consider again the $ATRBACH$ scheme in Example 6. We illustrate how the security mapping $τ_{H 2 L}$ works as follows:
Step (1) modifies action $(can_assign, + SEC, {{ts}_{2}}, {+ EMP, - NDR}, {{ts}_{3}}, PRC)$ in ψ to $(can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR}, {{ts}_{3}}, PRC)$ by adding $C_{a}^{e} = {+ SEC}$ . This step is also applied to other actions.

Step (2) transforms action $(can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR}, {{ts}_{3}}, PRC)$ to $\begin{array}{rcl} (13) & (can_assign, + SEC, + SEC, {{ts}_{2}}, {+ EMP, - NDR, - HED}, {{ts}_{3}}, PRC) \end{array}$ by processing negative roles in $C_{a}$ and C. Other actions are processed in a similar way.

Step (3) adds the following actions of type $ican_assign$ to ψ: $\begin{array}{l} (14) & (ican_assign, + CHR, {ts}_{1}, SEC), \\ (15) & (ican_assign, + CHR, {ts}_{2}, SEC), \\ (16) & (ican_assign, + NRS, {ts}_{3}, EMP), \\ (17) & (ican_assign, + CHR, {ts}_{3}, SEC), \\ (18) & (ican_assign, + NDR, {ts}_{3}, PRC), \\ (19) & (ican_assign, + HED, {ts}_{3}, NDR) . \end{array}$

The query $q_{H} = q_{L} = (u_{2}, PRC, {ts}_{3})$ .

The sequence $σ_{H} = (5), (6)$ in $ATRBACH$ will be transformed to $σ_{L} = (5^{″}), (15), (16), (13)$ , where action (5″) denotes the transformed action of (5) in $ATRBACH$ by using $τ_{H 2 L}$ . Note that in the sequence $σ_{L}$ , we need to execute the $ican_assign$ action (15) to assign user $u_{1}$ having senior role $CHR$ to junior role $SEC$ . Also, the $ican_assign$ action (16) is used to assign $u_{2}$ to junior role $EMP$ .

Theorem 3.
$τ_{H 2 L}$ is a security mapping.
Proof of Theorem 3.
Similar to the proof of Theorem 2, we show that $τ_{H 2 L}$ is a security mapping by showing that (i) we can always construct a sequence of actions $σ_{L}$ in $ATRBACL$ from a sequence $σ_{H} = a_{H}, a_{H}^{'}, \dots, a_{H}^{″}$ in $ATRBACH$ and vice versa, and (ii) $q_{H}$ and $q_{L}$ are equisatisfiability. Indeed, by applying Lemma 2 on each action $a_{H}$ of $σ_{H}$ , we get a set of sequences of the form $ρ_{L}$ above. The sequence $σ_{L}$ is then constructed by connecting sequences in the set with respect to the order of corresponding actions $a_{H}$ in $σ_{H}$ .

To construct $σ_{H}$ from $σ_{L}$ , we observe that $σ_{L}$ always has the form “ $\dots, a_{L}, \dots, a_{L}^{'}, \dots$ ”, where “…” is any sequence of $ican_assign$ actions. Then, applying Lemma 2 on each sequence “ $\dots, a_{L}$ ” in $σ_{L}$ (note that we can ignore the last “…” appearing in $σ_{L}$ since $ican_assign$ actions do not affect relations $RS$ and $TUA$ ), we get a set of $can_assign$ actions. The sequence $σ_{H}$ is constructed by connecting all the actions in the order.

Finally, the equisatisfiability of queries $q_{H}$ and $q_{L}$ on the last state $γ_{H}$ and $γ_{L}$ obtained by executing $σ_{H}$ and $σ_{L}$ , respectively, is explained as follows. First, it is not difficult to see that relations $RS$ and $TUA$ of the last states $γ_{H}$ and $γ_{L}$ are the same since, as stated in the proof of Lemma 2, each action $a_{H}$ in $σ_{H}$ and the corresponding sequence $ρ_{L}$ in $σ_{L}$ have the same effect on $RS$ and $TUA$ . Second, the relation $iTUA$ is always obtained from $TUA$ by executing $ican_assign$ actions simulating the use of tuples in the hierarchy $TRH$ . Thus, the query $q_{H}$ is satisfied with respect to the relation $TUA$ (of the last state $γ_{H}$ ) and the use of tuples in $TRH$ implies that the query $q_{L}$ is also satisfied with respect to the relation $iTUA$ (of state $γ_{L}$ ) obtained by executing the corresponding $ican_assign$ actions on the relation $TUA$ and vice versa. □

4.3. $τ_{H 2 M}$ : Multi-target mapping

A possible problem with $τ_{H 2 L}$ arises when the depth of the temporal hierarchy is large since this implies the execution of a large number of $ican_assign$ actions to simulate just one $can_assign$ action in $ATRBACH$ . To understand why, it is useful to introduce the notion of depth of a temporal hierarchy $TRH$ as the number of tuples in the longest chain of the form $(r_{1}, r_{2}, ts), (r_{2}, r_{3}, ts), \dots, (r_{n}, r_{n + 1}, ts)$ for $(r_{i}, r_{i + 1}, ts) \in TRH$ with $i = 1, \dots, n$ and for each time slot $ts \in TS$ . Then, consider Example 10 and imagine a temporal role hierarchy of depth n. In this case, we may need to execute n $ican_assign$ actions to assign a user to the most junior role. This may affect negatively the performance of the model checker in charge of exploring all possible interleavings of the available administrative actions by considerably enlarging its search space. To avoid this problem, we introduce a new mapping that “combines” the effects of several $ican_assign$ actions into one. The idea is to define a new version $mican_assign$ of $ican_assign$ that assigns to a user all the junior roles of a given role in one shot.

We define the access control scheme $\begin{matrix} ATRBACM = ⟨ Γ_{ATRBACM}, Q_{ATRBACM}, ⊢_{ATRBACM}, Ψ_{ATRBACM} ⟩, \end{matrix}$ where

$Γ_{ATRBACM} = Γ_{ATRBACL}$ .

$Q_{ATRBACM} = Q_{ATRBACL}$ .

$⊢_{ATRBACM} = ⊢_{ATRBACL}$ .

$Ψ_{ATRBACM}$ contains $Ψ_{ATRBACH}$ plus all tuples of the form $(mican_assign, r, ts, {Junior}_{ts} (r))$ , where ${Junior}_{ts} (r) = {r^{'} ∣ (r, r^{'}) \in {TRH}_{ts}}$ for $r \in R$ and $ts \in TS$ . Also the actions of type $mican_assign$ can be executed without the supervision of an administrator and their effect is the same as that obtained by executing atomically, one after the other, the administrative actions $(ican_assign, r, ts, r^{'})$ defined in Section 4.2, for each $r^{'} \in {Junior}_{ts} (r)$ .

$\mapsto_{ATRBACM}$ is defined as $\mapsto_{ATRBACL}$ except that the effect of the $ican_assign$ action is now replaced by that of the $mican_assign$ action.

The definition of

τ_{H 2 M}

can be derived from that of

τ_{H 2 L}

by replacing step (3) of

τ_{H 2 L}

in Section 4.2 with the following:

for each role $r \in R$ , time slot $ts \in TS$ , if ${Junior}_{t s} (r) \neq \emptyset$ then $(mican_assign, r, ts, {Junior}_{ts} (r)) \in ψ_{L}$ .

Theorem 4.
$τ_{H 2 M}$ is a security mapping.

This is a corollary of Theorem 3 since the effect of a $mican_assign$ action in $ATRBACM$ can always be simulated by a (finite) sequence of actions of type $ican_assign$ in $ATRBACL$ . Example 11.
Consider again the $ATRBACH$ scheme in Example 6. We illustrate how the security mapping $τ_{H 2 M}$ works as follows:
Administrative actions in ψ are processed by steps (1) and (2) as in $τ_{H 2 L}$ (see Example 10).

Step (3′) adds the following actions of type $mican_assign$ to ψ: $\begin{array}{l} (20) & (mican_assign, + CHR, {ts}_{1}, SEC), \\ (21) & (mican_assign, + CHR, {ts}_{2}, SEC), \\ (22) & (mican_assign, + NRS, {ts}_{3}, EMP), \\ (23) & (mican_assign, + CHR, {ts}_{3}, SEC), \\ (24) & (mican_assign, + NDR, {ts}_{3}, PRC), \\ (25) & (mican_assign, + HED, {ts}_{3}, {NDR, PRC}) . \end{array}$

The query $q_{H} = q_{L} = q_{M} = (u_{2}, PRC, {ts}_{3})$ .

We only need to execute the $mican_assign$ action (25) to assign any user having senior role $HED$ to the most junior role $PRC$ instead of the two $ican_assign$ actions (18) and (19) as in Example 10.

5. Implementation and experiments

We have implemented the three security mappings $τ_{H 2 F}$ , $τ_{H 2 L}$ and $τ_{H 2 M}$ in asaspTIME, which, by using a symbolic model checker, is capable of processing the generated SAIs. In the following, we first describe our extended version of asaspTIME (in Section 5.1) and then discuss the findings of our experiments (in Section 5.2).

5.1. asaspTIME: A safety analysis tool for ATRBAC policies without role hierarchies

Following [27], we reduce the SAI problems for the three target access control systems (namely, $ATRBACF$ , $ATRBACL$ and $ATRBACM$ ) defined in Section 4 to a reachability problem of a particular class of symbolic transition systems expressed by first-order logic formulae. In turn, such a problem is reduced to a finite sequence of constraint satisfaction problems. Here, we briefly recall the main notions underlying the approach in [27] that reduces a SAI problem to a sequence of constraint satisfaction problems that are compactly described by using a class of first-order logic formulae. Such a class, called Bernays–Schönfinkel–Ramsey (BSR), contains formulae of the form $\exists \underline{x} . \forall \underline{y} . φ (\underline{x}, \underline{y})$ for φ a Boolean combination of atomic sub-formulae built out of equality, predicates, constants (functions are not allowed), and variables in the tuples $\underline{x}$ , $\underline{y}$ . It is well-known (see, e.g., [26]) that the constraint satisfiability problem for BSR formulae is decidable and NEXPTIME complete. Practical approaches to building efficient procedures that handle this class of formulae (see again [26]) are available in state-of-the-art theorem provers, called Satisfiability Modulo Theories (SMT); see, e.g., [8] for an introduction to SMT solving and its applications. In the following, we show how SMT solvers can be used to support the reachability analysis of a class of symbolic transition systems expressed by using BSR formulae.

Definition 18.
An adequate BSR symbolic transition system (adequate BSR-STS, for short) is a tuple $⟨ \underline{s}, A x, In, Tr ⟩$ , where
$\underline{s}$ is a (finite) sequence of predicates, called the state variables,

$A x$ is a (finite) set of BSR formulae, called axioms,

$In (\underline{s})$ is a universal BSR formula (i.e., a BSR formula of the form $\forall \underline{y} . φ (\underline{y})$ ),6
⁶
From now on, we consider BSR formulae to be built over the symbols in $A x$ and $\underline{s}$ .

called the initial state formula, and

$Tr$ is a (finite) disjunction of BSR formulae of the form $\begin{matrix} (26) & \exists \underline{x} . (G (\underline{s}) \land \underset{s \in \underline{s}}{⋀} \forall \underline{y} . (s^{'} (\underline{y}) \Leftrightarrow U_{s} (\underline{s}, \underline{y}))), \end{matrix}$ called transition formulae, where

${\underline{s}}^{'}$ is the sequence obtained from $\underline{s}$ by priming each element,

$\underline{x}$ and $\underline{y}$ are tuples of variables,

$G (\underline{s})$ is a quantifier-free (BSR) formula, called the guard, containing the variables in $\underline{x}$ as free variables, and where each occurrence of the predicate symbols in $\underline{s}$ are applied to variables in $\underline{x}$ , and

$U_{s} (\underline{s}, \underline{y})$ is a quantifier-free (BSR) formula, called the update, containing the variables in $\underline{x}, \underline{y}$ as free variables, and where the length of $\underline{y}$ matches the arity of s, and each occurrence of the predicate symbols in $\underline{s}$ is applied to variables in $\underline{x}$ , $\underline{y}$ .

The reachability problem for an adequate BSR-STS $⟨ \underline{s}, A x, In, Tr ⟩$ and an existential BSR formula $γ (\underline{s})$ (i.e., a BSR formula of the form $\exists \underline{x} . φ (\underline{x})$ ), called the goal, consists of establishing whether there exists an integer $n ⩾ 0$ such that $\begin{array}{rcl} (27) & In ({\underline{s}}_{0}) \land τ ({\underline{s}}_{0}, {\underline{s}}_{1}) \land \dots \land τ ({\underline{s}}_{n - 1}, {\underline{s}}_{n}) \land γ ({\underline{s}}_{n}) \land Ax \end{array}$ is satisfiable, where $τ (\underline{s}, {\underline{s}}^{'}) : = ⋁_{tr \in Tr} tr (\underline{s}, {\underline{s}}^{'})$ and the sequence ${\underline{s}}_{i}$ is obtained from $\underline{s}$ by uniquely renaming each of its elements by appending the suffix i (for $i = 0, \dots, n$ ). For clarity, if $ϕ (\underline{s})$ is a formula containing symbols from $\underline{s}$ , then $ϕ ({\underline{s}}_{i})$ is the formula obtained from ϕ by pairwise replacement of each element in $\underline{s}$ with the corresponding one in ${\underline{s}}_{i}$ .

A monadic BSR-STS is an adequate BSR-STS whose predicates are unary.
Theorem 5 ([27]).

The reachability problem for monadic BSR-STSs is decidable.

The proof of the theorem in [27] is constructive. It presents a procedure that generates a sequence of BSR formulae representing sets of backward reachable states. The procedure has been implemented in the tool asaspTIME [29] with some heuristics for scalability.

To simplify the translation from the three access control systems $ATRBACF$ , $ATRBACL$ and $ATRBACM$ , we use the following extension of the notion of monadic BSR-STS by considering a many-sorted (typed) version of first-order logic (see, e.g., [14] for formal definitions). An effectively monadic BSR-STS is an adequate BSR-STS whose predicate symbols are n-ary for $n ⩾ 0$ and such that at least $n - 1$ arguments range over enumerated datatypes. An enumerated datatype is formalized by considering a sort symbol S, constants $e_{1}, \dots, e_{n}$ , and the following set $Enum ({e_{1}, \dots, e_{n}}, S)$ of formulae $\begin{array}{l} (28) & e_{i} \neq e_{j} for distinct i, j in {1, \dots, n}, \\ (29) & \forall x . (x = e_{1} \lor \dots \lor x = e_{n}) . \end{array}$ It is always possible [27] to transform an effectively monadic BSR-STS into a monadic BSR-STS.

Corollary 1.
The reachability problem for effectively monadic BSR-STSs is decidable.

This result has been applied to the safety analysis of Administrative Temporal RBAC policies without role hierarchies [29] corresponding to SAI problems for $ATRBACF$ . The main advantage in developing safety analysis based on Corollary 1 is the following. The user-role reachability problem is solved with respect to a finite but unknown number of users in the policies manipulated by the administrative actions. When the goal is unreachable, the safety certification takes into account the fact that users may join or leave the organization in which the policies are administered. When the goal is reachable, the technique is capable of establishing the number of users needed for some sequence of administrative actions to transform the initial policy into one satisfying the goal (usually obtained by negating a security goal).

Fig. 1.
The architecture of the extended version of asaspTIME.

Figure 1 shows the architecture of the (extended) version of asaspTIME. The three mappings $τ_{H 2 F}$ , $τ_{H 2 L}$ and $τ_{H 2 M}$ have been described in Section 4. The box labelled $BR$ is the symbolic procedure briefly sketched above, which uses BSR formulae to represent sets of backward reachable states. The box labelled $TR$ implements the translations from the three access control systems $ATRBACF$ , $ATRBACL$ and $ATRBACM$ to effectively monadic BSR-STSs. For the sake of conciseness, we avoid to give the definitions of these translations; instead, we illustrate how they work on a concrete instance of $ATRBACF$ (the translations for $ATRBACL$ and $ATRBACM$ are similar and are thus omitted).

Before presenting the example, we observe that, in order to solve SAI problems for $ATRBACF$ (and also for $ATRBACL$ and $ATRBACM$ ), we do not need to keep track of the current time t in the state $(RS, TUA, t)$ but only the time slot $ts$ that t belongs to. In fact, for any time instants $t, t^{'}$ belonging to the same time slot, if the administrative action $τ = (ty, C_{a}^{e}, C_{a}, s_{rule}, C, s_{r}, r)$ can be executed at t, then τ can also be executed at $t^{'}$ and vice versa (e.g., $⊧_{RS, TUA}^{@ t}$ and $⊧_{RS, TUA}^{@ t^{'}}$ are identical). For this reason, without loss of generality, we assume that the state of any $ATRBACF$ system is of the form $(RS, TUA, ts)$ , where $ts$ is a time slot.
Example 12.
Let us consider again the Example 8 with query $q = (u_{1}, PRC, PRC, {ts}_{3})$ . $TR$ works by first introducing the system variable $\underline{s}$ containing the predicate symbols:
$rs (y, z)$ , representing the relation $RS$ ,

$tua (x, y, z)$ , representing the relation $TUA$ ,

$at (z)$ , keeping track of the current time slot,
where x ranges over set U of users, y ranges over set R of roles and z ranges over set $TS$ of time slots.

The initial state $({RS}_{0}, {TUA}_{0}, {ts}_{1})$ is translated into the following universal formula $In (\underline{s})$ : $\begin{matrix} \forall x, y, z . [\begin{matrix} rs (y, z) & \Leftrightarrow & (\begin{matrix} (y = CHR \land z = {ts}_{1}) & \lor \\ (y = CHR \land z = {ts}_{2}) & \lor \\ (y = DDR \land z = {ts}_{2}) & \lor \\ (y = NDR \land z = {ts}_{3}) \end{matrix}) & \land \\ tua (x, y, z) & \Leftrightarrow & (\begin{matrix} (x = u_{1} \land y = CHR \land z = {ts}_{1}) & \lor \\ (x = u_{1} \land y = CHR \land z = {ts}_{2}) & \lor \\ (x = u_{1} \land y = CHR \land z = {ts}_{3}) & \lor \\ (x = u_{2} \land y = NRS \land z = {ts}_{3}) & \lor \end{matrix}) & \land \\ at (z) & \Leftrightarrow & z = {ts}_{1} \end{matrix}] . \end{matrix}$ The translation of action $(can_assign, SEC, CHR, {t s_{2}}, {NRS, - NDR}, {t s_{3}}, PRC)$ is $\begin{matrix} \exists u_{ad}, u, ts . [\begin{matrix} at (ts) & \land & ts = {ts}_{2} & \land \\ rs (SEC, {ts}_{2}) & \land & tua (u_{ad}, CHR, {ts}_{2}) & \land \\ tua (u, NRS, {ts}_{3}) & \land & \neg tua (u, NDR, {ts}_{3}) & \land \\ \forall y, z . {rs}^{'} (y, z) & \Leftrightarrow & rs (y, z) & \land \\ \forall x, y, z . {tua}^{'} (x, y, z) & \Leftrightarrow & (\begin{matrix} tua (x, y, z) & \lor & [\begin{matrix} x = u & \land \\ y = PRC & \land \\ z = {ts}_{3} \end{matrix}] \end{matrix}) & \land \\ \forall z . {at}^{'} (z) & \Leftrightarrow & at (z) \end{matrix}], \end{matrix}$ which is exactly of the form (26) where lines 1–3 are in guard $R (\underline{s})$ and the others are in update. Note how relation $TUA$ is updated while $RS$ is left unchanged.

Similarly, the translation of $(can_enable, SEC, CHR, {t s_{2}}, {NRS}, {t s_{3}}, PRC)$ is $\begin{matrix} \exists u_{ad}, u, ts . [\begin{matrix} at (ts) & \land & ts = {ts}_{2} & \land \\ rs (SEC, {ts}_{2}) & \land & tua (u_{ad}, CHR, {ts}_{2}) & \land \\ tua (u, NRS, {ts}_{3}) & \land & \neg tua (u, NDR, {ts}_{3}) & \land \\ \forall y, z . {rs}^{'} (y, z) & \Leftrightarrow & (\begin{matrix} rs (y, z) & \lor & [\begin{matrix} y = PRC & \land \\ z = {ts}_{3} \end{matrix}] \end{matrix}) & \land \\ \forall x, y, z . {tua}^{'} (x, y, z) & \Leftrightarrow & tua (x, y, z) & \land \\ \forall z . {at}^{'} (z) & \Leftrightarrow & at (z) \end{matrix}] . \end{matrix}$ The other administrative actions are translated in a similar way and are omitted.

The query $q = (u_{1}, PRC, PRC, {ts}_{3})$ is translated into the following existential BSR formula: $\begin{array}{rcl} G : = \exists x . (x = u_{1} \land rs (PRC, {ts}_{3}) \land tua (u_{1}, PRC, {ts}_{3})) . \end{array}$ We can easily see that the formulae above satisfy the conditions for an effectively monadic BSR-STS. As a consequence, we can solve the problem by the symbolic backward reachability procedure briefly sketched above which will return unreachable (according to what has been discussed in Example 8).

To summarize, asaspTIME takes as input a SAI for $ATRBACH$ , i.e., a reachability problem for Administrative Temporal RBAC policies with role hierarchies, first applies one of the three security mappings ( $τ_{H 2 F}$ , $τ_{H 2 L}$ , or $τ_{H 2 M}$ ), then translates the resulting problem into a symbolic reachability problem for adequate BSR-STSs (by invoking $TR$ ), and finally runs the reachability procedure (by invoking $BR$ ) in order to establish if the goal is reachable or unreachable. If the goal is reachable, then asaspTIME returns $solvable$ together with a sequence of administrative actions; otherwise, it returns $unsolvable$ . The returned answer is in terms of the original SAI for $ATRBACH$ .
5.2. Experiments

To evaluate the scalability of the three security mappings, we generate synthetic benchmarks as follows: we use the ATRBAC user-role reachability problems from [29] and add randomly generated temporal role hierarchies organized as lattices with a senior-most and a junior-most role.7

⁷
The evaluation is based on synthetic benchmarks derived from realistic policies according to current practice; see, e.g., [29,38,40]. In particular, [29] contains a thorough discussion of the weaknesses of current standards for the experimental evaluation of authorization policies.

The choice of this kind of temporal role hierarchies has been inspired by the discussion about the shape of hierarchies in [22] and the well-known fact (see, e.g., [12]) that it is always possible to compute a lattice containing a partial order as a sub-order by using the so-called completion process. So, there is no loss of generality with respect to expressiveness in considering role hierarchies structured as lattices. Furthermore, we do not consider problematic the (possible) exponential growth in the number of roles resulting from completion since the experiments below aim to evaluate the scalability of our technique.

A generated temporal role hierarchy $TRH$ is such that ${TRH}_{(a, a + 1)}$ and ${TRH}_{(a + 1, a + 2)}$ are “similar,” i.e., the cardinality of their intersection is close to their cardinalities. This seems to be a reasonable assumption inspired by a sort of “locality” principle: role hierarchies in contiguous time slots should not look very different. The benchmarks contain policies whose number of roles ranges from 15 to 34, the number of administrative actions ranges from 127 to 994, the number of time slots ranges from 5 to 40, the cardinality $| TRH |$ and the height $h ((R, TRH))$ of the temporal role hierarchy $TRH$ range from 50 to 600 and from 3 to 32, respectively.8

⁸

The height of the role hierarchy is the longest (simple) path in the Hasse diagram of the lattice.

At a first glance, the maximum values in the ranges above may seem unrealistic; specifically those for the number of administrative actions and the cardinality of the relation

TRH

. This is not the case for the following two reasons. The former is the result of the multiplicative effect of splitting the sets

s_{rule}

and

s_{r}

in an administrative rule

(ty, C_{a}, s_{rule}, C, s_{r}, r)

into singletons (this transformation has been described in the last paragraph before Section 4.1). For the latter, recall that

TRH \subseteq R \times R \times TS

so that increasing the number of time slots in

TS

yields larger values of

| TRH |

Fig. 2.

Results on benchmarks from [29] extended with randomly generated temporal role hierarchies.

Figure 2 shows the results of our experiments run on an Intel QuadCore (3.6 GHz) CPU with 16 GB RAM and Ubuntu 11.10. There are two benchmark classes: one inspired by a hospital (plot on the left) and one by a university (plot on the right). For each benchmark in a class, the three bars show the average time (in seconds) taken by asaspTIME using the security mapping $τ_{H 2 F}$ , $τ_{H 2 L}$ or $τ_{H 2 M}$ (from left to right) to solve 15 security analysis instances with a given number $Roles$ of roles, a given number $Rules$ of administrative actions (called rules, for short), a given number of time slots $TS$ , and the cardinality of the temporal role hierarchy $| TRH |$ (the tuple $Roles$ / $Rules$ / $TS$ / $| TRH |$ shown on the x-axis of the plots). The two plots clearly show the superiority of the last security mapping $τ_{H 2 M}$ over the other two. It is also clear that $τ_{H 2 F}$ is the less scalable of the three. The reason is the reduced number of administrative actions generated by $τ_{H 2 M}$ in comparison with $τ_{H 2 F}$ . For the benchmarks in the Hospital class, the number of actions generated by $τ_{H 2 M}$ is between 1.2 and 2.1 times the number of actions in the original policy, whereas those generated by $τ_{H 2 F}$ is between 2.3 and 63.1 times. For the benchmarks in the University class, the gap is even wider with the number of actions generated by $τ_{H 2 M}$ being between 1.4 and 1.7 times the number of actions in the original policy and those generated by $τ_{H 2 F}$ being between 3.8 and 56.3 times. The better behaviour of $τ_{H 2 M}$ over $τ_{H 2 L}$ is due to the fact that the former generates actions whose effect combines those of several actions generated by the latter, as explained in Section 4.3.

Fig. 3.

Behaviour for increasing values of the cardinality (left) and the height (right) of the temporal role hierarchy $TRH$ .

Figure 3 (left) shows the behaviour of asaspTIME using the three security mappings when the cardinality (left) of the temporal role hierarchy increases, from 50 to 500, and the height is fixed to 5. Figure 3 (right) shows the behaviour of the tool when using the three security mappings with increasing values, from 3 to 30, of the height $h ((R, TRH))$ of the temporal role hierarchy $TRH$ and the cardinality $| TRH |$ of temporal hierarchies is fixed to 200. In both cases, we picked one problem from the university benchmark and added randomly generated temporal hierarchies as follows. For each value of the cardinality (left) and the height (right), we generated 15 different temporal role hierarchies and extended the policy. The average time (in seconds) taken to solve each resulting problem is plotted in Fig. 3: the blue diamonds line shows the behaviour of $τ_{H 2 F}$ , the green squares line that of $τ_{H 2 L}$ and the violet triangles line that of $τ_{H 2 M}$ . As for the previous set of experiments, $τ_{H 2 M}$ performs much better than the other two and seems to have a polynomial (rather than exponential) growth.

We observe that it is difficult (if possible at all) to perform a comparison with other tools since, to the best of our knowledge, they do not support temporal role hierarchies. We argue why this is so in Section 6 when discussing how to apply our approach to the analysis of policies with dynamic temporal role hierarchies (as in [41]) rather than static (as in this work).

6. Related work

There is a long line of works on the safety analysis of access control policies that started with the seminal paper [17]. To the best of our knowledge, Li and Tripunitara [23] were the first to introduce security analysis in the context of ARBAC, followed by many papers, e.g., [1,3,6,7,10,15,18,21,24,28,31,37,38,43]. The idea underlying such works is to reduce safety analysis to graph manipulation [3,21,37] or fix-point computation performed either by Logic Programming (as in [24]) or model checking (as in [1,6,7,15,18,28,31,38,43]).

The analysis techniques for RBAC that are currently available are not readily applicable to extensions in which authorizations depend also on contextual information, such as time, that are widely used in real-world applications. For instance, two temporal extensions of RBAC are discussed in [9,20]. These models impose temporal constraints on roles being enabled for them to be assigned to users. In these models, the executability of administrative actions is also restricted by temporal constraints. Only few works, i.e., [25,29,35,40], have proposed techniques for the automated analysis of safety problems for ATRBAC models. In [25], the safety problem for ATRBAC policies is reduced to verification problems of timed automata [2], whose solution is supported by the model checker UPPAAL (http://www.uppaal.org). The approach supports the verification of a variety of properties, not only those for safety, but has the drawback of assuming a fixed set of users; every time the set of users changes, the analysis must be re-run. Additionally, the size of the state space to be explored by the model checker grows exponentially in the number of users, making the technique difficult to scale. The approach proposed in [40] amounts to decomposing safety of ATRBAC policies into reachability problems for policies that can be expressed in a model that is (close to) URA97. In this way, existing tools (such as rbac-pat [16] or VAC [15]) for the safety of URA97 administrative policies can be re-used. One of the main advantages of [40] is the possibility to leverage recent advances in the analysis of ARBAC policies. The main disadvantage is the state-space explosion since several safety problems for URA97 must be solved and the complexity of many restricted versions of this problem is known to be NP-hard [34]. The approach in [29] amounts to translating safety problems to (decidable) reachability problems of BSR-STSs to solve them. The analysis technique built on top of the model checker can solve reachability problems for ATRBAC systems with a finite but unknown number of users. In this way, the technique is capable of certifying safety by taking into account that users may join or leave the organization in which the TRBAC policies are administered since the certificate holds for any (finite) number of users. Similarly, it can discover the number of users required for a certain sequence of administrative actions to turn the initial policy into one violating a security goal. This dramatically enlarges the scope of applicability of the analysis and thus the usefulness of its results. Recently, Shahen et al. [35] proposed an approach to leverage an existing analysis tool to solve the safety problem in ATRBAC. The main idea is to reduce the safety problems in ATRBAC to the safety problems in ARBAC and then use Mohawk [18], an analysis tool for ARBAC system, to reason on the problems.

Unfortunately, the approaches above cannot deal with temporal role hierarchies, which is originally a component of the temporal RBAC model. In [41], Uzun et al. recognize the importance of temporal role hierarchies in the context of administrative policies and propose to extend the administrative model in [40] with dynamic temporal role hierarchies, i.e., relative positions of roles in the hierarchy can be modified, as opposed to the static model considered in this paper. In [42], among other things, Uzun et al. implement the approach given in [41]. The approach they propose firstly decomposes the original analysis problem into four independent steps that correspond to the analysis of the relations $TUA$ , $RS$ , temporal $PA$ and dynamic $TRH$ , respectively. The approach performs the steps separately and then combines the results returned by the four steps to conclude the answer for the original analysis problem. This decomposition is justified by an interpretation of the administrative actions that deviates from the semantics of pre-conditions in ARBAC [32]. For instance, [42] interprets a pre-condition on the user in $can_assign$ actions with respect to the direct role membership relation instead of the indirect one. More in detail, assume that the execution of an action $(can_assign, C_{a}, s_{rule}, C, s_{r}, r)$ , which modifies the relation $TUA$ , is determined by $TUA$ only. When the administrative pre-condition $C_{a}$ is satisfied, the action can be executed if there exists a user u such that u and $s_{r}$ satisfy pre-condition C under only the relation $TUA$ and not considering the relation $TRH$ (see, Definitions 15, 16 and 17). Indeed, this greatly simplifies the analysis of the temporal RBAC policy in general, and the policy with temporal role hierarchy in particular. Unfortunately, the results of such an analysis may be confusing for policy designers used to the semantics of pre-conditions proposed in [32]. In this paper, instead, we consider a semantics for pre-conditions that closely follows the spirit of [32] and we model that the execution of an administrative action is determined by all the relations in the model. In this sense, we believe this work to be the first to consider all aspects of the temporal role hierarchy in the analysis of ATRBAC.

The works in [19] and [36] are another attempt to consider the security analysis problem in the TRBAC policy. In the papers, the authors firstly propose an administrative model for TRBAC, namely AMTRAC (Administrative Model for Temporal Role-based Access Control), and define a number of security properties for TRBAC. Then, they present a methodology for performing security analysis of TRBAC that uses Alloy to formally represent TRBAC systems and administrative actions in AMTRAC. The methodology then exploits the Alloy analyser to solve the security analysis problem. Indeed, in [19], the authors claim that the AMTRAC model is more complete than the ATRBAC model proposed by Uzun et al. in [42] given that AMTRAC includes: (i) all administrative actions of the ARBAC model (non-temporal components of AMTRAC), and (ii) a new set of administrative actions that modify the role enabling base assignment including role triggers (temporal components of AMTRAC), while the ATRBAC model does not support role triggers. Furthermore, the difference between the two models is also in (i): the ATRBAC model does not include exactly the original administrative actions in the ARBAC model like AMTRAC but “temporalises” them by adding time schedules $s_{rule}$ and $s_{r}$ (cf. Definitions 16). Since the administrative model considered in Section 3 and in our previous works in [29,30], as well as in [35], is based on the ATRBAC model proposed in [42], our analysis techniques are designed for the ATRBAC model and their application to the AMTRAC model requires further investigation, which is left as future work.

7. Conclusions and future work

We have defined three mappings $τ_{H 2 F}$ , $τ_{H 2 L}$ and $τ_{H 2 M}$ from $ATRBACH$ , an access control scheme corresponding to the ATRBAC model with the presence of static temporal role hierarchy, to three access control schemes whose SAIs can be easily handled by available analysis techniques. The main idea underlying the mappings is to encode the effect of role hierarchies in the administrative actions. The mappings represent increasingly sophisticated variants of this idea and try to alleviate the state-space explosion problem deriving from the huge number of possible interleavings with which administrative actions can be executed. We have shown the application of the mappings to automated policy analysis and implemented them in the tool asaspTIME. The experimental evaluation shows the superiority of $τ_{H 2 M}$ over $τ_{H 2 F}$ and $τ_{H 2 L}$ since the first allows for the generation of problems with smaller state spaces. To the best of our knowledge, asaspTIME is the first tool capable of reasoning in presence of temporal role hierarchies striking a good trade-off between scalability and precision with which the semantics of $ATRBACH$ is taken into consideration (as discussed in Section 6).

The main line of future work is to extend our approach to cope with the dynamic temporal role hierarchies – i.e., the temporal role hierarchy can be changed by adding/deleting some tuple by administrators – as done in [41]. Doing this requires us to extend the mappings defined in this work to also encode changes to the relation $TRH$ . We plan to do this by using the actions $ican_assign$ (introduced in Section 4.2) and $mican_assign$ (introduced in Section 4.3) along the following lines. First, we represent all possible role relationships $(r^{'}, r, ts)$ by using a set of $ican_assign$ actions as in $τ_{H 2 L}$ . Then, the effect of administrative actions that modify the dynamic role hierarchy $TRH$ can be simulated by enabling or disabling the execution of the corresponding $ican_assign$ actions. For instance, adding a tuple $(r_{1}, r_{2}, ts)$ to the dynamic role hierarchy will make the action $(ican_assign, r_{1}, ts, r_{2})$ enabled and vice versa. At this point, the dynamic role hierarchy can be abstracted away (as it is encoded by a set of $ican_assign$ actions) and it is thus possible to reuse available analysis techniques as in Section 5.1 to solve the user-role reachability problem in the context of a dynamic role hierarchy. The main roadblock to achieve this is the presence of negative roles in the pre-conditions $C_{a}$ and C of an administrative action (cf. step (2) of $τ_{H 2 L}$ and $τ_{H 2 M}$ in Section 4.2 and Section 4.3, respectively). In fact, with dynamic role hierarchies, the set of roles that are senior to the negative roles in $C_{a}$ and C may change (instead this is not possible which temporal role hierarchies are static) so that the set of senior roles prior to the addition or deletion of some tuples in $TRH$ may no longer be valid and needs to be replaced with the updated version. Thus, we need further sophisticated mechanisms to handle changes in the set of senior roles and in pre-conditions of administrative actions. The details of how to do this are currently being investigated.

Footnotes

Acknowledgments

This work was partially supported by the PRIN 2010-11 project “Security Horizons”, and funded by Vietnam National Foundation for Science and Technology Development (NAFOSTED) under grant number 102.01-2016.28.

References

Alberti,

Armando and

Ranise, Efficient symbolic automated analysis of administrative role based access control policies, in: ASIACCS, ACM, 2011.

Alur and

Dill, A theory of timed automata, Theoretical Computer Science 126 (1994), 183–285. doi:10.1016/0304-3975(94)90010-8.

Ammann,

Lipton and

Sandhu, The expressive power of multi-parent creation in monotonic access control models, Journal of Computer Security 4(2–3) (1996), 149–196.

Amthor,

W.E.

Kühnhauser and

Pölck, Heuristic safety analysis of access control models, in: Proceedings of the 18th ACM Symposium on Access Control Models and Technologies, SACMAT ’13, ACM, New York, 2013, pp. 137–148. doi:10.1145/2462410.2462413.

Amthor,

W.E.

Kühnhauser and

Pölck, Worse: A workbench for model-based security engineering, Computers & Security 42(Supplement C) (2014), 40–55. doi:10.1016/j.cose.2014.01.002.

Armando and

Ranise, Automated symbolic analysis of ARBAC policies, in: 6th STM Workshop, LNCS, Vol. 6710, Springer, 2010, pp. 17–33.

Armando and

Ranise, Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving, Journal of Computer Security 20(4) (2012), 309–352. doi:10.3233/JCS-2012-0461.

Beckert,

C.A.R.

Hoare,

Hähnle,

Smith,

D.R.

Green,

Ranise,

Tinelli,

Ball and

S.K.

Rajamani, Intelligent systems and formal methods in software engineering, IEEE Int. Sys. 21(6) (2006), 71–81. doi:10.1109/MIS.2006.117.

Bertino,

Bonatti and

Ferrari, TRBAC: A temporal role based access control model, ACM TISSEC 4(3) (2001), 191–233. doi:10.1145/501978.501979.

10.

Calzavara,

Rabitti and

Bugliesi, Compositional typed analysis of ARBAC policies, in: Proceedings of the 28th Computer Security Foundations Symposium (CSF), IEEE, 2015, pp. 33–45.

11.

Crampton, Understanding and developing role-based administrative models, in: CCS, ACM, 2005.

12.

B.A.

Davey and

H.A.

Priestley, Introduction to Lattices and Orders, 2nd edn, Cambridge University Press, 1991.

13.

De Capitani di Vimercati,

Foresti,

Jajodia and

Samarati, Access control policies and languages, International Journal of Computational Science and Engineering (IJCSE) 3(2) (2007), 94–102. doi:10.1504/IJCSE.2007.015739.

14.

H.B.

Enderton, A Mathematical Introduction to Logic, Academic Press, 1972.

15.

A.L.

Ferrara,

Madhusudan and

Parlato, Policy analysis for self-administrated role-based access control, in: TACAS, Springer, 2013.

16.

M.I.

Gofman,

Luo,

A.C.

Solomon,

Zhang,

Yang and

S.D.

Stoller, RBAC-PAT: A policy analysis tool for role based access control, in: TACAS, LNCS, Vol. 5505, Springer, 2009, pp. 46–49.

17.

M.A.

Harrison,

W.L.

Ruzzo and

J.D.

Ullman, Protection in operating systems, Communications of the ACM 19 (1976), 461–471.

18.

Jayaraman,

Ganesh,

Tripunitara,

Rinard and

Chapin, Automatic error finding for access-control policies, in: CCS, ACM, 2011.

19.

Jha,

Sural,

Vaidya and

Atluri, Security analysis of temporal RBAC under an administrative model, Computers & Security 46 (2014), 154–172. doi:10.1016/j.cose.2014.08.001.

20.

J.B.D.

Joshi,

Bertino,

Latif and

Ghafoor, A generalized temporal role-based access control model, IEEE TKDE 7(1) (2005), 4–23.

21.

Koch,

L.V.

Mancini and

Parisi-Presicce, Decidability of safety in graph-based models for access control, in: ESORICS, LNCS, Vol. 2502, 2002, pp. 229–244.

22.

Li and

Mao, Administration in role based access control, in: ASIACCS, ACM, 2007.

23.

Li and

M.V.

Tripunitara, Security analysis in role-based access control, in: Proceedings of ACM Symposium on Access Control Models and Technologies, ACM, 2004, pp. 126–135.

24.

Li and

M.V.

Tripunitara, Security analysis in role-based access control, ACM TISSEC 9(4) (2006), 391–420. doi:10.1145/1187441.1187442.

25.

Mondal,

Sural and

Atluri, Security analysis of GTRBAC and its variants using model checking, Computers & Security 30 (2011), 128–147.

26.

Piskac,

de Moura and

Bjørner, Deciding effectively propositional logic using DPLL and substitution sets, Journal of Automated Reasoning 44(4) (2010), 401–424. doi:10.1007/s10817-009-9161-6.

27.

Ranise, Symbolic backward reachability with effectively propositional logic – Applications to security policy analysis, FMSD 42(1) (2013), 24–45.

28.

Ranise and

Truong, Incremental analysis of evolving administrative role based access control policies, in: DBSec, Springer, 2014, pp. 206–275.

29.

Ranise,

Truong and

Armando, Scalable and precise automated analysis of administrative temporal role-based access control, in: SACMAT, ACM, 2014.

30.

Ranise,

Truong and

Viganò, Automated analysis of RBAC policies with temporal constraints and static role hierarchies, in: Proceedings of the 14th Edition of the Computer Security Track at the 30th ACM Symposium on Applied Computing (SECSAC), ACM, 2015.

31.

Ranise,

T.A.

Truong and

Armando, Boosting model checking to analyse large ARBAC policies, in: 8th STM Workshop, LNCS, Vol. 7783, Springer, 2012, pp. 273–288.

32.

Sandhu,

Bhamidipati and

Munawer, The ARBAC97 model for role-based control administration of roles, ACM TISSEC 1(2) (1999), 105–135. doi:10.1145/300830.300839.

33.

Sandhu,

Coyne,

Feinstein and

Youmann, Role-based access control models, IEEE Computer 2(29) (1996), 38–47. doi:10.1109/2.485845.

34.

Sasturkar,

Yang,

S.D.

Stoller and

Ramakrishnan, Policy analysis for administrative role based access control, in: CSF, IEEE, 2006.

35.

Shahen,

Niu and

Tripunitara, Mohawk+T: Efficient analysis of administrative temporal role-based access control (ATRBAC) policies, in: Proceedings of the 20th ACM Symposium on Access Control Models and Technologies, SACMAT ’15, ACM, New York, 2015, pp. 15–26. doi:10.1145/2752952.2752966.

36.

Shatma,

Sural,

Vaidya and

Atluri, AMTRAC: An administrative model for temporal role-based access control, Computers & Security 39 (2013), 201–218. doi:10.1016/j.cose.2013.07.005.

37.

Soshi,

Maekawa and

Okamoto, The dynamic-typed access matrix model and decidability of the safety problem, IEICE-TF 1 (2004), 1–14.

38.

S.D.

Stoller,

Yang,

Ramakrishnan and

M.I.

Gofman, Efficient policy analysis for administrative role based access control, in: CCS, ACM, 2007.

39.

M.V.

Tripunitara and

Li, A theory for comparing the expressive power of access control models, Journal of Computer Security 15 (2007), 231–272.

40.

Uzun,

Atluri,

Sural,

Vaidya,

Parlato and

A.L.

Ferrara, Analyzing temporal role based access control models, in: SACMAT, ACM, 2012.

41.

Uzun,

Atluri,

Vaidya and

Sural, Analysis of TRBAC with dynamic temporal role hierarchies, in: DBSec XXVII, LNCS, Vol. 7964, 2013, pp. 297–304.

42.

Uzun,

Atluri,

Vaidya,

Sural,

A.L.

Ferrara,

Parlato and

Madhusudan, Security analysis for temporal role based access control, Journal of Computer Security 22(6) (2014), 961–996. doi:10.3233/JCS-140510.

43.

Yang,

Gofman,

S.D.

Stoller and

Yang, Policy analysis for administrative role based access control without separate administration, Journal of Computer Security 23(1) (2015), 1–29. doi:10.3233/JCS-140511.

Automated and efficient analysis of administrative temporal RBAC policies with role hierarchies

Abstract

Keywords

1. Introduction

1.1. Contributions

3.1. Temporal RBAC with static role hierarchies

4.1. τ H 2 F : A temporalised version of σ H 2 F

4.1.1. Definition of ATRBACF

4.2.1. Definition of ATRBACL

4.2.2. Definition of τ H 2 L

4.2.3. Correctness of τ H 2 L

5.1. asaspTIME: A safety analysis tool for ATRBAC policies without role hierarchies

7 The evaluation is based on synthetic benchmarks derived from realistic policies according to current practice; see, e.g., [29,38,40]. In particular, [29] contains a thorough discussion of the weaknesses of current standards for the experimental evaluation of authorization policies.

7. Conclusions and future work

Footnotes

Acknowledgments

References

4.1. $τ_{H 2 F}$ : A temporalised version of $σ_{H 2 F}$

4.1.1. Definition of $ATRBACF$

4.2.1. Definition of $ATRBACL$

4.2.2. Definition of $τ_{H 2 L}$

4.2.3. Correctness of $τ_{H 2 L}$

⁷
The evaluation is based on synthetic benchmarks derived from realistic policies according to current practice; see, e.g., [29,38,40]. In particular, [29] contains a thorough discussion of the weaknesses of current standards for the experimental evaluation of authorization policies.