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
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
Taking into consideration the effect of all possible sequences of administrative actions transforming P into
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.
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
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 (
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 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
To ease reading, in Table 1 we give a roadmap for the main notions considered in the paper.
A roadmap for the main notions considered in the paper
We introduce the notions of access control schemes, access control systems, and security analysis instances by adapting them from [39].
An access control scheme is a state-transition system
We write
Consider an access control scheme An access control system is a pair A security analysis instance (SAI) is the triple
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.
We now formalize the access control scheme
Let U, R and P respectively be sets of users, roles and permissions.
An RBAC policy is a tuple
If
We define
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
A pre-condition is a finite set of signed roles of the forms
Permission to assign users to roles is specified by a ternary relation
A user u is a member of u is not a member of
We omit the policy γ when it is clear from the context.
Let
there exists there exists
Note that in both cases in Definition 6 we also write
Let User User
Action (1) can be executed by administrator
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
For
A Security Analysis Instance (SAI)
Let us consider again Example 1 and a query
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
Given two access control schemes
The mapping σ from A to B extends to SAIs as follows.
We now formalize the access control scheme
An RBAC policy with hierarchy is a tuple
We say that a user u is a member of role r in
User u has permission p in
We are now ready to define
The definition of
Consider again the sets U, R, ψ, and the current policy User User User
Like for
In fact, every SAI for
We define for each for each
Note that every SAI
Note that, in the worst case,
Consider the query
A SAI
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
We extend the ATRBAC model in [29] with static temporal role hierarchies to define the access control scheme
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).
Let
To ease readability, we will use concrete time intervals, e.g.,
A time instant is a non-negative real number. A time instant t belongs to a time slot
In the definition, we employ the usual modulo operator
Below, we assume
A Temporal RBAC policy γ with static temporal role hierarchies extends an RBAC policy in three respects:
TRBAC adds the role status relation
The user-role assignment relation
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
A hierarchical TRBAC policy is a tuple
We say that user u is a member of role r (with respect to the TRBAC policy π) in time slot
We define
We illustrate the definitions by extending the hospital scenario considered in Example 1 with time constraints. We assume that the hospital in Example 1 works for 24 hours (i.e., Role User Role User
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,
Let Time slot Schedule s satisfies C under User u and time slot User u and schedule s satisfy C under u and u and s satisfy C under
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
A (temporal) administrative action has the form
An administrative action of type
Administrative actions are executed instantaneously and are interleaved with time-passing transitions for incrementing time. Formally, the effect of the administrative actions in
there exist there exists there exist
or
In case 2, we also write
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 Consider again the TRBAC policy in Example 5 and an ATRBAC system with the following set ψ of temporal administrative actions:
Because of (i)–(iv), action (5) can be executed to change the status of the ATRBAC system as follows:
We define
A SAI Consider again the ATRBAC system in Example 6 and a temporal query
We describe three security mappings from
The second security mapping
The third security mapping
Before we formally define the three security mappings above, let us observe that, as discussed in [40], any action
: A temporalised version of
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).
Definition of
First of all, we define the access control scheme
We define We define We define We define Finally, the definition of the relation
there exist
Let us consider again the hospital in Example 5 with
Note that while case 2 in the definition of
Action (7) cannot be executed at state
Before defining the security mapping relating
We can now define
for each for each for each
Similar to the security mapping
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 Consider again the Action Step (1) modifies the action to Step (2) modifies the action to Step (3) transforms the actions to those in the following set:
The query The sequence
We now claim the correctness of
There exist
Before proving the lemma, the following remark is in order. Let u be a user, for each role for each role every pre-condition in ϕ contains ϕ contains pre-condition
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
Then, it is not difficult to see that
For the left-to-right implication, let
Without loss of generality, the following proof can be applied to any other type of
where
Now we form a set of actions χ of the form
We note that the reachable states
Finally, we show that
For the right-to-left implication, let
Given that
By applying Lemma 1 to each action in the sequence
Finally, we show that the queries
In the worst case, similar to
This suggests transforming each tuple in the temporal role 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
To do this, we consider a new type of administrative action
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).
Definition of
We define the access control scheme
Finally, the definition of An action of type either An action of type An action of type An action
Definition of
We can now define the following security mapping
for each
for each
for each
Note that step (1) adds the original enabling condition
Contrary to the mapping
Correctness of
We show the correctness of
Let
Similar to Section 4.1, the following proof can be applied to other types of administrative action.
Before proving the lemma, we observe that the execution of an action Let Now, the sequence We can generate a sequence of Finally, we emphasize that final states For the right-to-left direction, we argue that an executable sequence Consider again the Step (1) modifies action Step (2) transforms action Step (3) adds the following actions of type The query The sequence
Similar to the proof of Theorem 2, we show that To construct Finally, the equisatisfiability of queries
Note that
A possible problem with
We define the access control scheme
The definition of
for each role
This is a corollary of Theorem 3 since the effect of a Consider again the Administrative actions in ψ are processed by steps (1) and (2) as in Step (3′) adds the following actions of type The query We only need to execute the
We have implemented the three security mappings
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,
An adequate BSR symbolic transition system (adequate BSR-STS, for short) is a tuple From now on, we consider BSR formulae to be built over the symbols in
The reachability problem for an adequate BSR-STS
A monadic BSR-STS is an adequate BSR-STS whose predicates are unary.
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
To simplify the translation from the three access control systems
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

The architecture of the extended version of
Figure 1 shows the architecture of the (extended) version of
Before presenting the example, we observe that, in order to solve SAI problems for
Let us consider again the Example 8 with query
where x ranges over set U of users, y ranges over set R of roles and z ranges over set
The initial state
Similarly, the translation of
The query
To summarize,
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.
A generated temporal role hierarchy
The height of the role hierarchy is the longest (simple) path in the Hasse diagram of the lattice.

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

Behaviour for increasing values of the cardinality (left) and the height (right) of the temporal role hierarchy
Figure 3 (left) shows the behaviour of
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).
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 (
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
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
Conclusions and future work
We have defined three mappings
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
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.
