Proactive enforcement of provisions and obligations

Abstract

We present an approach to the proactive enforcement of provisions and obligations, suitable for building policy enforcement mechanisms that both prevent and cause system actions. Our approach encompasses abstract requirements for proactive policy enforcement, a system model describing how enforcement mechanisms interact with and control target systems, and concrete policy languages and associated enforcement mechanisms. As examples of policy languages, we consider finite automata and timed dynamic condition response (DCR) graphs. We use finite automata to illustrate the basic principles and DCR graphs to show how these principles can be adapted to a practical, real-time policy language. In both cases, we show how to algorithmically determine whether a given policy is enforceable and, when this is the case, construct an associated enforcement mechanism. Our approach improves upon existing formalisms in two ways: (1) we exploit the target system’s existing functionality to avert policy violations proactively, rather than compensate for them reactively; and (2) rather than requiring the manual specification of remedial actions in the policy, we deduce required actions directly from the policy.

Keywords

Access control run-time enforcement obligations business process modeling

1. Introduction

Problem context. Many security requirements can be decomposed into provisions and obligations [7,29,38,40]. Provisions specify conditions or properties dependent on the present and the past. They cover most traditional access control requirements. For example, access to customer records is granted to users in the role of customer-relations manager, provided customer consent was previously granted. Obligations, in contrast, impose conditions on the future that an agent or process should fulfil. For example, a hospital may be required to delete patient records within 14 days after a patient’s release.

Provisions and their enforcement by access control mechanisms are well understood. Obligations are less well understood, and subject to active research [2,4,19–21,23,24,30,31,33–37,48,53]. The enforcement of obligations is difficult as, to be enforceable, obligations must be associated with deadlines. A simple but limited enforcement mechanism is to associate obligations with access control rules, whereby the enforcement mechanism immediately takes the obliged action when the rule grants access, for example, logging the taken action. Alternatively, obligations may be associated with deadlines, whose expiration triggers remedial actions to be taken by the enforcement mechanism.

The state of the art generally handles obligations in limited ways, like those suggested above. The theory of how to handle obligations is underdeveloped, especially when deadlines are involved. With few exceptions, policy violations are not prevented, rather they are remediated. Namely, the enforcement mechanism witnesses a deadline expiring, but is powerless to prevent the concomitant policy violation and is reduced to taking remedial actions after the fact, such as logging, lowering a reputation rating, etc. Moreover, the enforcement mechanism’s interaction with the target system is often too limited for effective obligation enforcement or the exact extent of the mechanism’s control over the target system is unclear. While an enforcement mechanism can intercept actions and prevent them from happening, it cannot, a priori, force the target system to take action when required. Existing mechanisms tend to take only actions independent of the target system’s functionality, such as logging or sending notifications. We expand on these points and discuss exceptions in Section 8.

Problem addressed. We tackle the problem of proactive policy enforcement and the design of enforcement mechanisms that direct the target system to prevent policy violations. Not every policy can be enforced, and enforceability depends on the enforcement mechanism’s precise powers over the target system. We distinguish between whether an enforcement mechanism can (1) control an action by denying that it happens at a given point in time, (2) proactively cause an action to happen in the target system, or (3) merely observe that an action happens in the target system.

The above distinctions are critical. For example, at a hospital it is (or should be) observable when a patient dies. However it is neither meaningful for an enforcement mechanism to deny nor cause this action happen. In other cases, a mechanism may control whether the action is allowed, but not cause the action to happen by itself. For instance, a hospital IT system may be able to deny the immediate re-admission of a released patient; however, it cannot outright cause a patient to be readmitted, as that would require the patient’s consent. Finally, some actions may be both controllable and causable. For example, the enforcement mechanism can both deny and proactively cause the transfer of records from the hospital IT system’s local data storage to a remote archive, depending on the circumstances. Such distinctions between controllable (in the sense of denying) and uncontrollable (but observable) actions are well-known in other areas, such as supervisory-control theory [50].1

¹
We follow established terminology where possible. For example, controllable and uncontrollable come from supervisory control theory, whereas to deny (an action) comes from the security literature on access control.

Here the supervisor plays the role of the enforcement mechanism; however, in the classical supervisory-control theory, the supervisor cannot cause actions in the target system to occur.

These observations motivate the following technical questions, answered in this paper. Given a policy in a specification language that distinguishes between causable and controllable actions, how do we construct a proactive enforcement mechanisms for it? In particular, can we efficiently compute a sequence of actions sufficient to resolve an impending obligation violation? And in what sense can this be done transparently in that the enforcement mechanism alters the target system’s behavior only when absolutely required by the policy?

Approach taken. Answering these questions necessarily involves a system model, a policy language, and an enforcement mechanism. In the first part of this paper, we present our underlying theory of proactive enforcement. We start, in Section 2, by presenting our model of systems and policies. The system model must clarify how the target system and the enforcement mechanism interact and what the mechanism can and cannot cause or control in the target system. The policy language must be expressive enough to formulate practical policies, yet constrained enough that we can efficiently compute (1) whether a policy is enforceable and (2) which actions are needed to avert impending obligation violations. In Section 3, we specify our requirements for a proactive enforcement mechanism, which connects the system model and the policy, using the latter to compute action sequences for execution within the former. We also establish basic technical results about such mechanisms and relate different enforcement requirements.

In the second part of the paper, we consider two representative policy languages and show how to construct enforcement mechanisms from policies expressed in each of them. First, in Section 5, we show how, and under what conditions, we can construct proactive enforcement mechanisms from finite automata. We introduce the key idea of a resolver, which is the part of the enforcement mechanism that causes sequences of actions to occur to prevent an obligation’s violation, and we show how to construct one. Second, we consider a richer, industrial-strength, policy language: the DCR process modeling language [12,16,27]. This is a declarative graphical process notation that incorporates both causality and time, and is used in industry to specify and build case-management systems. Specifically, in Section 6 we present DCR processes and their underlying theory and in Section 7 we show when and how a policy specified as a DCR process is enforceable. Additionally, we present a nontrivial example.

Contributions. Conceptually, we present a framework for reasoning about and constructing enforcement mechanisms for timed provisions and obligations. Our enforcement mechanisms are novel in that they deduce those actions necessary to avert policy violations and proactively cause the target system to take these actions in the nick of time, that is, whenever a deadline is about to be missed.

This approach improves upon existing formalisms in two ways (see also the discussion on related work in Section 8). First, we proactively exploit the target system’s existing functionality to avert policy violations, rather than to compensate reactively for them. Second, rather than requiring the manual specification of remedial actions in the policy, we deduce relevant actions directly from the policy.

Technically, we show how to construct enforcement mechanisms for two different policy languages and study associated decision problems. For policies specified by automata we define the notion of a derived enforcement mechanism and characterize the policy automaton for which such a mechanism exists. For policies specified by timed DCR processes we show that the enforceability of policies expressed as timed DCR processes is decidable but NP-hard. We then give a sufficient polynomial time verifiable condition for a DCR policy to be enforceable. Moreover, we give an algorithm that, given a DCR state of an enforceable DCR policy, computes a sequence of actions that, when executed on the target system, will discharge impending obligations.

Scope and structure. We focus exclusively on policies governing the sequencing of actions. This helps focus our presentation on the central issue of proactive policy enforcement. We leave open extensions to policy languages that handle other features like actions dependent on data, and the question of whether and how comparable enforcement mechanisms can be realized in other formalisms.

This paper is a substantially revised and extended version of the conference publication [5]. The present paper completely reworks the formal development, dispensing with the notion of a “directed language” in favor of a direct definition of a proactive enforcement mechanism. This change enables a smoother presentation of the use of DCR as a policy language. We also use it to develop new results on how to derive enforcement mechanisms from policies specified as finite automata in Section 5 and to establish a close relationship to Edit Automata [36].

Formalization. We have formalized the core theory of proactive enforcement in Isabelle/HOL and our theory files are available on-line at [11]. We have, however, not formalized our applications of the theory to other models like Edit Automata and DCR graphs. To make precise exactly what has and has not been verified in Isabelle, the definitions, lemmas, and theorems that have been formalized are marked with a black box in this paper, like the one at the end of this paragraph.

The remainder of this paper is organized as follows. In Section 2, we introduce our system model and the notion of policies as languages. In Section 3, we define requirements and establish properties of enforcement mechanisms. In this section we also show that edit automata can be used to depict our enforcement mechanisms and in Section 4 we formalize a tight relationship between these two formalisms. We provide examples of policy languages and enforcement for policies given by finite automata in Section 5 and timed dynamic condition response graphs in Sections 6–7. In Section 8 we make extensive comparisons with related work and in Section 9 we draw conclusions.

2. System model and enforcement

2.1. System model

The target system and the enforcement mechanism (also called a Policy Enforcement Point, or simply PEP) are independently running processes. The target system takes actions. The enforcement mechanism must, somehow, ensure that these actions conform to a given security policy.

Now how does an enforcement mechanism accomplish this? Following [36,48], the result of enforcement should be a stream of actions performed by the target system and the enforcement mechanism. Clearly, the mechanism should ensure that this stream complies with the policy being enforced. However, rather than retroactively translating the target system’s output as done in most previous work, our focus is on proactive enforcement: the enforcement mechanism directs the target system to be policy compliant by suppressing and causing actions in the target system. In particular, the mechanism cannot cause actions to happen that are not enabled in the target system and thereby add to its possible system behaviors.

More concretely, the enforcement mechanism has just two ways of manipulating the target system:

It may selectively deny the target system certain actions

It may selectively instruct or cause the target system to undertake certain actions

Not every action can be denied: If the target system is an aircraft, we cannot reasonably deny it the action “warn the pilot that an engine has failed.” Conversely, not every action can be caused: the “refuel the aircraft” action is not available to commercial aircraft while in flight. As such, we classify the actions of the target system as “uncontrollable” (those that cannot be denied) and “causable” (those that we may force upon the target system at any time).

We sketch the interaction of the enforcement mechanism and the target system in Fig. 1.

Fig. 1.

System model.

Whenever the target system wishes to take a controllable action, it requests permission from the enforcement mechanism (top arrow), which responds by reactively instructing the target system to execute some number of causable actions, and then granting or denying the requested action (second arrow from top).

Whenever the enforcement mechanism observes a deadline approaching, it may proactively instruct the target system to execute causable actions (second to last arrow).

Finally, whenever the target system performs an uncontrollable action, it informs the enforcement mechanism that it does so (bottom arrow).

We restrict our attention to discrete time systems as, for example, in [8,43], and we assume that enforcement mechanisms can only proactively cause actions within a time-step, just before a $tick$ of time. For example, if the target system needs to take an action $a$ within the deadline d, the enforcement mechanism can, before some $tick$ within the deadline d, cause the system to take the action $a$ , depicted by the second to last arrow. For this, we shall assume that there is a global notion of time known by all systems. We will, without loss of generality, indicate the passage of time with the $tick$ action, which we formally include among the target system actions.

2.2. Soundness of the enforcement mechanism

Recall that the objective of the enforcement mechanism is to regulate the target system so that its observable actions conform to a (timed) security policy. However, whether the mechanism can actually achieve this depends (1) on the exact method of synchronization between the target system and the enforcement mechanism and (2) what timing guarantees they both provide. We discuss these aspects next.

Synchronization. The key question is how uncontrollable actions may interleave with controllable ones, both within the target system and within the enforcement mechanism. Here is an example where we write $? a$ for a request to perform the action a, and $! a$ for the grant to do a (without causation), and simply a for the system performing the action a. Suppose that we have a policy that disallows a to be executed after a d action has been executed. Now suppose further that a is controllable but d is not. Then the target system must obtain permission before executing a. If the target system and enforcement mechanism communicate asynchronously, we may have the following sequence of actions: $\begin{matrix} ? a d! a a . \end{matrix}$ That is, the target system requests permission to execute a, executes d while it is waiting, while the request for permission to execute a is still on its way to the enforcement mechanism, the target system gets permission $! a$ , and finally executes a. The result is that d is executed before a even though the policy does not allow it and the enforcement mechanism is not aware of the reversed order.

The simple solution to problems like the above is to assume that the target system and the enforcement mechanism operate synchronously; for example, the target system suspends operation while waiting for a request to the enforcement mechanism to complete.

In practice, it may be possible to avoid such draconian measures. E.g., we may exploit additional knowledge about the sequencing of target system operations: some uncontrollable actions may be known to not happen in certain system states. For instance, we may safely assume that the uncontrollable action “engine failure detected” does not happen when the engine is not engaged. Alternatively, we may be in the fortunate position that the security policy is closed under commutation of uncontrollable and other actions within some time limit. A policy like “the uncontrollable action d must be followed by action a within 3 seconds” has this property: If we guarantee that the follow-up action a happens 2.5 seconds after d, we can safely commute d with arbitrary other actions within the first 2 seconds.

Time. Since our security policies are timed policies, the enforcement mechanism must itself be fast enough to process requests from the target system, and the target system must be fast enough in executing any caused sequences of actions.

Recall that we work with a discrete time model: Time advances in ticks, with some number of actions happening between ticks. Consider the policy “in every time period (between two consecutive ticks), the action b must happen.” We can imagine that the target system attempts to execute b, but the enforcement mechanism uses so much time processing the request $? b$ that we miss the deadline.

We resolve this situation by making real-time assumptions. Namely, we assume that the actions of the target system will always fit inside a tick. If requests happen seldomly and slowly enough that the enforcement mechanism can “keep up” and the target system similarly “keeps up” with caused events, we can avoid the above unfortunate situation. More specifically, we assume upper bounds on the rate of actions by the target system, the round-trip time between the target system and the enforcement mechanism, and the processing time of the target system. Altogether, these bounds limit the number of actions per time unit that can be undertaken by the target system. Taking a “tick” to be such a time unit, we avoid the above unfortunate situation.

Establishing semantic assumptions. The theory we will present only guarantees that the enforcement mechanism will observe actions conforming to the given security policy, under implicit assumptions about the enforcement mechanism being “fast enough.” For a concrete application of our theory, it is necessary also to establish that this “correctness at the enforcement mechanism” entails also “correctness at the target system.” We conclude this section with a few examples of system where such correctness can reasonably be established.

The enforcement mechanism and the target system are truly synchronous and therefore the enforcement mechanism controls when the target system acts. This means that the target system is incapable of taking actions of any kind while waiting for responses from the enforcement mechanism. Examples of such a setup include a target system controlled by a virtual machine, a debugger, or an instrumented CPU, which pauses the target system after each processing step while making enforcement decisions, and which causes actions by direct manipulation of the data and code of the target system.

The tolerances for the timing of uncontrollable events are such that the causable actions may pre-empt them, provided the causable actions do so only with negligible impact on the timing of uncontrollable actions. Think of an operating system handling keyboard inputs, where a keystroke is an uncontrollable action: The human operating the keyboard will neither perceive nor care about his input being delayed a few milliseconds while, say, the operating system is executing enforcement mechanism instructions to log network packets.

The causable actions and uncontrollable actions are independent in the sense of Mazurkiewicz [39] (see also [52]). That is, we assume that the target system is such that we cannot meaningfully distinguish between uncontrollable actions before, during, or after causable actions. Think of an enforcement mechanism inserting an access control check before database access inside a web application, where new TCP connections from clients constitute the uncontrollable actions. The access control actions have no bearing on opening TCP connections and vice versa and the two sets of actions can be processed, indeed interleaved, in any order.

2.3. Target system and policies

Prior to formalizing systems and policies, we first introduce relevant notation. For a finite alphabet Σ of actions, we write $Σ^{*}$ for the set of finite words over Σ as usual, and we refer to a set $L$ of words as a language. We write the concatenation of words v and w as $v \cdot w$ and write $v ⊑ w$ iff v is a prefix of w, i.e. $w = v \cdot v^{'}$ for some word $v^{'}$ . We write $w ∖ x$ for the word w with every occurrence of the symbol $x \in Σ$ removed. Finally, we let $prefixes (L)$ be the prefix closure of the language $L$ and write ϵ for the empty word.

We now turn to our system model. A target system is a language over an alphabet comprising uncontrollable actions, controllable actions, causable actions, and time. We account for time by including a special $tick$ action in our alphabet, where the passage of time is indicated by tick’s occurrence.

Definition 1.
A target system $(S, Σ, Γ, Δ)$ is a prefix closed language $S \subseteq Σ^{}$ , with $tick \in Σ$ , controllable actions* $Γ \subseteq Σ ∖ {tick}$ , and causable actions $Δ \subseteq Σ ∖ {tick}$ .

In this definition, prefix closure formalizes that the target system S produces actions consecutively. The progression of time is modelled by $tick$ , which is neither controllable nor causable, as time’s progression can be neither suppressed nor caused. All other actions can be controllable, causable, both, or neither. We consider only finite behaviors of the target system since our focus is on the enforcement of safety properties in the form of provisions and obligations with associated deadlines.

We note that if the target system contains the string $a_{1} a_{2} tick a_{3} \in S$ , it means that the enforcement mechanism observes $a_{1}$ , followed by $a_{2}$ , followed by observing that time advances, before finally observing $a_{3}$ .
Definition 2.
A security policy $P$ over an alphabet Σ is a prefix-closed language $P \subseteq Σ^{*}$ .
Example 3.
As a first simple example, consider the informal policy over the actions $Σ_{1} = {a, b, c, tick}$ that “ $a$ must not occur”. This policy, which we call $P_{1}$ , is clearly prefix-closed. We can express it as the language of the regular expression ${(b + c + tick)}^{⋆}$ .
Example 4 (Provisions).

Consider the informal policy over the actions $a$ and $b$ that “ $b$ can only happen within 1 second after $a$ .” This is an example of a timed provision. Taking $tick$ to signify the passage of time, e.g., a second, this policy is upheld by the strings $a$ and $a b tick$ , but violated by the string $b$ and $a tick tick b$ . As a first attempt, we may model this policy as the prefix closure of the language $P_{2}$ characterized by the regular expression $\begin{matrix} (1) & {(tick + a {(a + b)}^{⋆} tick)}^{⋆} . \end{matrix}$ That is, a $b$ is allowed whenever there has not been a tick since the last $a$ . It is sometimes more helpful to specify a policy language not as a regular language defined via a regular expression, but rather as a finite automaton recognizing the same language. Here is an automaton for the language above:

However, this example also highlights a discrepancy between, on the one hand, the formalization of time as discrete time steps, which progresses only on the $tick$ action and, on the other hand, the continuous progress of time. According to the discrete formalization, the first $a$ and $b$ in the string $a b tick a$ will both happen at time t, yet still in the order first $a$ then $b$ . In contrast, the second $a$ happens at time $t + 1$ . The string $a a tick b$ is then a counterexample because $a$ happens at time t and $b$ at time $t + 1$ .

Note that, since the real time of the system is progressing continuously, this has the consequence that the above policy will both reject valid sequences and permit invalid sequences. For example, in the sequence $a tick b$ it may be the case that $a$ and $b$ happened almost simultaneously ( $a$ just before and $b$ just after the $tick$ ); or it may be the case that they happen almost two ticks apart ( $a$ just after the previous tick and $b$ just before the next). One therefore must choose a granularity of ticks small enough that the relevant time intervals can be represented with an acceptable precision. In the above example, assume that time $δ = 1 / n$ passes between ticks, for some natural number $n ⩾ 1$ . We can then define a formal policy where b will be allowed if it occurs faster than $1 - δ$ seconds after $a$ , but possibly denied incorrectly if it occurs after $1 - δ$ seconds and before $1 + δ$ second after, and only correctly denied if it happens at least $1 + δ$ second after $a$ . Clearly, choosing $δ = 1$ makes the formalization too imprecise, since $b$ may be rejected arbitrarily close to $a$ and will only be guaranteed to be rejected if it happens at least 2 seconds after $a$ . Choosing a smaller granularity means that the formalization of the policy must keep record of the intermediate time steps until one second has passed. This makes both regular expressions and standard finite automata practically unhelpful formalisms, since the size of the formalization will grow substantially; we propose in Section 7 an alternative modelling formalism that does not require all sequencing of ticks and actions to be modelled explicitly.

Example 5 (Obligations).

Consider the informal policy over the actions $a$ and $b$ that “when $a$ happens, $b$ must subsequently happen within 1 second.” This is an example of a timed obligation. We model this policy, $P_{3}$ , as the prefix closure of the language characterized by the regular expression: $\begin{matrix} (2) & {({(b + tick)}^{⋆} a a^{⋆} b)}^{⋆} . \end{matrix}$ (As in the previous example, the time granularity should in be chosen so the imprecision is acceptable). Below is an alternative formalization of this policy given by an automaton recognizing the prefix-closure of that language.

Note that the right-most state, representing the state in which $b$ is required before the next $tick$ , is still accepting; it must be for the policy to be prefix-closed. In general, obligations to act are captured not by having non-accepting intermediary states, but rather (like here) by having states where $tick$ , the passage of time, is not enabled.

Note that our notion of policy does not require time to progress. Whereas in practice time will progress, our formal development of enforcement mechanism, transparency, and soundness in the following sections does not in fact depend on this assumption. In particular, this means our results can be applied in settings where time is irrelevant. Hence we work in the more general setting without this assumption.

3. Enforcement mechanisms

3.1. Formalization

Our system model formalizes an enforcement mechanism that can replace each single input action x with either nothing (so it suppresses x), x itself (no-op), or a sequence of caused events (insertions) followed by x or nothing. Hence our enforcement mechanism constitutes a variant of a Mealy machine adapted to our system model. The output language is $Σ^{⋆}$ , and we shall call the machine’s “output” component the replacement function and the machine’s “transition” component the state update function.

Definition 6 (Enforcement mechanism).

Let $T = (S, Σ, Γ, Δ)$ be a target system and let $P$ be a policy. An enforcement mechanism $M = (E, r, u, e_{0})$ for T and $P$ consists of a set E of (enforcement) states, a replacement function $r : Σ \times E \to Σ^{*}$ , a state update function $u : Σ \times E \to E$ , and an initial state $e_{0}$ . The replacement function must satisfy for all $e \in E$ :

$r (tick, e) \in Δ^{*} tick$ ,

for all $a \in Γ$ , $r (a, e) \in Δ^{*} (ϵ + a)$ , and

for all $a \notin Γ \cup {tick}$ , $r (a, e) = a$ .

These conditions formalize that the mechanism respects time, causability, and controllability in accordance with the cases (A)–(C) of our system model on page 250. In Definition 6, Condition (1) says that the replacement function may insert any sequence of causable actions before time progresses. This intervention is justified by (B), in particular the principle that the enforcement mechanism may plan executions “in the nick of time.” Condition (2) says that controllable actions can be preceded by causable actions and optionally also suppressed. This intervention is justified by (A). Finally, Condition (3) says that uncontrollable actions must always be taken when present, which follows directly from (C).

An enforcement mechanism gives rise to an enforcement function, which modifies an input sequence by repeatedly applying both the replacement and update functions.

Definition 7 (Enforcement function).

An enforcement mechanism $M = (E, r, u, e_{0})$ defines an enforcement function $[[M]] : Σ^{*} \to Σ^{*}$ by the assignment $[[M]] (σ) = m (σ, e_{0})$ , where $m : Σ^{*} \times E \to Σ^{*}$ is defined recursively as follows: $\begin{array}{c} m (ϵ, e) = ϵ \\ m (a \cdot σ, e) = r (a, e) \cdot m (σ, u (a, e)) . \end{array}$

Example 8.
Recall the policy $P_{1}$ stating that “ $a$ must not occur” from Example 3 given by the language ${(b + c)}^{⋆}$ over the alphabet $Σ_{1} = {a, b, c, tick}$ . Assume the target system has the language $Σ_{1}^{⋆}$ and that the action $a$ is controllable. We can enforce this policy using the enforcement mechanism $M_{1} = ({e}, r_{1}, u_{1}, e)$ , where the replacement function $r_{1}$ is given by $\begin{matrix} r_{1} (x, e) = \{\begin{array}{ll} ϵ & when x = a \\ x & otherwise \end{array} \end{matrix}$ and the state update function $u_{1}$ is the constant function $u_{1} (x, e) = e$ . It is straightforward to check that $M_{1}$ is an enforcement mechanism and that the corresponding enforcement function $[[M_{1}]] : Σ_{1}^{⋆} \to P_{1}$ maps words in ${a, b, c, tick}^{⋆}$ to ${b, c, tick}^{⋆}$ by removing all occurrences of $a$ from its input string.

In terms of notation, it will be convenient to represent enforcement mechanisms graphically, using a notation similar to that of edit automata [35,36] and deterministic Mealy automata. Given an enforcement mechanism $M = (E, r, u, e_{0})$ , we represent it as a graph with the enforcement states E as nodes, and edges $s \to t$ labelled with $a / b$ whenever $r (a, s) = b$ and $u (a, s) = t$ . The initial state $e_{0}$ is indicated with an arrow from “start”. Since enforcement mechanisms define prefix-closed languages, all states are final.
Example 9.
We graphically depict the enforcement mechanism $M_{1} = ({e}, r_{1}, u_{1}, e)$ from Example 8. When we have multiple edges between the same node or pairs of nodes, as is the case here, we draw just a single edge with multiple labels.

A key technical property of enforcement functions is that they operate on input sequences an event at a time. Given an input sequence $a \cdot σ$ , and an enforcement function in state e, the corresponding output sequence will be $r (a, e)$ followed by $[[M]] (σ, u (a, e))$ .

Notation. Given a function $f : X \times Y \to Y$ , let $f^{⋆} : X^{⋆} \times Y \to Y$ denote the function that recursively “folds” f over a word from $X^{⋆}$ , defined by: $\begin{array}{c} f^{⋆} (ϵ, y) = y \\ f^{⋆} (x \cdot σ, y) = f^{⋆} (σ, f (x, y)) . \end{array}$
Lemma 10.
Let $M = (E, r, u, e_{0})$ be an enforcement mechanism. For all $σ \in Σ^{⋆}$ and $a \in Σ$ . Then $\begin{array}{c} (3) & [[M]] (σ \cdot a) = [[M]] (σ) \cdot r (a, u^{⋆} (σ, e_{0})) \\ (4) & m (σ \cdot a, e_{0}) = m (σ, e_{0}) \cdot r (a, u^{⋆} (σ, e_{0})) . \end{array}$
Proof.
By induction on σ, we have that $m (σ \cdot σ^{'}, e) = m (σ, e) \cdot m (σ^{'}, u^{⋆} (σ, e))$ . Equations (3) and (4) immediately follow. □

A monotone function on words is one where if $v ⊑ w$ then $m (v) ⊑ m (w)$ . If an enforcement function is monotone, then intuitively all decisions made by the enforcement mechanism are final in the sense that past decisions will not be changed upon discovering future actions. It is straightforward to see that any enforcement mechanism gives rise to a monotone enforcement function. Lemma 11.
For any enforcement mechanism $M$ , the enforcement function $[[M]]$ is monotone.
Proof.
We must show for any σ, τ that $[[M]] (σ) ⊑ [[M]] (σ \cdot τ)$ . We have: $\begin{aligned} [[M]] (σ \cdot τ) & = m (σ \cdot τ, e_{0}) & by definition \\ = m (σ, e_{0}) \cdot m (τ, u^{⋆} (σ, e_{0})) & by Lemma 10(4) \\ = [[M]] (σ) \cdot m (τ, u^{⋆} (σ, e_{0})) & by definition. \end{aligned}$ Hence $[[M]] (σ \cdot τ) ⊒ [[M]] (σ)$ . □

3.2. Soundness and transparency

We start with the core requirement for an enforcement mechanism: it upholds the given policy.

Definition 12 (Soundness).

Let $P$ a policy. An enforcement mechanism $M$ is sound $P$ iff its range $[[M]]$ is contained in $P$ , that is, iff for all $σ \in Σ^{*}$ we have $[[M]] (σ) \in P$ .

Note that the enforcement mechanism is sound with respect to a policy and not any particular target system. That is, a sound enforcement mechanism can be combined with any target system and the result will conform with the given policy.

Example 13.
The enforcement mechanism $M_{1}$ in Example 8 is sound with respect to the policy $P_{1}$ stating that “ $a$ must not occur.” This is because the codomain of the enforcement function $[[M_{1}]]$ is contained in this policy.

However, soundness is only part of the story. Enforcement mechanisms are traditionally also required to be transparent. This is formulated in [35, p. 5] as:
An enforcement mechanism must preserve the semantics of executions that already obey the property in question.
For example, in Example 8, if all actions in $Σ_{1}$ were controllable, then a sound enforcement mechanism might simply suppress all strings. This would not be transparent for the policy “ $a$ must not occur”. Moreover, this is not the policy’s intention as it does not forbid occurrences of b and c.

The informal definition cited above is compatible with most formal notions of transparency given in the literature, also under other names. For example, the notion of “precise enforcement” [35, Definition 2] prohibits enforcement from modifying the target system actions when the target system stays within the policy. The notion of “effective enforcement” [35, Definition 3] relaxes this requirement, whereby the enforcement mechanism may modify the target system only up to a system-specific equivalence.

We argue that these previous notions are all too weak. In particular, they all release the enforcement mechanism from all obligations after the target system has transgressed once. Namely, if the target system ever attempts to violate the policy, even just once, the enforcement mechanism is subsequently completely free to modify the target system’s behavior, even if the target system never attempts further transgressions. Hence we strengthen this requirement to the point where the enforcement mechanism must admit any additional actions that are policy-compatible with the corrected behavior of the target system observed so far.
Definition 14 (Transparency).

Let $M$ be an enforcement mechanism for a target system $(S, Σ, Γ, Δ)$ and a policy $P$ . We say that $M$ is transparent iff for all $σ \in Σ^{⋆}$ and $a \in Σ$ , we have $[[M]] (σ \cdot a) \neq [[M]] (σ) \cdot a$ implies $[[M]] (σ) \cdot a \notin P$ .

This definition corresponds closely to the intuition that a transparent enforcement mechanism must change the target system’s behavior “as little as possible.” It follows from transparency that if $[[M]] (σ) \cdot a \in P$ then $[[M]] (σ \cdot a) = [[M]] (σ) \cdot a$ .

Example 15.
It is easy to see that the enforcement mechanism $m_{1}$ of Example 8 is transparent: It leaves its input unmodified iff that input contains no $a$ s, which is when that input is already in the policy $P_{1}$ .
Example 16.
Consider again the policy $P_{1}$ that “ $a$ must not occur.” However we now additionally assume that every action is controllable, and we construct the enforcement mechanism $M_{3}$ that suppresses all output after encountering an $a$ .

(We have again omitted $tick$ , which must in fact be admitted in both states.) The enforcement function $[[M_{3}]]$ for this mechanism would satisfy the standard notion of transparency since any string σ without $a$ s is preserved: $[[M_{3}]] (σ) = σ$ . However, this mechanism is not transparent in the sense of Definition 14, since $\begin{matrix} ϵ = [[M_{3}]] (a \cdot b) \neq [[M_{3}]] (a) \cdot b = b, yet [[M_{3}]] (a) \cdot b = b \in P . \end{matrix}$

This example may give the impression that under our notion of transparency, an enforcement mechanism must necessarily react identically to identical violations. This is not the case: although it cannot act more restrictively, it may add additional actions. We illustrate this with the following example.
Example 17.
Consider again the policy $P_{1}$ over the alphabet ${a, b, c, tick}$ . Suppose we would now like to define an enforcement mechanism $M_{4}$ that on the first violation suppresses the offending $a$ , but on subsequent violations also triggers the action $c$ , e.g., inserting a CAPTCHA after a failed attempt to access a resource without preceding authentication. For example, the enforcement function should behave as follows. $\begin{array}{c} m_{2} (a) = ϵ \\ m_{2} (b) = b \\ m_{2} (b a) = b \\ m_{2} (b a b) = b b \\ m_{2} (b a b a) = b b c \end{array}$ We can realize this enforcement mechanism as follows.

It is straightforward to verify that this enforcement mechanism is both sound and transparent.

We note a few properties of transparency. First, one can construct an enforcement mechanism that is transparent but not sound. The easy example is to take the enforcement mechanism to be the identity function, which is clearly transparent, since it never takes any corrective action. Non-trivial examples can also be constructed, which do take corrective actions, but do not always direct the target system back into the policy, or sometimes allow the system to transgress.

Second, any sound and transparent enforcement mechanism is the identity on already correct inputs; that is, our notion of transparency generalizes the traditional ones.
Proposition 18.
Let $M$ be a sound and transparent enforcement mechanism for a target system $S$ and policy $P$ . For any $σ \in P$ we then have $[[M]] (σ) = σ$ .
Proof.
By induction on σ, using the definition of transparency. □

Third, a sound enforcement function of a transparent and sound enforcement mechanism is idempotent. Recall that a function f is idempotent if $f (f (x)) = f (x)$ . For an enforcement function, this means that the mechanism would not wish to further change its own output, if presented with that output as input. Informally speaking, an idempotent enforcement function “likes its own output.”
Theorem 19.
Let $M$ be a sound and transparent enforcement mechanism for a target system $S$ and policy $P$ . For any $σ \in Σ^{⋆}$ we have $[[M]] ([[M]] (σ)) = [[M]] (σ)$ .
Proof.
Because $M$ is sound, $[[M]] (σ) \in P$ . But then by Proposition 18 $[[M]] ([[M]] (σ)) = [[M]] (σ)$ . □

Finally, we note that if a sound and transparent enforcement mechanism exists for a policy, that policy must allow time to progress. Proposition 20.
Let $P$ be a security policy. Suppose there exists a sound and transparent enforcement mechanism $M$ for $P$ . Then for all $σ \in P$ there exists $σ^{'}$ such that $σ \cdot σ^{'} \cdot tick \in P$ .
Proof.
Consider some $σ \in P$ . Because $M$ is transparent and sound, by Proposition 18 we have $σ = [[M]] (σ)$ . By Lemma 10 we have $\begin{aligned} [[M]] (σ \cdot tick) & = [[M]] (σ) \cdot r (tick, u^{⋆} (σ, e_{0})) & by Lemma 10 \\ = σ \cdot r (tick, u^{⋆} (σ, e_{0})) & by Proposition 18. \end{aligned}$ By Definition 6, Condition (1), we find that $\begin{matrix} r (tick, u^{⋆} (σ, e_{0})) \in Δ^{⋆} tick . \end{matrix}$ But then clearly for some $σ^{'} \in Δ^{⋆}$ we have $σ \cdot σ^{'} \cdot tick = M (σ \cdot tick) \in P$ . □

4. Enforcement mechanisms induce edit automata

We consider in this section the relationship between our enforcement mechanisms and edit automata introduced in [35]. Edit automata are a class of finite automata generalizing security automata [48] that can not only suppress prohibited actions but can add obliged ones. The relationship to edit automata goes beyond shared notation: an enforcement mechanism in the sense of Definition 6 directly induces an edit automaton. We follow the original presentation of edit automata, but allow ourselves the slight generalization where edit automaton may insert more than one symbol; this generalization is straightforward (but tedious and unhelpful) to remove.

Notation. We write $A ⇀ B$ to indicate the set of partial functions from A to B.

An edit automaton [35] over an alphabet Σ is a five-tuple $(S, s_{0}, δ, γ, ω)$ where

S is a set of states,

$s_{0} \in S$ is the initial state,

$δ : Σ \times S ⇀ S$ is a transition function,

$ω : Σ \times S ⇀ {+, -}$ is the suppression indicator function, and

$γ : Σ \times S ⇀ Σ^{*} \times S$ is an insertion function.

Edit automata have a labelled-transition semantics as defined in Fig. 2. They take an input in

Σ^{⋆} \times S

to a remainder input and a next state in

Σ^{⋆} \times S

, while producing an output action in Σ. For transitions to be deterministic, it is assumed that δ and ω have the same domain (there is a transition from a state iff we suppress or grant), whereas δ and γ have disjoint domains (there is a transition from a state iff we do not insert).

Fig. 2.

Edit automata semantics.

Note that we may construct an edit automaton that replaces an input symbol with a string of outputs by performing a suppression followed by insertions: Suppose in state s we wish the symbol a to be replaced with $b_{1} \dots b_{n}$ , arriving at state $s^{'}$ . Simply add a new state $\hat{s}$ and define: $\begin{array}{c} δ (a, s) = \hat{s} \\ ω (a, s) = - \\ γ (x, \hat{s}) = (b_{1} \dots b_{n}, s^{'}) for all x \in Σ . \end{array}$ We now use this technique to construct edit automata corresponding to enforcement mechanisms. We write $Δ^{+}$ to mean $Δ \cdot (Δ^{⋆})$ , that is, the set of strings comprising one or more elements of Δ.

Definition 21.

Let $T = (S, Σ, Γ, Δ)$ be a target system, and let $M = (E, r, u, e_{0})$ be an enforcement mechanism for T. The edit automaton corresponding to $M$ is $E (M) = (\hat{E}, e_{0}, δ, γ, ω)$ . This edit automaton has the same states as $M$ with the addition of intermediate states necessary for representing “replacement” as insertion followed by suppression: $\begin{matrix} \hat{E} = E \cup {(e, a) | r (a, e) \in Δ^{+} a ?} . \end{matrix}$ The initial state is the same as in $M$ , and the transition function δ, insertion function γ, and suppression indicator ω are defined as follows. Consider some $e \in E$ and $a \in Σ$ . Except where explicitly defined below, ω, δ, and γ are undefined. $\begin{array}{c} ω (a, e) = +, δ (a, e) = u (a, e) when r (a, e) = a \\ ω (a, e) = -, δ (a, e) = u (a, e) when r (a, e) = ϵ \\ \begin{array}{c} ω (a, e) = -, δ (a, e) = (a, e) \\ γ (a, (e, a)) = (r (a, e), u (a, e)) \end{array}\} when r (a, e) \in Δ^{+} a ? \end{array}$

We show that the edit automaton induced by an enforcement mechanism has the same semantics as the enforcement mechanism, in the sense that whenever the edit automaton consume its input and outputs a sequence α, then the enforcement mechanism also outputs α on that same input. The converse is false, for the technical reason that the edit automaton consumes remaining input and terminates when faced with a situation it does not know how to response to, whereas the enforcement function in that case is undefined. Recall from Definition 7 that an enforcement mechanism $M$ gives rise to an underlying enforcement function m.

Proposition 22.

Let T be a target system, $M$ be an enforcement mechanism for T, and $E (M)$ the induced edit automaton. Then for all input sequences σ and states $e, e^{'} \in E$ , $\begin{matrix} (5) & if (σ, e) \overset{α}{\Rightarrow} (ϵ, e^{'}) for E (M) then u^{⋆} (σ, e) = e^{'} and m (σ, e) = α for M . \end{matrix}$

Proof sketch.

By induction on σ.

Base case. Assume $σ = ϵ$ . From the edit automaton rules in Fig. 2, we see that only [A-Reflex] and then [E-Stop] applies, so $α = ϵ \cdot \dots \cdot ϵ = ϵ$ and $e^{'} = e$ . By definition, also $u^{⋆} (ϵ, e) = e$ and $m (ϵ, e) = ϵ$ .

Inductive step. Assume that $σ = σ^{'} \cdot a$ and suppose that $(σ \cdot a, e) \overset{α}{\to} (ϵ, e^{'})$ . By inspection of the edit automata rules in Fig. 2, we have $\begin{matrix} (σ \cdot a, e) \overset{α^{'}}{\Rightarrow} (a, e^{″}) \overset{α^{″}}{\Rightarrow} (ϵ, e^{'}), \end{matrix}$ with $e^{″} \in E$ . By the induction hypothesis, $\begin{matrix} u^{⋆} (σ, e) = e^{″} and m (σ, e) = α^{'} . \end{matrix}$ We proceed by rule inversion on the first step of $(a, e^{″}) \overset{α^{″}}{\to} (ϵ, e^{'})$ . Note that by assumption $e^{'} \in E$ . We prove, in all cases, that $m (a, e^{″}) = α$ and $u (a, e^{″}) = e^{'}$ . The result follows from the induction hypothesis (5) and Lemma 10, Equation (4).

[E-StepA] Because this rule applies, $ω (a, e^{″}) = +$ . By Definition 21, $r (a, e^{″}) = a$ and $e^{'} = δ (a, e^{″}) = u (a, e^{″})$ . We conclude that $α = a = r (e^{″}, a) = m (a, e^{″})$ .

[E-StepS] Because this rule applies, $ω (a, e^{″}) = -$ . Then by Definition 21, either (i) $r (a, e^{″}) = ϵ$ or (ii) $r (a, e^{″}) \in Δ^{+}$ . In case (i), clearly $α^{″} = ϵ = m (a, e^{″})$ and $e^{'} = δ (a, e^{″}) = u (a, e^{″})$ . In case (ii), we must have that $δ (a, e^{″}) = (a, e^{″})$ and $γ (a, (e^{″}, a)) = (r (a, e^{″}), u (a, e^{″}))$ . It follows that $e^{'} = u (a, e^{″})$ and $\begin{matrix} (a, e^{″}) \overset{ϵ}{\to} (a, e^{″}) \overset{r (e^{″}, a)}{\to} (ϵ, e^{'}), \end{matrix}$ whence $m (a, e^{″}) = r (a, e^{″}) = α^{″}$ . [E-Ins]: Because this rule applies, $γ (a, e^{'})$ is defined. But since $e^{″} \in E$ , $γ (a, e^{″})$ is not defined: By inspection of Definition 21, γ is only defined at states $(a^{'}, e^{‴}) \in \hat{E} ∖ E$ . □

5. Representing policies as finite automata

In this section, we shall show how to automatically derive sound and transparent enforcement mechanisms from policies specified as finite automata. The key insight will be that automata defining policies implicitly give rise to proactive enforcement mechanisms.

5.1. Automata defining policies

Since we are interested in timed obligations and provisions, we require an automata model supporting an appropriate notion of time. There are various such models and we will use one based on an explicit representation of the passage of time as a $tick$ action. Recall that a finite automaton $(Σ, S, δ, s_{0}, F)$ comprises an alphabet Σ, a set of states S, a partial transition function $δ : S \times Σ ⇀ S$ , an initial state $s_{0} \in S$ , and a subset $F \subseteq S$ of final states. A string σ is accepted by the automaton if $δ^{⋆} (σ, s_{0})$ is defined and in F, and the language of the automaton is its set of accepted strings.

Notation. Recall the notation $f^{⋆}$ defined on page 256. We use this notation to extend a transition functions δ of finite automata to strings: For a sequence $a_{1} \dots a_{n}$ and a state s, we have $δ^{⋆} (a_{1} \dots a_{n}, s) = δ^{⋆} (a_{2} \dots a_{n}, δ (a_{1}, s))$ and so forth. That is, $δ^{*} (a_{1} \dots a_{n})$ computes the state reached after following the string $a_{1} \dots a_{n}$ . Obviously, whether $δ^{⋆}$ is defined depends on δ.

Definition 23.
A policy automaton over Σ is a finite automaton $(Σ, S, δ, s_{0}, F)$ such that $tick \in Σ$ and $F = S$ , that is, every state is final. We omit F when defining such automata.

These automata define policies via their associated language. As we require that policies are prefix closed (see Definition 2), our policy-defining automata are everywhere accepting.
Lemma 24.
Let A be a policy automaton over Σ. Then the language $L (A)$ of A is a security policy.
Proof.
By Definition 2, we must show that $tick \in Σ$ and that $L (A)$ is prefix closed. But these are both immediate given the definition of policy automaton. □
Example 25.
Recall the policy “when $a$ happens, $b$ must subsequently happen within 1 second” from Example 5. It is straightforward to construct a policy automaton generating this language; we give one in Fig. 3a on the following page. Although the automata in this figure are superficially similar to the graphs of enforcement mechanisms of the previous sections, they denote another kind of object: the latter is a finite automata, whereas the former are Mealy machines. Moreover, the latter recognize a language, whereas the former indicate how to suppress or substitute some actions for others.
Example 26.
Consider the policy over the actions $a$ and $b$ from Example 4 stating that “ $b$ can only happen within 1 second after $a$ .” It is again straightforward to construct a policy automaton generating this language; Fig. 3c on the next page provides an example.

Fig. 3.
Examples of policy automata and induced mechanisms. Dashed edges indicate where the resolver is used.
5.2. Deriving enforcement mechanisms

The question we now address is: given security policies specified as finite automata, like those in Figs 3a and 3c, how do we construct a sound and transparent enforcement mechanism for that policy? To this end, we introduce a device called a resolver. A resolver f for a policy automaton F tells us how to find a path $f (a, s) = a_{1}, \dots, a_{n}$ from a state s where a requested action a is not available to a state where it is. We use this path to proactively enforce the requested action a: Instead of denying a, we instruct the target system to follow the path $f (a, s)$ , forcing it to arrive at a state where a is available.

Definition 27 (Resolver).

Let $F = (Σ, S, δ, s_{0})$ be a policy automaton over Σ, let $Δ \subseteq Σ ∖ {tick}$ , and suppose $f : Σ \times S ⇀ Δ^{*}$ is a partial function. We say that f is a Δ-resolver for F iff whenever $s \in S$ and $a \in Σ$ such that $f (a, s)$ is defined, then $δ^{⋆} (f (a, s) \cdot a, s)$ is also defined.

When a policy automaton has resolver that is defined for all non-controllable actions, we can then derive an enforcement mechanism from the policy automaton.

Definition 28.
Let F be a policy automaton over Σ, suppose $Δ, Γ \subseteq Σ ∖ {tick}$ , and let f be a Δ-resolver for F. We say that F is resolvable at(Δ, Γ, f) iff for all $a \in Σ$ and $s \in S$ either
$δ (a, s)$ is defined, or

$a \in Σ$ and $f (a, s)$ is defined, or

$a \in Γ$ .

These conditions say that either (1) the policy automaton is willing to do the action a outright, or (2) the requested action a is a tick, and the policy automaton can get to a state where it can do a using only causable actions, or (3) it has the power to deny a.

Ad (2), for the notion
Definition 29.
Let $F = (Σ, S, δ, s_{0})$ be a policy automaton over Σ that is resolvable at $(Δ, Γ, f)$ . Define the update and replacement functions $u : Σ \times S \to S$ and $r : Σ \times S \to Σ^{⋆}$ as follows: $\begin{array}{c} u (a, e) = \{\begin{array}{ll} δ (a, e) & when defined \\ δ^{⋆} (f (a, s) \cdot a, s) & when δ (a, s) not defined and f (a, s) defined \\ e & when neither δ (a, s) nor f (a, s) defined \end{array} \\ r (a, e) = \{\begin{array}{ll} a & when δ (a, s) defined \\ f (a, e) \cdot a & when δ (a, s) not defined and f (a, s) defined \\ ϵ & when neither δ (a, s) nor f (a, s) defined . \end{array} \end{array}$ The induced enforcement mechanism is then defined as $M (F) = (S, r, u, s_{0})$ .

We must justify this definition by proving that $M (F)$ is in fact an enforcement mechanism.
Lemma 30.
Let $F = (Σ, S, δ, s_{0})$ be a policy automaton resolvable at $(Δ, F, f)$ , and write u, r for the induced update and replacement functions from Definition 29 . Then $M (F) = (S, r, u, s_{0})$ is an enforcement mechanism.
Proof.
We must show that the replacement function r satisfies Conditions 1–3 of Definition 6.

(1) Consider some $s \in S$ ; we must show $r (tick, e) \in Δ^{} tick$ . We proceed by case analysis on Definition 28. If $δ (tick, e)$ is defined, then $r (tick, e) = tick \in Δ^{} tick$ . Otherwise, if $f (tick, e)$ is defined, then $r (tick, e) = f (tick, e) \cdot tick \in Δ^{} tick$ . Otherwise $tick \in Γ$ , which contradicts Definition 28.

(2) Consider some $s \in S$ and $a \in Γ$ ; we must prove $r (a, s) \in Δ^{} (ϵ + a)$ . We proceed by case analysis on Definition 28. If $δ (a, s)$ is defined, then $r (a, s) = a \in Δ^{} (ϵ + a)$ . Otherwise, if $a \in Γ$ and $f (a, s)$ is defined, then $r (a, s) = f (a, s) \cdot a \in Δ^{} (ϵ + a)$ . Otherwise $a \in Γ$ , which contradicts Definition 28. Otherwise we must have $a \in Γ$ and neither defined, in which case $r (a, s) = ϵ \in Δ^{} (ϵ + a)$ .

(3) Consider some $s \in S$ and $a \notin Γ \cup {tick}$ ; we must prove $r (a, s) = a$ , which we do by case analysis on Definition 28. If $δ (a, s)$ is defined, then $r (a, s) = a$ . Otherwise, (2) $a \in Γ \cup {tick}$ or (3) $a \in Γ$ , but these both contradict the assumption $a \notin Γ \cup {tick}$ . □

We proceed to prove that the induced enforcement mechanism is both sound and transparent. For this result, we will need the following lemma, which says that running an output of the induced enforcement mechanism through the original automaton yields the same state as if one had simply iterated the induced mechanism’s state update function. Lemma 31.
Let F be a policy automaton resolvable at* $(Δ, F, f)$ , write u, r for the induced update and replacement functions from Definition 29 , let e be a state of F, and let m be associated with $M (F)$ as defined in Definition 7 . Then $\begin{matrix} u^{⋆} (σ, e) = δ^{⋆} (m (σ, e), e) \end{matrix}$ with both sides of the equality always defined.
Proof.
By induction on σ. The base case is trivial. In the inductive step, because F is resolvable we may proceed by cases on the three conditions in Definition 28; each case corresponds directly to a defining clause in Definition 29. It is now straightforward to verify each individual case. □
Theorem 32.
Let F be a policy automaton over Σ that is resolvable at $(Δ, Γ, f)$ . Then $M (F) = (S, r, u, s_{0})$ is a (i) sound and (ii) transparent enforcement function for the policy $L (F)$ .
Proof.
(i) $M (F)$ is sound. We must prove that the range of the enforcement function $[[(S, r, u, s_{0})]]$ is contained in $L (F)$ . Take m as given in Definition 7; it is sufficient to prove that for any $σ \in Σ^{⋆}$ we have $m (σ, s_{0}) \in L (F)$ . But this follows from Lemma 31 and the definition of m.

(ii) $M (F)$ is transparent. We must prove that for all $β \in Σ^{⋆}$ and $a \in Σ$ , we have $[[M]] (β \cdot a) \neq [[M]] (β) \cdot a$ implies $[[M]] (β) \cdot a \notin L (F)$ . But this is immediate since for all $a \in Σ$ and $s \in S$ , $r (a, s) \neq a$ iff $δ (a, s)$ not defined. □
Example 33.
(i) A denying resolver. Consider the automaton specifying the provision policy of Fig. 3c. A resolver for this automaton must handle the situation that either $a$ never occurred, or it occurred more than one tick ago, yet the target system attempts to execute $b$ . We use the everywhere undefined function ⊥ as the resolver. This resolver never knows what to do, and so the enforcement mechanism it induces simply denies actions for which δ is undefined, that is, the attempt to execute $b$ . We show the resulting induced enforcement mechanism in Fig. 3d. To make clear where the resolver is used, we draw the corresponding edges as dashed edges.

Here is an example application of this enforcement mechanism denying an attempt to execute $b$ in a situation where there was no $a$ within the last $tick$ : $\begin{array}{r} a \cdot b \cdot tick \cdot b \mapsto a \cdot b \cdot tick . \end{array}$

(ii) A proactive resolver. Alternatively, rather than denying $b$ , if $a$ is causable and $b$ is controllable, we can insert an $a$ before the attempted $b$ . Using the resolver function $b \mapsto a$ has this effect. This resolver proactively executes $a$ to advance to the right-most state, thereby enabling $b$ . We display the induced enforcement mechanism for this resolver in Fig. 3e.

Here is an example application of this enforcement mechanism proactively executing an a to enable b: $\begin{aligned} a \cdot b \cdot tick \cdot b \mapsto \\ a \cdot b \cdot tick \cdot \underline{a} \cdot b . \end{aligned}$

These two examples demonstrate how we may choose between (i) the traditional enforcement of provisions (deny when prerequisites are not met) by supplying a trivial resolver or (ii) the proactive enforcement of provisions by causing the prerequisites by supplying a non-trivial resolver.

(iii) Resolving a deadline in the nick of time. Finally, consider the automaton specifying the obligation-policy of Fig. 3a: When “ $a$ happens, $b$ must happen within one second.” This requirement is modelled by the right-most state not having $tick$ action: the $b$ is required before $tick$ is allowed. Just like the resolver in case (ii) above inserted an $a$ to allow a $b$ , a resolver can insert a $b$ to allow a $tick$ . We show the resulting enforcement mechanism in Fig. 3b.

Here is an example of applying the enforcement mechanism to an input string, where the enforcement mechanism inserts a missing $b$ in state $o_{1}$ to pave the way for a $tick$ : $\begin{aligned} b \cdot tick \cdot b \cdot a \cdot a \cdot tick \mapsto \\ b \cdot tick \cdot b \cdot a \cdot a \cdot \underline{b} \cdot tick . \end{aligned}$

5.3. Towards larger policies

The examples from Section 2.3 that we have used until now have been designed to be small and suitable for illustrations. We now provide part of a larger, more realistic example: a health-care data retention policy as might be found in regulations like HIPAA [9]. We use this example, taken from [3, Section 3.3], to illustrate here policies specified by finite automata, and subsequently, in Section 6, policies specified declaratively using DCR processes.

The policy targets hospitals, which must balance the dual requirements of protecting patients’ privacy while documenting the treatments given and the procedures followed. The tension between doctors collecting and using data and hospitals protecting the data over the long-term is resolved by retaining patient records in a central hospital database during the treatment and moving the records to an access restricted archive shortly after the patient’s release. In practice, the associated policy might look like this:

Records must be archived and deleted within 14 days of the patient’s release, unless the patient is re-admitted within those 14 days.

Records cannot be deleted unless they have been previously archived after the patient’s last release.

Records must not be unarchived before at least 8 years have passed after they were last archived

Records can not be deleted, archived, or unarchived while the patient is admitted to the hospital.

Table 1
Policy activities

Action Significance Mechanism’s control

$release$ The patient is released

$delete$ The patient’s records are deleted from the central database Causable, controllable

$archive$ The patient’s records are copied from the central database to the restricted long-term archive Causable, controllable

$unarchive$ The archived records are deleted Causable, controllable

$readmit$ The patient is re-admitted

Action	Significance	Mechanism’s control
$release$	The patient is released
$delete$	The patient’s records are deleted from the central database	Causable, controllable
$archive$	The patient’s records are copied from the central database to the restricted long-term archive	Causable, controllable
$unarchive$	The archived records are deleted	Causable, controllable
$readmit$	The patient is re-admitted

We list the actions associated with this policy in Table 1. Note that for simplicity and clarity, in our formalization we will consider only a single fixed patient and set of records.

Rule 1 can be split in two parts, the first part stating that “Records must be archived within 14 days of the patient’s release, unless the patient is re-admitted within those 14 days.” and the other part stating that “Records must be deleted within 14 days of the patient’s release, unless the patient is re-admitted within those 14 days.”

Fig. 4.

Automaton for first part of rule 1: “Records must be deleted within 14 days of release, unless the patient is re-admitted within those 14 days.”

Fig. 5.

Automaton for second part of rule 1: “Records must be archived within 14 days of release, unless the patient is re-admitted within those 14 days.”

We give finite automata corresponding to the two parts of the rule in Figs 4 and 5. Note that we use labels like $\neg {release}$ as shorthand for a set of transitions for any label different from $release$ . If a tick represents an hour, then each of the automata has 339 states. Even if we let a tick represent a day, reducing the state space to 17 states, it is not easy to figure out which rule is encoded by looking at the automaton.

The automaton corresponding to a policy consisting of both parts of the rule is obtained as a (synchronous) product automaton of the two automata, i.e. an automaton with states being pairs $(s_{1}, s_{2})$ of states, where $s_{1}$ is a state of the first automaton and $s_{2}$ is a state of the second automaton. We show (to the best of our ability) this product automaton in Fig. 6 on page 269. There is a transition with label a from a state $(s_{1}, s_{2})$ to a state $(s_{1}^{'}, s_{2}^{'})$ if there are transitions with label a from $s_{i}$ to $s_{i}^{'}$ for $i \in {1, 2}$ . The product automaton has 114921 states, again assuming a tick represents an hour. It has 1013 reachable states.

Fig. 6.

Automaton for rule 1: “Records must be deleted and archived within 14 days of release, unless the patient is re-admitted within those 14 days.”

Even in this simplified setting, this example shows that finite automata are not always convenient for expressing policies. In particular, while automata provide a general purpose specification language, they are relatively verbose. An automaton is as large as the state space it describes, which limits its practicality for most nontrivial policies. Large state spaces may also arise as a consequence of the exponential blow up of the size of the automaton when the number of activities is increased as well as due to the representation of time as ticks. For example, when specifying the hospital data retention policy in Figs 4, 5 and 6, we must resort to meta-notation to represent “14 days worth of ticks.” One may use more complex automata models, such as timed automata or Petri Nets [49], which represent time more compactly, but the explicit state space representation remains inconvenient for policies giving rise to large state spaces. Moreover, if the policy rules are provided in natural language, as in the example above, the translation from rules to automata results in a large representational gap that must be bridged.

An alternative to explicit state-based models is to use a rule-centric, declarative specification language like a temporal or deontic logic. By using a declarative formalism, we avoid representing the state space explicitly. Moreover, textual rules like the four rules given above are often declarative in nature, fitting rule-centric formalisms much more neatly than state-based ones like finite state automata. When this is the case, the use of a declarative formalism also reduces the complexity associated with manually translating from textual descriptions to formal specifications; in the ideal case there is a one-to-one correspondence, known as the isomorphism principle [6].

In the next section, we therefore describe how to use a declarative specification language as a policy language and we propose the use of timed DCR graphs [28]. Compared to other commonly used declarative specification languages, such as LTL, DCR graphs allow us to compute plans directly on the declarative specification. Moreover, as we will see, the semantics of DCR graphs is close enough to finite automata that we can directly apply the theory developed in the present section. Indeed, in Section 7, we show how our theory of resolvable policy automata can be combined with the DCR graph policy model to produce practically useful enforcement mechanisms for policies specified as DCR graphs.

Fig. 7.

Automaton for rule 3: “Records must be archived for at least 8 years.”

6. DCR graphs: A declarative industrial-strength policy language

In this section, we present policy dynamic condition response graphs, a sublanguage of dynamic condition (DCR) graphs, as an example of a declarative specification language and an alternative to using finite automata for specifying timed properties. Instead of specifying a policy in terms of states and transitions, a DCR graph describes (i) the causal relationships between actions declaratively in terms of condition and response relations between events labelled with actions and (ii) dynamic conflict relationships between actions in terms of exclusions and inclusions between events. A marking of the events provides an operational run-time representation. This formalism is very expressive: DCR graphs can represent the union of regular and ω-regular languages [15,41]. This means that it can represent both represent safety and liveness properties and also that it is more expressive than LTL.

The DCR formalism was introduced in [27,41] as an event-based model for specifying distributed workflows and case management processes. It has subsequently been developed into an industrial-strength policy language specifying rules for governmental case management processes [13–15,17,26,28]. In particular, the language is supported by cloud-based design tools offered by DCRSolutions.net and a process engine is available as a web service (free for academic use) and has been embedded in the commercial WorkZone Enterprise Information Management system offered by NEC Corporation.2

²
https://www.nec.com.au/solutions/data-and-applications/workzone-case-and-information-management

In the present paper, we restrict our attention to policy DCR graphs, a subclass of DCR graphs representing security policies that are only safety properties. As for the automaton models given in the previous section, the acceptance criteria for policy DCR graphs is simplified compared to general DCR graphs, as policy graphs specify prefix closed languages. Also, whereas general DCR graphs allow the specification of unbounded deadlines (representing “eventually”), policy DCR graphs only allow the specification of finitary deadlines. For this purpose, let $N_{0}$ be the set of natural numbers including 0.

6.1. Policy DCR graphs

Definition 34.
A policy DCR graph is a tuple , where
$E$ is a set of events,

$M : E \to (N_{0} \cup {⊥}) \times {⊥, ⊤} \times (N_{0} \cup {⊥})$ is a marking,

$L = Σ ∖ {tick}$ is the set of actions,

$ℓ : E \to L$ is a labelling function, labelling events with actions,

$∙ \overset{}{\leftarrow} \subseteq E \times N_{0} \times E$ is the timed condition relation,

$∙ \to \subseteq E \times N_{0} \times E$ is the timed response relation,

$◇ \leftarrow \subseteq E \times E$ is the milestone relation,

$\to + \subseteq E \times E$ is the include relation, and

$\to % \subseteq E \times E$ is the exclude relation.

An event $e \in E$ with $ℓ (e) = a$ represents a way to execute the action a. The marking M is the run-time state of the graph. A marking $M (e) = (h, i, r)$ of the event $e \in E$ is to be interpreted as follows. If $h = ⊥$ then the event has not yet been executed. If $h = n \in N_{0}$ then the last time the event e was executed is n ticks ago. If $r = ⊥$ then the event is not required to be executed within any deadline. If $r = n \in N_{0}$ then the event must be executed within n ticks. If $i = ⊥$ , the event is said to be excluded and if $i = ⊤$ included.

We represent a marking as a finite sequence of pairs of events and event states, e.g., $M = e_{1} : Φ_{1}, \dots, e_{k} : Φ_{k}$ , where $Φ_{j} = (h, i, r)$ is an event state as defined above. We understand the extension $M, e : Φ$ of such a finite sequence M to be undefined when $e \in dom (M)$ .

The five relations (arrows) regulate both which events may execute in a given marking, and how such an execution modifies that marking. Relations are sometimes called constraints because their purpose is to constrain the possible executions of the graph. In particular, a graph with no relations and an initial marking defined as $M (e) = (⊥, ⊤, ⊥)$ for all events $e \in E$ allows all possible executions.

The exclusion/inclusion relations and the associated parts of the state is a unique feature of DCR graphs: Relations from excluded events are ignored, and excluded events can not be executed. This provides a direct way to express defeasible rules as we will exemplify below in Example 35.

We write $e ∙ \overset{k}{\leftarrow} f$ as shorthand for $(e, k, f) \in ∙ \overset{}{\leftarrow}$ . This relation means that for the event e to be executed, the event f must in the current marking either previously have been executed at least k time units ago or f must be excluded. We say that this condition has delay k. When $k = 0$ , we write simply $e ∙ \overset{}{\leftarrow} f$ .

Again we write $e ∙ \overset{d}{\to} f$ as a shorthand for $(e, d, f) \in ∙ \to$ . This relation means that when e is executed, f is then required to execute within d time units, or to be excluded.

We write $e ◇ \leftarrow f$ as shorthand for $(e, f) \in ◇ \leftarrow$ . This relation means that for the event e to be executed, the event f must be either excluded or not currently required to be executed.

We write $e \to % f$ as shorthand for $(e, f) \in \to %$ . This relation means that when e is executed, it excludes f.

We write $e \to + f$ as shorthand for $(e, f) \in \to +$ , which means that when the event e is executed, the event f is included.

Below we exemplify DCR policies by formulating the rules discussed in Section 5.3. Example 35.
Recall the obligation of the hospital given Section 5.3, where the event $delete$ (“the patient’s record is deleted”) must happen within 14 days after the event $release$ (“a patient is released from the hospital”). Given the choice for the duration of a tick of one day, we specify this obligation with a timed response relation: $\begin{matrix} release ∙ \overset{14 d}{\to} delete, \end{matrix}$ where $14 d$ represents 14 days measured in ticks. If the duration of a tick were a second, then $14 d$ would be short for 1209600.

Now, the first rule of the example given in Section 5.3 also states an exception to the rule above: The deletion should happen “unless the patient is re-admitted within those 14 days.” This is exception can be modelled conveniently using the exclude relation. $\begin{matrix} readmit \to % delete, \end{matrix}$ and the include relation $\begin{matrix} release \to + delete, \end{matrix}$ to ensure that the deletion obligation is included at release, if it was previously excluded. The second part of rule one in the example is the exact same rule, just for $archive$ instead of $delete$ . This is modelled by the relations $\begin{array}{c} release ∙ \overset{14 d}{\to} archive \\ readmit \to % archive \\ release \to + archive . \end{array}$ To model the second rule, which states that records cannot be deleted unless they have been archived after the patient’s last release, we use a milestone relation $\begin{matrix} delete ◇ \leftarrow archive . \end{matrix}$ The meaning of this relation is, that if $archive$ is pending (which it will be if there has been a $release$ with no subsequent $archive$ due to the response relation $release ∙ \overset{14 d}{\to} archive$ ) then $delete$ is not enabled.

To model the provision given by the third rule, that the event $archive$ (“archiving data”’) cannot be followed by the event $unarchive$ (“delete archived data”) for at least 8 years, we use a timed condition: $\begin{matrix} unarchive ∙ \overset{8 y}{\leftarrow} archive, \end{matrix}$ where $8 y$ is short for 252460800, if the duration of a tick is a second.3
³
We ignore here the general problem of translating ticks to calendar times and the non-trivial complications with time zones, leap years, etc. that translation entails.

Finally, to model the fourth rule, which states that records cannot be deleted or archived prior to the patient’s release, we use an exclude relation from $readmit$ to $unarchive$ and include and condition relations from $unarchive$ to $delete$ , $archive$ , and $unarchive$ : $\begin{array}{c} unarchive ∙ \overset{}{\leftarrow} release \\ delete ∙ \overset{}{\leftarrow} release \\ archive ∙ \overset{}{\leftarrow} release \\ readmit \to % unarchive \\ release \to + unarchive \\ release \to + delete \\ release \to + archive . \end{array}$ The condition relations models that the three events cannot happen before $release$ has happened at least once, the exclude relation $readmit \to % unarchive$ models that $unarchive$ cannot happen if the patient is readmitted. Note that we already have exclude relations above ensuring that $delete$ and $archive$ cannot happen if the patient is readmitted. Finally, the include relations model that after release, the three actions $unarchive$ to $delete$ , $archive$ are possible again.

The complete policy given in Section 5.3 is thus modelled by 15 relations and 5 events.

6.2. Enabledness and effects

Below we formalize when an event e in a DCR graph is enabled in a given marking M and the effect on the marking M when executing e, yielding a new marking $M^{'}$ .

We extend the term notation for relations to sets of relations by writing a sequence of relation terms separated by a vertical bar. This allows us to specify and refer to a timed DCR graph as a term $[M] T$ , where M is the sequence of pairs of events and event states and T is the term for the relations. We can now define the operational model for DCR graphs: when events are enabled for execution, and what happens when they are executed.

Definition 36 (Enabled events).

Let G be a policy DCR graph with marking M. An event e of G is enabled, written $e \in enabled (G)$ , iff (a) $M (e) = (_, ⊤,_)$ and (b) $\forall f, k . e ∙ \overset{k}{\leftarrow} f$ and $M (f) = (h, ⊤,_)$ implies $h ⩾ k$ and (c) $\forall f . e ◇ \leftarrow f$ and $M (f) = (_, ⊤, r)$ implies $r = ⊥$ .

A $tick$ action can happen in a timed DCR graph G if there are no included required response events with deadline 0, defined formally by $\forall e \in E . M (e) = (_, ⊤, r)$ implies $r \neq 0$ . Assuming $tick \notin E$ , we write $tick \in enabled (G)$ to denote that the tick action can happen.

Thus enabled events (a) are included, (b) their included conditions have already been executed at least the number of time steps ago specified in the delay, and (c) have no required included milestones.

We proceed to formalize how the marking is updated when an enabled event e is executed. First, for a DCR graph G with events $E$ , marking M and $e, f \in E$ define $deadline (e) (f) = \min {d | e ∙ \overset{d}{\to} f}$ . Second, for a DCR graph G with events $E$ , we write $(e \to %)$ for the set ${f \in E | e \to % f}$ of events excluded by e; and similarly for the set $(e \to +)$ of events included by e. For the timed relations, we use the same notation and take $(e ∙ \to)$ to be the set ${e^{'} \in E | \exists d \in N_{0} . e ∙ \overset{d}{\to} e^{'}}$ of responses to e, and similarly for $(e \to +)$ and $(e \to %)$ .

Definition 37 (Execution).

Let G be a timed DCR graph, with timed marking M. When $e \in enabled (G)$ and $e \neq tick$ , the result of executing e is a new DCR graph $G^{'}$ with the same events, labels, labelling function and relations, but a new marking $M^{'}$ where $M^{'} (f) = (h^{'}, i^{'}, r^{'})$ whenever $M (f) = (h, i, r)$ and

$h^{'} = 0$ when $f = e$ ,

$h^{'} = h$ when $f \neq e$ ,

$i^{'} = ⊥$ when ( $e \to % f$ or $i = ⊥$ ) and ,

$i^{'} = ⊤$ when $e \to + f$ or ( $i = ⊤$ and ), and

$r^{'} = \min {d | e ∙ \overset{d}{\to} f}$ when $\exists d . e ∙ \overset{d}{\to} f$ and $r^{'} = r$ otherwise.

Now, the effect of executing the $tick$ event if $tick \in enabled (G)$ is a graph $G^{'}$ with the same events, labels, labelling function and relations, but a new marking $M^{'}$ defined for $e \in E$ by $M^{'} (e) = (h^{'}, i^{'}, r^{'})$ where if $M (e) = (h, i, r)$ then

$h^{'} = h + 1$ if $h \in N_{0}$ otherwise $h^{'} = ⊥$ ,

$i^{'} = i$ , and

$r^{'} = r - 1$ if $r \in N_{0}$ otherwise $r^{'} = ⊥$ .

For a timed DCR graph G represented by the term

[M] T

and

e \in E \cup {tick}

, we write

T ⊢ M \overset{e}{\to} M^{'}

to denote that

e \in enabled (G)

and

M^{'}

is the updated marking resulting from executing e in G.

Example 38.
Consider the DCR graph $\begin{matrix} (6) & [release : (⊥, ⊤, ⊥), delete : (⊥, ⊤, ⊥)] release ∙ \overset{14 d}{\to} delete . \end{matrix}$ From the marking, we can see that both the events $release$ and $delete$ have the same state: they have not been previously executed, they are included, and they are not required, i.e., they have no obligation to eventually execute. Following Definitions 36 and 37, we find that both events are enabled. After executing $release$ , the marking is updated to $\begin{array}{r} release : (0, ⊤, ⊥), delete : (⊥, ⊤, 14 d) . \end{array}$ That is, $release$ is registered as having happened now (time since execution 0 ticks ago) and $delete$ is registered with deadline $14 d$ . As a second example, consider the DCR graph: $\begin{array}{c} [archive : (⊥, ⊤, 0), unarchive : (⊥, ⊤, ⊥)] \\ unarchive ∙ \overset{8 y}{\leftarrow} archive . \end{array}$ This DCR graph has only the single enabled and pending event $archive$ , which has deadline 0 and thus must happen before time advances. The $unarchive$ event is not enabled, as it has an unfulfilled condition. Executing $archive$ yields the following marking: $\begin{matrix} archive : (0, ⊤, ⊥), unarchive : (⊥, ⊤, ⊥) . \end{matrix}$ In the new marking, $archive$ is registered as having just happened (time since execution 0 ticks ago) and is no longer required (required response state is set to ⊥). The event $unarchive$ is still not enabled, as the time since execution for $archive$ must be at least $8 y$ for $unarchive$ to be enabled.

6.3. Transition semantics

The transitions $T ⊢ M \overset{e}{\to} M^{'}$ defined in Definition 37 give rise to a timed event labelled transition system (timed event LTS).

Definition 39.
A timed DCR graph $[M] T$ defines a timed event LTS, $lts ([M] T) = (M, E^{'}, \to, M, ℓ^{'})$ , whose components are: events $E^{'} = E ⊎ {tick}$ ; transitions $\to \subseteq M \times E^{'} \times M$ , where $M \overset{e}{\to} M^{'}$ iff $T ⊢ M \overset{e}{\to} M^{'}$ ; states $M = {M^{'} | M \to^{} M^{'}}$ ; initial* state M; and event labelling defined by $ℓ^{'} (e) = ℓ (e)$ for $e \in E$ and $ℓ^{'} (tick) = tick$ .
Definition 40.
A run of $lts ([M] T)$ is a finite or infinite sequence of transitions starting from the initial state. We call a run non-Zeno if it is finite or contains infinitely many $tick$ events.

The LTS has a notion of acceptance: a run is accepting iff it is non-Zeno and every included, required response event in an intermediate marking will eventually be executed or excluded. For finite runs this is equivalent to requiring that it ends in a state with no included pending events. Recall that we write “ $_$ ” for “don’t care”.
Definition 41.
A finite or infinite run $σ = M_{0} \overset{e_{0}}{\to} \dots M_{k} \dots$ is accepting iff it is non-Zeno and $\forall i ⩾ 0 . e \in E . M_{i} (e) = (_, ⊤, d) ⟹ \exists j ⩾ i . (M_{j} (e) = (_, ⊥, d) or e_{j} = e$ , that is, every included required event in an intermediate marking will eventually be executed or excluded. For a finite run $σ = M_{0} \overset{e_{0}}{\to} \dots M_{k}$ it follows that it is accepting iff $\forall e \in E . M_{k} (e) = (_, ⊤, d) ⟹ d = ⊥$ , that is, no included event in the terminal marking is a required response event.

A trace of a process $[M] T$ is a possibly infinite word $s = {(s_{i})}_{i \in I}$ such that $[M] T$ has a possibly empty finite or infinite accepting run $M_{0} \overset{e_{0}}{\to} \dots M_{k} \dots$ with $s_{i} = ℓ (e_{i})$ . Note that the set of traces is not necessarily prefix closed. The timed language $P$ of a process P is the set of traces of P. The finite words contained in the prefix closure of the timed language defines a security policy according to Definition 2.

Note the distinction between events and labels in the definition of a trace. While DCR graphs derive some of their expressive power from this distinction [16], in most practical modelling scenarios labels and events are one-to-one. When we develop theory for enforcing DCR policies in the next section, we will work at the level of events. Policy specifications that do require the distinction between events and label will require additional work to apply the present theory.
7. Enforcing DCR policies

We now consider what is necessary for a DCR policy to be proactively enforceable. Namely, when does an enforcement mechanism exist for a policy? The key insight is that DCR processes have a semantics based on finite labelled transition systems, which in turn can be viewed as finite automata. This means that provided we can construct resolvers for those transition systems, we can directly apply the theory of Section 5 to DCR graphs to produce practically usable enforcement mechanisms.

First, we define how the LTS of a DCR process gives rise to a policy automaton. Recall from Definition 39 that a timed DCR graph $[M] T$ defines a timed LTS, $lts ([M] T) = (M, E, \to, M, ℓ^{'}, Σ)$ , where the states $M$ are the markings reachable from $[M] T$ , and the transitions are $M \overset{e}{\to} M^{'}$ where $e \in E \cup {tick}$ and $M, M^{'} \in M$ .

Definition 42.
Let $lts ([M] T) = (M, E, \to, M, ℓ^{'}, Σ)$ be the timed LTS for the DCR process $[M] T$ . Then the policy automaton for $[M] T$ is the policy automaton $\begin{matrix} (7) & (E \cup {tick}, M, \to, M) . \end{matrix}$

Note that the policy automaton ignores the labelling of the DCR process. This is meaningful in the common case where labels and events are 1–1; we leave the (less helpful) extension to non-trivial label mappings for future work.

We will be interested specifically in the case where all events of the target system are controllable, that is, the enforcement mechanism can always deny an action. In this case, all we need of a policy will be that we can always cause our way to meeting a deadline.
Definition 43 (DCR time-resolvability).

Let $P = [M] T$ be a DCR process and $S \subseteq dom (M)$ a subset of events. We say that P is S-time resolvable iff for any marking $M^{'}$ reachable from M with $deadline (M^{'}) = 0$ , there exists a sequence $e_{1} \cdot \dots \cdot e_{n}$ of events with each $e_{i} \in S$ such that (1) the following is a transition sequence: $\begin{matrix} M^{'} \overset{e_{1}}{\to} M_{1}^{'} \overset{e_{2}}{\to} \dots \overset{e_{n}}{\to} M_{n}^{'} \end{matrix}$ and (2) $deadline (M_{n}^{'}) > 0$ . Assume a particular choice $e_{1} \cdot e_{2} \cdot \dots \cdot e_{n}$ of such a sequence if one exists, and define $resolve ([M^{'}] T)$ to be the (partial) function that exhibits this choice and yields the corresponding sequence of labels $ℓ (e_{1}) \cdot ℓ (e_{2}) \cdot \dots \cdot ℓ (e_{n})$ .

That is, in any reachable state with one or more deadlines about to be missed, one may execute some sequence of the events in the set S to avoid missing those deadlines.

Theorem 44.
Let $T = (S, Σ, Γ, Δ)$ be a target system, let P be a Δ-time resolvable DCR policy with the resolver function $resolve (-)$ , and assume that $Γ = Σ ∖ {tick}$ and $dom (P) \subseteq Σ ∖ {tick}$ . Let A be the policy automaton for P (Definition 42 ). Then A is resolvable (Definition 28 ) at $(Δ, Σ ∖ {tick}, resolve)$ , and the corresponding induced enforcement mechanism (Definition 29 ) is sound and transparent for A.
Proof.
It suffices to show that A is resolvable at $(Δ, Σ ∖ {tick}, resolve)$ ; the result then follows from Theorem 32. To show that A is resolvable, we must define a resolve function $f : M \times Σ \to Σ^{⋆}$ . Take the definition: $\begin{matrix} f (M, e) = \{\begin{array}{ll} resolve ([M] T) & when e = tick and deadline (M) > 0 \\ ⊥ & otherwise . \end{array} \end{matrix}$ Note that $f (M, e)$ is defined iff $e = tick$ , and in this case clearly $f (M, tick) \cdot tick$ is the sequence of labels of a valid run starting from M; so f is indeed a resolver function (Definition 27). We must show that with this resolver function f, the transition semantics of $[M] T$ is in fact resolvable for the given target system (Definition 28). That is, we must show that for all states M and all events $e \in Σ \cup {tick}$ , one of the following is true:
$M \overset{e}{\to} M^{'}$ for some $M^{'}$ ,

$e \in Γ \cup {tick}$ and $f (M, e)$ is defined, or

$e \in Γ$ .
If (1) is the case, we are done, so suppose not. By construction, $f (M, e)$ is defined iff $e \in tick$ , in which case (2), so again suppose not. Then $e \neq tick$ and by assumption $e \in Γ$ , hence (3). □

Hence, any DCR process for which we can find a way to avoid missing deadlines can be used as the definition of a security policy, and we can derive a sound and transparent enforcement mechanism for that policy. The question then becomes: When can we be sure that a given DCR process can always reach a point where it meets its deadlines?
7.1. Time-locked DCR processes

First, let us see an example of a DCR process that cannot meet its deadlines, a so-called time-locked DCR process.

Example 45.
Consider a hospital data retention rule as in Example 35, stating that a patient record must be archived within 14 days and the patient record must not be unarchived before 8 years after it has been archived.

Suppose now we were to add the constraints $\begin{matrix} early ∙ \overset{1 y}{\to} unarchive | archive \to % early, \end{matrix}$ which model that the patient can request that his records are unarchived early, no later than a year after the request. The entire model is then $\begin{aligned} unarchive ∙ \overset{8 y}{\leftarrow} archive \\ release ∙ \overset{14 d}{\to} archive \\ early ∙ \overset{1 y}{\to} unarchive \\ archive \to % early . \end{aligned}$ However, the added constraints may impose the requirement that unarchive happens after at most a year, contradicting the other requirement that unarchive happens only after at least eight years after archival.

Let us see a concrete example, where we start in the initial policy state, and follow how the markings in the policy evolve during an execution of policy events. In the table below, each row represents a state of the graph. The first row is the initial state, the second row is the state after the execution of the event $release$ , the third row is the state after the execution of the event $early$ , the fourth row is the state after the execution of the event $archive$ , and the last row is the state after one year has passed.

In the last state, the event $unarchive$ must happen now, but it cannot due to the required delay of 8 years since $archive$ . The deadline could be extended by re-executing $early$ , but $early$ is excluded. This process is not deadlocked: $release$ can still happen. It is, however, time-locked: it has reached a marking from which time cannot possibly advance.
Definition 46 ([28]).

A process $[M] T$ is time-locked iff no marking $M^{'}$ reachable from M has $T ⊢ M^{'} \overset{tick}{\to} M^{″}$ , for some marking $M^{″}$ .

We conclude that a DCR policy is not necessarily enforceable, even if all events are controllable and causable: If there is a time-lock in a policy, then there are target systems for which no sound and transparent enforcement mechanism exists, since one cannot prevent time from advancing.

Theorem 47.
Let $P$ be the language of a DCR process P that has a time-lock. Assume that $P$ is non-empty and take as the target system $(prefixes (P), dom (P) \cup {tick}, dom (P), dom (P))$ . Then no transparent enforcement mechanism m is sound for $P$ .

This theorem begets the question whether we can decide if a DCR process is time-lock free. As it happens, time-lock–freedom is decidable, but NP-hard. We sketch the development here; see the Appendix for details.

To see that time-lock–freedom is decidable, we note that the LTS of a DCR process is extended bisimilar [25] to a finite one.
Proposition 48.
It is decidable whether a DCR process P is time-lock free.

By reduction from boolean satisfiability, we then find that deciding time-lock–freedom is NP-hard. Time-lock–freedom is intimately tied to the question of reachability event executions, since we can resolve a potential time-lock iff we can find a way to execute events that are pending with deadline zero. This observation will be useful in the next section, so we note the NP-hardness of this reachability problem already now. Definition 49.
Let $P = [M_{1}] T$ be a DCR process, and let e be an event of P. We say that e is eventually executable in P iff there is a transition sequence $M_{1} \overset{e_{1}}{\to} M_{2} \overset{e_{2}}{\to} \dots \overset{e_{n}}{\to} M_{n + 1} \overset{e}{\to} N$ .
Lemma 50.
There exists an $NLOGSPACE$ -reduction from boolean satisfiability to eventual executability for time-lock–free DCR processes.
Theorem 51.
(a) Deciding eventual executability of any e in any DCR process P is NP-hard and (b) deciding time-lock–freedom for DCR processes is NP-hard.

7.2. Resolving DCR deadlines

We have just seen that the existence of an enforcement mechanism for a DCR policy depends precisely on the policy’s time-lock–freedom. We now give a polynomial-time computable sufficient condition for a DCR policy to be time-lock free, which also supports the effective computation of a sequence of events that averts violating a given deadline. Anticipating an application of Theorem 32, we call such a DCR policy “resolvable.” We will subsequently use this notion to define a sound and transparent enforcement mechanism for resolvable DCR policies.

Lemma 52.
A DCR process P is time-lock–free iff it is S-resolvable for some S.
Example 53.
It is easily verified that the policy $T_{0}$ given in Section 5.3 is S-resolvable for $S = {release}$ , or $S = {readmit}$ , or $S = {delete, archive}$ .

Note that a DCR process P can be time-lock–free and yet have no way to accept. For example, consider the process $[e : (⊥, ⊤, 1)] e ∙ \overset{k}{\leftarrow} e$ , where an event e that has not happened is pending (with a deadline of 1), and has itself as condition (with any delay k). This means that e must happen in the future, but also that it can happen only if it happened in the past; however it did not happen the past. It follows that resolvability does not entail that any trace of P can be extended to an accepting one.

From Proposition 48 and Theorem 51, we find immediately a bound on the complexity of determining resolvability:
Proposition 54.
Let P be a DCR process and let $S \subseteq dom (M)$ . It is decidable, but NP-hard, whether a P is S-resolvable.

Given NP-hardness, we require a tractable approximation to resolvability in practice. We begin by considering which events may reach deadlines. We call these busy events.
Definition 55.
An event e is busy in $[M] T$ iff there exists a reachable marking $M^{'}$ with $e : (i, ⊤, k) \in M^{'}$ for some $k \neq ⊥$ and some i.

Note that, as defined, busy events may have the indefinite deadline ω. We can identify busy events in time polynomial in the size of the DCR process:
Lemma 56.
An event e is busy in $[M] T$ only if for some $k \neq ⊥$ either $e : (i, ⊤, k) \in M$ for some i or $f ∙ \overset{k}{\to} e \in T$ for some f.

The only way to violate an obligation is to neither execute nor exclude a busy event when its deadline arrives. Clearly, either (1) the busy event must be under the enforcement mechanism’s control or (2) an alternative event that excludes the busy event must be under the enforcement mechanism’s control. In the following, we will focus just on the first option. To this end, we define dependable events.
Definition 57.
An event e is dependable in P iff in any $P^{'}$ reachable from P, the event e is either excluded or enabled.

The following proposition follows immediately.
Proposition 58.
Let P be a DCR process, let B be the set of busy events of P, and suppose every event in B is dependable. Then P is B-resolvable.

This proposition provides an approximation for resolvability that can be computed in time polynomial in P, since we can approximate the busy events using Lemma 56 and dependable events with those that have no conditions or milestones. In practice, however, it is unlikely that every busy event is dependable. For example, in our policy from Section 5.3, $delete$ is busy, but not dependable: it has a milestone from $archive$ and so may be included but not enabled. We will need to consider the dependencies of busy events.
Definition 59.
Let $P = [M] T$ , and let e be an event of P. The inhibitors of e is the set $\begin{matrix} I (e) = {f | \exists k . e ∙ \overset{k}{\leftarrow} f \lor e ◇ \leftarrow f} . \end{matrix}$ Let the inhibition graph $I (P)$ of P be the directed graph that has nodes $dom (P)$ (P’s events) and an edge from f to e iff $f \in I (e)$ . For a subset of events X, define the inhibition subgraph for X as the subgraph of $I (P)$ comprising every event f with a path to some $e \in X$ in $I (P)$ and every edge on those paths. We denote this graph ${\hat{I}}_{P} (X)$ and its set of nodes $I_{P} (X)$ , dropping the subscript P and writing simply $I (X)$ when P is clear from the context.

The inhibitors of an event e are (the transitive closure of) those events that may cause e to be not executable because they are milestones or conditions for e.
Definition 60.
Let X be a set of events of a DCR process $[M] T$ . We say that X is dependable iff the following three conditions hold.
The inhibition graph $\hat{I} (X)$ is acyclic.

For any two nodes e, f in $\hat{I} (X)$ , if there is a relation $e ∙ \overset{k}{\to} f$ for some k or a relation $e \to + f$ , then there is a path from e to f.

For any two nodes e, f in $\hat{I} (X)$ , if there is a relation $f ∙ \overset{k}{\leftarrow} e$ for some k, then $k = 0$ .

Intuitively, a set of events is dependable if, when we build the graph of those events’ dependencies (milestones and conditions), the dependencies form a directed acyclic graph (1), and we can eventually execute any event in the set by simply executing the events in that acyclic graph in a topological order, i.e., “bottom-up”.

Care must be taken because of the interplay between responses and milestones. We must avoid the situation where resolving a dependency by executing it re-blocks a previously resolved dependency by either reinstating a milestone or a condition (2). Similarly, we must ensure that no event in the set depends any other event in the set with a delay (3).
Theorem 61 (Approximation of Resolvability).

Let P have busy events B. If B is dependable, then P is $I (B)$ -resolvable. Moreover, there exists a polynomial time algorithm computing $resolve$ (Definition 43 ) for every $P^{'}$ reachable from P.

The actual algorithm is simply this: Given a subset $X \subseteq B$ , $resolve (B)$ is a topological sort of $\hat{I} (X)$ .

Example 62.
We return to our data retention example of Example 35. Inspecting the relations, we see that the inhibition graph has only the two edges: $\begin{array}{r} archive \to unarchive archive \to delete . \end{array}$ The busy events of $P_{0}$ are over-approximated by Lemma 56 to $B = {delete, archive}$ . The inhibition subgraph and inhibition closure of B are then simply ${\hat{I}}_{P_{0}} (B) = archive \to delete$ and $I_{P_{0}} (B) = {archive, delete}$ . It is straightforward to verify that $I_{P_{0}} (B)$ is dependable. By Theorem 61, it is thus decidable in polynomial time that $P_{0}$ is indeed ${archive, delete}$ -resolvable. Summing up, if we have the ability to execute $archive$ and $delete$ , then we can guarantee compliance for obligations.

7.3. Practical enforcement of DCR policies

It is instructive to see what an implementation of the enforcement mechanism one derives from a DCR process using Theorem 44 looks like in practice. Taking apart the various definitions involved, we see that this enforcement mechanism allows the target system to execute as long as it stays within the policy. If the target system deviates by attempting an action that is not allowed (“not enabled” in DCR parlance), it is simply denied. If time is about to progress ( $tick$ ) and the policy has unmet deadlines, the enforcement mechanism uses the $resolve$ function to find a sequence of causable actions to execute to get to a point where no deadline is about to expire.

This construction can be automated: All we need is a mechanical way to derive from a given DCR process a corresponding $resolve$ function. We saw that this is generally decidable; however, and more usefully, Theorem 61 gives a direct polynomial approximation in terms of “busy” events.

Figure 8 gives the F# code implementing this enforcement mechanism for illustration purposes, where enforcement happens at the points indicated with (i), (ii), and (iii) in comments.

Fig. 8.

F# implementation of a DCR policy enforcement mechanism.

At point (i), the enforcement mechanism is presented with a target system action which is enabled in the DCR process, that is, admitted by the policy. This action is simply granted.

At point (ii), the enforcement mechanism is presented with a (non- $tick$ ) action that is not enabled, hence not permitted by the policy. This action is simply denied.

At point (iii), the enforcement mechanism is arriving at a deadline, and uses the $resolve (-)$ function to meet those deadlines. Note that in contrast to Definition 43, the mechanism does not update its enforcement state; instead, it causes the target system to follow the $resolve (-)$ output (see comments after Theorem 61 on how to implement $resolve$ ). It will later observe those actions as they happen, at which point it will advance its state at point (i). This implementation is formally justified by Lemma 31, which says that the end-state of replacement is always the same as if the target system had simply followed the replacement from the beginning.

Our prototype uses the policy $P$ also as the target system; this is well-suited for experimentation and simulation in the DCR Workbench. To turn the prototype into an actual enforcement mechanism, it suffices to update the driver function producing the Observation inputs and executing the Reaction outputs of Fig. 8 to one that interacts, say, via REST, with an actual system, as dictated by the system model of Section 2.

8. Related work

In this section, we compare our approach with related policy specification languages for handling obligations and with alternative enforcement mechanisms.

8.1. Specification

The idea of adding obligations to policies was first proposed by Minsky and Lockman [40]. They augmented permissions with tasks to be executed within a stated deadline after an access request is granted. This deadline corresponds, for example, to the passage of time or is triggered by other events. Park and Sandhu examined obligations in the context of usage control [44] and Bettini et al. [7] systematically considered the combination of provisions and obligations within a datalog formalism. In both cases, the emphasis is on policy specification (and, in the case of [7], also analysis), rather than applications to enforcement and monitoring.

Obligations have also been used in languages such as PONDER [10] and XACML [42]. Obligations there are triggered by events: an event’s occurrence directly results in actions to discharge the obligation. This is in contrast to our work where obligations are associated with events that become pending but need not be immediately discharged.

Temporal logics are, of course, well suited for specifying properties based on the past (provisions) and future (obligations). For example, linear-time temporal logics (LTL) have been used in [4,23,30,53] to formalize regulations with obligations and usage-control policies. LTL formulas are closely related to DCR processes: Core (untimed) DCR processes are equivalent in their expressivity to ω-regular languages [15], whereas (propositional) LTL is equivalent to a subset of ω-regular languages, namely the star-free languages [51]. DCR processes also have the advantage that their operational semantics does not depend on the possibly exponential translation to (e.g. Büchi) automata, which is most often employed for LTL; see, for example, the use of LTL and Büchi automata to formalize (untimed) obligations in [18].

Notations for Business Process Modelling share many of the aims and qualities of LTL variants based on Büchi automata, and high-level system descriptions have been formalized using BPMN notation for the purpose of policy monitoring, such as [1]. Researchers in this field have also explored using process models as policy specifications for enforcement. For example, [22] presents a model-checking framework for Petri Nets, where nets capture security policies for physical access control. We explore enforcement further in the next section.

8.2. Enforcement

Obligations are fundamentally more difficult to enforce than provisions. For provisions, policy monitoring and enforcement are equivalent. Any enforceable policy can be monitored as the enforcement mechanism’s denial of an action signifies a policy violation when that action takes place. Conversely, a monitor can serve as a policy decision point for an enforcement mechanism. When policies contain obligations, there are monitorable policies that cannot be enforced, in particular when one distinguishes, as we have done (see also [33]), between actions that can be controlled by the enforcement mechanism versus those that can only be observed [2].

Our solution is for the (standard) setting where one interacts with the target system as a black box, which one can neither examine nor modify. Even with these restrictions, enforceability is a rich concept that depends on the underlying mechanism used [20,24], for example, whether the mechanism can only suppress actions, like security automata [48], or can initiate or change actions as with edit automata [35,36] or mandatory results automata (MRA) [37].

As with our approach, edit automata and MRA share the ability to proactively change behavior to enforce policies. They differ though in that neither formalism handles real-time constraints, which is an essential aspect of obligations. Their system models are quite different too. Our system model essentially extends that of security automata with additional target-system interfaces of controllable and causable actions. The MRA system model interposes the enforcement mechanism between the target system and an execution platform. For edit automata, no distinction is made between observable and controllable events and hence it remains open what an edit automaton can actually control on the target system.

Enforcement of timed obligations has also been studied in [45]. The enforcement mechanism they propose operates by taking as input a sequence of actions σ produced by the target systems and transforming it into an output sequence $σ^{'}$ that is sound with respect to a given temporal property ϕ modelled by a timed automata. There is no interaction per se with the target system. Rather the monitor simply buffers events it receives from the target system and outputs them possibly with delays so that ϕ is satisfied on the resulting output. In comparison with our work, the enforcement mechanism is rather weak as it can neither cause actions to occur and it must make the strong assumption that delayed actions can actually be delayed (e.g., suppressed and later caused) in the real world.

A number of enforcement mechanisms have been proposed for obligations, like those for PONDER and XACML, which do not involve any sophisticated calculations. They enforce obligations simply by executing the appropriate actions (such as logging information) when the obligation to do so arises. Li et al. [34] provide operational extensions to XACML enforcement such as support for pre-obligations and on-going obligations, as introduced in the UCON model [44] – see also Elrakaiby et al. [19] who study enforcement of UCON-style obligations in the context of active databases.

In the Business Process Modelling space, enforcement of process model compliance is generally envisioned as an integral part of applications: users of workflow systems are only allowed to instruct the system to act within the confines of the underlying process model. However, work on separate enforcement mechanism in this space does exist, e.g., [32], where the authors propose an enforcement mechanism for a Petri-net based process specifications.

Finally, there is related work in other communities. For example, in supervisory-control theory for discrete event systems [46], a supervisor process (in our work, enforcement mechanism) attempts to control the behavior of a generator process (in our work, the target system) over its controllable events, which corresponds to our mechanism without the ability to force actions. Subsequent extensions of supervisory-control theory to timed discrete event systems [8,50] include delays and deadlines of each event and a designated subset of so-called forcible events. The supervisor process can now disable the tick (time) actions in case a forcible event is enabled. But the target system may choose to perform a non-forcible event; indeed the supervisor cannot enforce that a forcible event happens as in our approach. Also closely related is the research of Renard et al. [47] who present an automata-based framework for enforcing regular timed properties with uncontrollable events. Their enforcement mechanisms work by buffering and delaying input events so that the output satisfies a specified policy. Again, in contrast, our mechanisms do not buffer and delay, but actively schedule controllable events to prevent obligations’ violations.

9. Conclusions and future work

Obligations are a central notion found in a wide range of security policies such as those for usage control, data protection and privacy, and digital rights management. We have investigated their specification and enforcement in a black-box setting where the enforcement mechanism proactively computes and schedules those events needed to prevent policy violations. As not all policies in this setting are enforceable, we have also established complexity results for enforceability for both policies specified by automata and by DCR processes.

Our work shows how to avoid the violation of obligations by proactively taking actions. We have assumed that the sequence of actions caused proactively can always be executed within a single time-step. If time is measured in hours or days this is usually reasonable. However, for finer time granularities or if resolving an obligation requires delays, one would need to support $tick$ actions during enforcement.

Our approach in this paper is not limited to obligations: one can reasonably consider proactively avoiding the violations of provisions too. For example, suppose we have the provision “action a can happen only if b previously happened”, and suppose the string w contains no occurrences of b. The present approach would suppress a, i.e., $m (w \cdot a) = m (w)$ . However, we might instead cause the action b to happen before allowing a: $m (w \cdot a) = m (w) \cdot b \cdot a$ .

Finally, with respect to the usefulness of proactive enforcement in practice, the proof of the pudding is in the eating. We are presently engaged in a large-scale case study of policy enforcement with a major European railway service. While it seems that our policy language is well-suited for capturing temporal constraints between actions, the formalism presented here does not handle actions depending on data. An extension to handle data is currently underway.

Footnotes

Proofs

Here we provide the remaining proofs for all lemmas and theorems in the paper. Proof of Theorem 47.

Suppose m is sound and transparent. By the definition of a time-lock, there exists a $w \in prefixes (P)$ such that w is a shortest sequence exhibiting a time-lock in $lts (P)$ . Because m is transparent, $w \in D_{m}$ and $m (w) = w$ . Because w exhibits a time-lock, w is not accepting and so $w \notin P$ . Let $v \in dom {(P)}^{*}$ . By the definition of a time-lock, $w \cdot v$ is also not accepting. But then m is not sound, which is a contradiction. □

Proof of Proposition 48.

Immediate from Proposition 66. □

Proof of Lemma 50.

Let B be a boolean satisfiability problem over atoms, conjunction, and negation. That is, B is a string in the language $\begin{matrix} S : : = x | S \land S | \neg S, \end{matrix}$ where x is an atom. Construct a DCR process $[[B]]$ that has, for each non-leaf node n of the abstract syntax tree of B, events $n^{t}$ , $n^{f}$ and $n^{b 1}$ , $n^{b 2}$ , $n^{b 3}$ , and for each atom a the nodes $a^{t}$ , $a^{f}$ and $a^{b 1}$ , $a^{b 2}$ . For each non-leaf node n, add relations as follows.

For each atom a, add the relations $a^{b 1} ∙ \overset{}{\leftarrow} a^{b 1}$ , $a^{b 2} ∙ \overset{}{\leftarrow} a^{b 2}$ , $a^{t} ∙ \overset{}{\leftarrow} a^{b 1}$ , $a^{f} ∙ \overset{}{\leftarrow} a^{b 2}$ , $a^{t} \to + a^{b 2}$ , and $a^{f} \to + a^{b 1}$ .

For each non-leaf node n, add the relations $n^{b 1} ∙ \overset{}{\leftarrow} n^{b 1}$ , $n^{b 2} ∙ \overset{}{\leftarrow} n^{b 2}$ , and $n^{b 3} ∙ \overset{}{\leftarrow} n^{b 3}$ .

For each non-leaf node $n = u \land v$ add the relations $n^{t} ∙ \overset{}{\leftarrow} n^{b 1}$ , $n^{t} ∙ \overset{}{\leftarrow} n^{b 2}$ , $n^{f} ∙ \overset{}{\leftarrow} n^{b 3}$ , $u^{t} \to % n^{b 1}$ , $v^{t} \to % n^{b 2}$ , $u^{f} \to % n^{b 3}$ , and $v^{f} \to % n^{b 3}$ .

For each non-leaf node $n = \neg u$ add the relations $n^{t} ∙ \overset{}{\leftarrow} u^{f}$ and $n^{f} ∙ \overset{}{\leftarrow} u^{t}$ .

Define a marking

M_{0}

where every event is

(⊥, ⊤, ⊥)

, except

a^{b 1}

and

a^{b 2}

, which must be

(⊥, ⊥, ⊥)

. Consider a run of

[[B]]

executing a maximal number of distinct events from

[[B]]

. Note that for each atom a, either

a^{t}

a^{f}

has been executed, but not both. Define from this an assignment of ⊤ or ⊥ to a. By induction, each non-leaf node n has

n^{t}

executed iff this assignment evaluates n true and

n^{f}

executed iff it evaluates n false. But then for the root node r of B,

r^{t}

is executed in some run iff B is satisfiable and

r^{f}

is executed in some run iff it is not. Hence

r^{t}

is eventually executable in

[[B]]

iff B is satisfiable. The DCR process

[[B]]

has

O (| B |)

nodes and relations, and so this reduction is in

NLOGSPACE

. By inspection of the reduction, we see that

[[B]]

contains no responses or initially pending events. Hence it is trivially time-lock–free. □

Proof of Theorem 51.

(a) is immediate from Lemma 50. For (b), let B be a boolean satisfiability problem, suppose $([[B]], e)$ is the corresponding eventual execution problem, and suppose $[[B]] = [M] T$ . Choose $f \notin dom (M)$ . Then $[f : (⊥, ⊤, 0), M] T | f ∙ \overset{0}{\leftarrow} e$ is time-lock free iff f is eventually executable iff B has a satisfying assignment. □

Proof of Lemma 52.

Suppose P is not S-resolvable for any S. By definition, there then exists a state from which time cannot advance after any finite sequence of events, and so P has a time-lock. Suppose instead P is S-resolvable for some S, and suppose for a contradiction that $P^{'}$ is reachable from P and is time-locked. But then $resolve (P^{'})$ is defined and leads to a state in which time has advanced, which is a contradiction. □

Proof of Lemma 56.

Immediate from the definition of busy events. □

Lemma 63.

If X is dependable for $[M] T$ , then so is any $Y \subseteq X$ .

Proof.

Immediate from the definition. □

Proof of Theorem 61.

Suppose $M^{'}$ is reachable from M, and suppose X is the maximal set of events satisfying $x : (i_{x}, 1, 0) \in M^{'}$ for $x \in X$ and some $i_{x}$ s. We must prove that there is some finite set of events ${e_{1}, \dots, e_{m}} \subseteq I (X)$ such that $\begin{matrix} (8) & M^{'} \overset{e_{1}}{\to} M_{1}^{'} \overset{e_{2}}{\to} \dots \overset{e_{m}}{\to} M_{m}^{'} \end{matrix}$ is an event transition sequence and $deadline (M_{m}^{'}) > 0$ . Clearly each $x \in X$ is busy, $X \subseteq B$ , and X is dependable by Lemma 63. Because X is dependable, $\hat{I} (X)$ is acyclic. Let $e_{1}, \dots, e_{n}$ be a topological sorting of $\hat{I} (X)$ . We prove by induction on n that:

a subsequence of $e_{1}, \dots, e_{n}$ is a transition sequence from $M^{'}$ ,

at each $M_{i}^{'}$ , $e_{i}$ is either enabled or excluded, and

at each $M_{j}^{'}$ with $j > i$ , $e_{i}$ is excluded if it was at $M_{i}^{'}$ , pending only if it is excluded, and executed otherwise.

For

k = 1

, by the definition of

\hat{I} (X)

e_{1}

has no conditions or milestones and so is either enabled or excluded (2). If it is enabled, we keep and execute it, and otherwise we forget about it (1). (3) is vacuously true. For

k > 1

we know that all of the conditions and milestones of

e_{k}

are among

e_{1}, \dots, e_{k - 1}

, and by the induction hypothesis (2) and (3) each of those are either executed or excluded. By Definition 60 of dependability, item 3, if

e_{k}

has a condition to an earlier

e_{j}

, it is with time constraint 0. Thus

e_{k}

is enabled iff it is included. If it is excluded we have (1,2). If it is included and so enabled, we execute it to establish (1,2). By Definition 60 of dependability, item 2, executing

e_{k}

does not make any of

e_{1}, \dots, e_{k - 1}

pending or included, establishing (3).

Clearly, each $x \in X$ are among $e_{1}, \dots, e_{n}$ , and by construction, each x is either excluded or executed in $M_{n}^{'}$ . By the definition of dependability, if follows that $deadline (M_{n}^{'}) > 0$ .

This proof also provides an algorithm for computing $resolve$ : Simply compute $\hat{I} (X)$ from its definition – clearly in polynomial time – and choose any topological sorting of the resulting graph. □

References

Asim,

Yautsiukhin,

A.D.

Brucker,

Baker,

Shi and

Lempereur, Security policy monitoring of BPMN-based service compositions, Journal of Software: Evolution and Process 30(9) (2018), e1944, JSME-17-0099.R2.

Basin,

Jugé,

Klaedtke and

Zălinescu, Enforceable security policies revisited, ACM Transactions on Information and System Security 16(1) (2013), 3. doi:10.1145/2487222.2487225.

Basin,

Klaedtke and

Müller, Monitoring security policies with metric first-order temporal logic, in: Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, ACM Press, New York, NY, USA, 2010, pp. 23–33. doi:10.1145/1809842.1809849.

Basin,

Klaedtke,

Müller and

Zălinescu, Monitoring metric first-order temporal properties, J. ACM 62(2) (2015), 15:1–15:45. doi:10.1145/2699444.

D.A.

Basin,

Debois and

T.T.

Hildebrandt, In the nick of time: Proactive prevention of obligation violations, in: IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27–July 1, 2016, 2016, pp. 120–134.

T.J.M.

Bench-Capon and

F.P.

Coenen, Isomorphism and legal knowledge based systems, Artificial Intelligence and Law 1(1) (1992), 65–86. doi:10.1007/BF00118479.

Bettini,

Jajodia,

X.S.

Wang and

Wijesekera, Provisions and obligations in policy rule management, J. Network and System Mgmt. 11(3) (2003), 351–372. doi:10.1023/A:1025711105609.

Brandin and

Wonham, Supervisory control of timed discrete-event systems, IEEE Transactions on Automatic Control 39 (1994), 329–342. doi:10.1109/9.272327.

CDC, The health insurance portability and accountability act of 1996 (hipaa), Public Law, 1996.

10.

Damianou,

Dulay,

Lupu and

Sloman, in: The Ponder Policy Specification Language, Lecture Notes in Computer Science, Vol. 1995, 2001, pp. 18–39.

11.

Debois, Isabelle .THY theory formalisation of the present paper. Available at: https://www.itu.dk/people/debois/archive/JCS.thy.

12.

Debois and

Hildebrandt, The DCR workbench: Declarative choreographies for collaborative processes, in: Behavioural Types: From Theory to Tools,

Gay and

Ravara, eds, River Publishers Series in Automation, Control and Robotics, River Publishers, 2017, pp. 99–124.

13.

Debois,

T.T.

Hildebrandt and

Slaats, Hierarchical declarative modelling with refinement and sub-processes, in: Business Process Management – 12th International Conference, BPM 2014, Haifa, Israel, September 7–11, 2014. Proceedings, Lect. Notes Comput. Sci., Vol. 8659, Springer, 2014, pp. 18–33. doi:10.1007/978-3-319-10172-9_2.

14.

Debois,

T.T.

Hildebrandt and

Slaats, Concurrency and asynchrony in declarative workflows, in: Business Process Management – 13th International Conference, BPM 2015, Innsbruck, Austria, August 31–September 3, 2015, Proceedings, Lect. Notes Comput. Sci., Vol. 9253, Springer, 2015, pp. 72–89. doi:10.1007/978-3-319-23063-4_5.

15.

Debois,

T.T.

Hildebrandt and

Slaats, Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes, in: FM 2015: Formal Methods – 20th International Symposium, Oslo, Norway, June 24–26, 2015, Proceedings, 2015, pp. 143–160. doi:10.1007/978-3-319-19249-9_10.

16.

Debois,

T.T.

Hildebrandt and

Slaats, Replication, refinement & reachability: Complexity in dynamic condition-response graphs, Acta Informatica 55(6) (2018), 489–520. doi:10.1007/s00236-017-0303-8.

17.

Debois,

T.T.

Hildebrandt,

Slaats and

Marquard, A case for declarative process modelling: Agile development of a grant application system, in: EDOC Workshops’14, IEEE Computer Society, 2014, pp. 126–133.

18.

D.J.

Dougherty,

Fisler and

Krishnamurthi, Obligations and their interaction with programs, in: 12th European Symposium on Research in Computer Security (ESORICS),

Biskup and

Lopez, eds, Lecture Notes in Computer Science, Vol. 4734, Springer, 2007, pp. 375–389.

19.

Elrakaiby,

Cuppens and

Cuppens-Boulahia, Formal enforcement and management of obligation policies, Data & Knowledge Engineering 71(1) (2012), 127–147. doi:10.1016/j.datak.2011.09.001.

20.

Falcone,

J.-C.

Fernandez and

Mounier, What can you verify and enforce at runtime?, International Journal on Software Tools for Technology Transfer 14(3) (2012), 349–382. doi:10.1007/s10009-011-0196-8.

21.

Falcone and

Pinisetty, On the runtime enforcement of timed properties, in: Runtime Verification,

Finkbeiner and

Mariani, eds, Springer International Publishing, Cham, 2019, pp. 48–69. doi:10.1007/978-3-030-32079-9_4.

22.

Finkbeiner,

Gieseking,

Hecking-Harbusch and

E.-R.

Olderog, Model checking branching properties on Petri nets with transits, in: Automated Technology for Verification and Analysis,

D.V.

Hung and

Sokolsky, eds, Springer International Publishing, Cham, 2020, pp. 394–410. doi:10.1007/978-3-030-59152-6_22.

23.

Giblin,

A.Y.

Liu,

Müller,

Pfitzmann and

Zhou, Regulations expressed as logical models (REALM), in: Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems, Frontiers Artificial Intelligence Appl., Vol. 134, IOS Press, Amsterdam, The Netherlands, 2005, pp. 37–48.

24.

K.W.

Hamlen,

Morrisett and

F.B.

Schneider, Computability classes for enforcement mechanisms, ACM Trans. Progr. Lang. Syst. 28(1) (2006), 175–205. doi:10.1145/1111596.1111601.

25.

Hennessy and

Stirling, The power of the future perfect in program logics, Information and Control 67(1) (1985), 23–52. doi:10.1016/S0019-9958(85)80025-5.

26.

T.T.

Hildebrandt,

A.A.

Andaloussi,

L.R.

Christensen,

Debois,

N.P.

Healy,

H.A.

López,

Marquard,

N.L.H.

Møller,

A.C.M.

Petersen,

Slaats and

Weber, Ecoknow: Engineering effective, co-created and compliant adaptive case management systems for knowledge workers, in: Proceedings of the International Conference on Software and System Processes, ICSSP’20, Association for Computing Machinery, New York, NY, USA, 2020, pp. 155–164.

27.

T.T.

Hildebrandt and

R.R.

Mukkamala, Declarative event-based workflow as distributed dynamic condition response graphs, in: 3rd Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software (PLACES), EPTCS, Vol. 69, 2010, pp. 59–73.

28.

T.T.

Hildebrandt,

R.R.

Mukkamala,

Slaats and

Zanitti, Contracts for cross-organizational workflows as timed dynamic condition response graphs, J. Log. Algebr. Program. 82(5–7) (2013), 164–185. doi:10.1016/j.jlap.2013.05.005.

29.

Hilty,

Basin and

Pretschner, On obligations, in: Proc. ESORICS, LNCS, Vol. 3679, Springer, 2005, pp. 98–117.

30.

Hilty,

Pretschner,

Basin,

Schaefer and

Walter, A policy language for distributed usage control, in: Proc. ESORICS, 2007, pp. 531–546.

31.

Hublet,

Basin and

Krstić, Real-time policy enforcement with metric first-order temporal logic, in: Computer Security – ESORICS 2022,

Atluri,

Di Pietro,

C.D.

Jensen and

Meng, eds, Springer, Cham, 2022, pp. 211–232. doi:10.1007/978-3-031-17146-8_11.

32.

Kasinathan and

Cuellar, Workflow-aware security of integrated mobility services, in: Computer Security,

Lopez,

Zhou and

Soriano, eds, Springer International Publishing, Cham, 2018, pp. 3–19. doi:10.1007/978-3-319-98989-1_1.

33.

Katt,

Zhang,

Breu,

Hafner and

J.-P.

Seifert, A general obligation model and continuity: Enhanced policy enforcement engine for usage control, in: Proceedings of the 13th ACM Symposium on Access Control Models and Technologies, SACMAT’08, ACM, New York, NY, USA, 2008, pp. 123–132. doi:10.1145/1377836.1377856.

34.

Li,

Chen and

Bertino, On practical specification and enforcement of obligations, in: Proceedings of the Second ACM Conference on Data and Application Security and Privacy, CODASPY’12, ACM, New York, NY, USA, 2012, pp. 71–82. doi:10.1145/2133601.2133611.

35.

Ligatti,

Bauer and

Walker, Edit automata: Enforcement mechanisms for run-time security policies, Int. J. Inf. Secur. 4(1–2) (2005), 2–16. doi:10.1007/s10207-004-0046-8.

36.

Ligatti,

Bauer and

Walker, Run-time enforcement of nonsafety policies, ACM Trans. Inform. Syst. Secur. 12(3) (2009), 19. doi:10.1145/1455526.1455532.

37.

Ligatti and

Reddy, A theory of runtime enforcement, with results, in: Proceedings of the 15th European Symposium on Research in Computer Security, Lect. Notes Comput. Sci., Vol. 6345, Springer, Heidelberg, Germany, 2010, pp. 87–100.

38.

Margheri,

Masi,

Pugliese and

Tiezzi, A rigorous framework for specification, analysis and enforcement of access control policies, IEEE Transactions on Software Engineering 45(1) (2019), 2–33. doi:10.1109/TSE.2017.2765640.

39.

Mazurkiewicz, Trace theory, in: Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency, Springer-Verlag, New York, NY, USA, 1987, pp. 279–324.

40.

N.H.

Minsky and

A.D.

Lockman, Ensuring integrity by adding obligations to privileges, in: Proceedings of the 8th International Conference on Software Engineering, ICSE’85, IEEE Computer Society Press, Los Alamitos, CA, USA, 1985, pp. 92–102.

41.

R.R.

Mukkamala, A formal model for declarative workflows: Dynamic condition response graphs, PhD thesis, IT University of Copenhagen, 2012.

42.

OASIS, eXtensible Access Control Markup Language (XACML) V. 3.0, OASIS Standard.

43.

Ostroff, Deciding properties of timed transition models, IEEE Transactions on Parallel Distributed Systems 1(2) (1990), 170–183. doi:10.1109/71.80145.

44.

Park and

Sandhu, The UCON ABC usage control model, ACM Transactions on Information and Systems Security 7 (2004), 128–174. doi:10.1145/984334.984339.

45.

Pinisetty,

Falcone,

Jéron,

Marchand,

Rollet and

O.L.

Nguena Timo, Runtime enforcement of timed properties, in: Runtime Verification,

Qadeer and

Tasiran, eds, Springer, Berlin, Heidelberg, 2013, pp. 229–244. doi:10.1007/978-3-642-35632-2_23.

46.

P.J.

Ramadge and

W.M.

Wonham, Supervisory control of a class of discrete event processes, SIAM J. Control Optim. 25(1) (1987), 206–230. doi:10.1137/0325013.

47.

Renard,

Falcone,

Rollet,

Pinisetty,

Jéron and

Marchand, Enforcement of (timed) properties with uncontrollable events, in: Theoretical Aspects of Computing, 12th International Colloquium,

Leucker,

Rueda and

F.D.

Valencia, eds, Vol. 9399, Springer, 2015, pp. 542–560.

48.

F.B.

Schneider, Enforceable security policies, ACM Trans. Inform. Syst. Secur. 3(1) (2000), 30–50. doi:10.1145/353323.353382.

49.

Srba, Timed-arc Petri nets vs. networks of timed automata, in: Applications and Theory of Petri Nets 2005,

Ciardo and

Darondeau, eds, Springer, Berlin, Heidelberg, 2005, pp. 385–402. doi:10.1007/11494744_22.

50.

Thistle, Supervisory control of discrete event systems, Mathematical and Computer Modelling 23(11–12) (1996), 25–53. doi:10.1016/0895-7177(96)00063-5.

51.

Thomas, Automata on infinite objects, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), MIT Press, 1990, pp. 133–192.

52.

Winskel and

Nielsen, Models for concurrency, Technical Report DAIMI PB-463, Computer Science Department, Aarhus University, Denmark, 1993.

53.

Zhang,

Parisi-Presicce,

Sandhu and

Park, Formal model and policy specification of usage control, ACM Trans. Inform. Syst. Secur. 8(4) (2005), 351–387. doi:10.1145/1108906.1108908.

Proactive enforcement of provisions and obligations

Abstract

Keywords

1. Introduction

1 We follow established terminology where possible. For example, controllable and uncontrollable come from supervisory control theory, whereas to deny (an action) comes from the security literature on access control.

2.1. System model

2.3. Target system and policies

Example 5 (Obligations).

3. Enforcement mechanisms

3.1. Formalization

Definition 6 (Enforcement mechanism).

Definition 7 (Enforcement function).

Definition 12 (Soundness).

5.1. Automata defining policies

Definition 27 (Resolver).

2 https://www.nec.com.au/solutions/data-and-applications/workzone-case-and-information-management

Definition 36 (Enabled events).

Definition 37 (Execution).

8.1. Specification

8.2. Enforcement

9. Conclusions and future work

Footnotes

Proofs

References

¹
We follow established terminology where possible. For example, controllable and uncontrollable come from supervisory control theory, whereas to deny (an action) comes from the security literature on access control.

²
https://www.nec.com.au/solutions/data-and-applications/workzone-case-and-information-management