SEPD: An Access Control Model for Resource Sharing in an IoT Environment

Abstract

In an open Internet-of-Things (IoT) environment, the chance encounters of smart devices have made it difficult to articulate access control policies for complete strangers. Based on the metaphor of public sphere, the access control model SEPD is proposed to ease policy administration and facilitate trust inspiration for IoT devices. We articulate a system architecture for SEPD, and offer an in-depth study of its access control policies, known as presence policies. In particular, we characterize when presence policies are resilient against half-truth attacks, devise a policy language based on Temporal Constraint Networks, and empirically profile the efficiency of constructing proofs of compliance for presence policies.

1 Introduction

This work attempts to address two access control challenges in Internet-of-Things (IoT) environments [4, 32, 37, 38]. The first challenge is that of policy administration. As the number of devices proliferates, and as chance encounters between unfamiliar devices become the norm, manual specification of access control policies becomes unscalable. The second challenge is that of trust inspiration, especially between devices who do not know one another previously. We want to provide means for complete strangers to gain the trust of one another without resorting to the use of a global identity management framework.

Take, for example, a smart home owned by John. In John’s living room is a smart TV, a smart stereo system, as well as other gadgets. If John wants to specify access control policies for these fixtures, so that his family members (a relatively small and stable set of users) can access the resources in the smart devices he owns, then standard access control paradigms apply readily [15, 18, 21, 28]. However, imagine John now hosts a party in his living room. Visitors want to make music, videos, and sensor data streams available for access by one another. Worst still, although they know John either directly or through friends, they may not know one another. In fact, no one, not even John, knows everyone in the party. Policy administration and trust inspiration become particularly challenging.

Public Spheres. The challenges in the previous example arise from the fact that John turns his living room into a public sphere. A public sphere has four qualities [22]: (1) It is not “gated,” and is therefore accessible by everyone. (2) It is used for diverse purposes, even at the same time. (3) It promotes the sharing of experiences. (4) Participants are aware of sharing expectations. As an example, we do not limit who can enter a park or a mall (Quality 1). Those who enter know full well that they will meet people, and their appearances and actions will be observable by others (Quality 4). Yet, these interactions are exactly what people look for when they enter that space (Quality 3), although they congregate not for a single purpose (Quality 2). A public sphere is therefore different from a private space, in that it is not intimate (participants do not know one another), it is unprotected (interactions are not centrally mediated), and it is unfamiliar (who or what you interact with may change relatively frequently). The goal of this work is to use the public sphere as a controlling metaphor for regulating the sharing of digital resources during the chance encounters of smart devices. Though a worthy goal in its own right, protecting infrastructure resources is not our main focus.

The SEPD Model. We propose an access control model SEPD, for supporting the sharing of resources in public spheres. SEPD offers four features. (1) Well-defined Spaces serve as arenas for resource sharing. Entering a space is a physical gesture for a user to signal that she consents to make a limited subset of her resources sharable with other visitors of that space. (2) The owner of a space will configure and announce access control policies that regulate resource sharing among visitors of the space. Users now enter the space with an explicitly articulated Expectation of what is to be shared and what kind of person will have access. (3) Access control policies are formulated in terms of users’ history of Presence in the space. The “familiar faces” will earn higher levels of access. (4) The authorization system is structured in the style of a Distributed trust management system [9]. The authorization system does not track the location history of the users. Instead, location verifiers are in place to issue presence certificates to the users. To access a resource currently in the space, the user must construct a proof of compliance using the presence certificates, demonstrating to the resource-bearing device that her history of visitation satisfies the access control policy issued by the space owner. Features (1) and (2) ease policy administration: Users are relieved from formulating and updating access control policies, as such responsibilities are now delegated to the space owner. Features (3) and (4) support the establishment of trust without resorting to a global identity management solution. Historical presence data become a ground for inspiring trust, as people have done in the physical world for millennia.

Contributions. This work (a) proposes a system architecture for SEPD (Sect. 3), (b) characterizes when a presence policy is resilient against half-truth attacks (Sect. 4), (c) devises a policy language for specifying presence policies using Temporal Constraint Networks (Sect. 5), and (d) evaluates the efficiency of constructing a proof of compliance using Mixed Integer Programming (Sect. 6).

Notations. We write $dom (f)$ and $ran (f)$ respectively for the domain and range of a function f. If $S \subseteq dom (f)$, then $f|_{S}$ denotes the restriction of f to the smaller domain S. $K_{A}$ and $K^{-1}_{A}$ denotes respectively the public and private key of principal A.

2 Related Work

Location-based Access Control (LBAC) takes into account the location of the requestor when authorization decisions are made [3, 5, 12, 30]. For example, a nurse is allowed to access the medical record of a patient only if she is in the premise of the hospital [12]. The location of a principal is inferred through sensor readings, and the authorization decision is a function of this location information [10]. In the physical world, physical interactions are possible only because of the physical presence of an actor: e.g., to turn on or off the lights in a room requires someone to use the switch, so the design of the switch itself embodies the access control policy [30]. To be present at a particular location may already be the result of some positive authorization decisions, as access to this location could be protected by conventional methods such as guards, fences or locked doors [12]. Extensions to Role-Based Access Control (RBAC) [5, 11, 27] and to Relationship-Based Access Control (ReBAC) [34] have been proposed to support location awareness. For example, a combination of RBAC and physical access control (keypad locks, smart-cards on doors) was presented in [5], where users would be assigned a spatial-role after interacting with one of the physical components of the system. LBAC policies are envisioned to take into account conditions that are position-based (conditions that involve having the user present at a specified location), movement-based (conditions that involve having the user moving in a specific direction or at a certain speed), or interaction-based (conditions involving relationships between multiple users or entities) [3]. Our work is unique in that SEPD policies take into account of the requester’s history of presence (Sect. 4.1), on top of whether the requester is currently present, thereby giving it a flavour of History-Based Access Control (HBAC) [14, 25, 31].

Attribute-Based Access Control (ABAC) has been advocated to ease policy administration in IoT environments. An example is NIST’s Next Generation Access Control (NGAC), in which automated device registration facilities the introduction of new devices [6]. Users, however, are known principals in the authorization system. Proposed for protecting messages sent to smart vehicles, the dynamic groups of Gupta et al. are induced by attributes, some of which are location related [19]. In both works, users and/or resources are known entities to the authorization system. SEPD, however, supports resource sharing among resource-requesting and resource-bearing devices that neither know one another nor are known to the authorization system. This is achieved by structuring the authorization scheme as a distributed trust management framework [9] (Sect. 3). Policy administration is facilitated by having the space owner specify policies in an intensional policy language (Sects. 4–5).¹

HCAP is a history-based capability system designed to support the enforcement of history-based access control policies in an IoT environment, in order to impose workflow-induced or spatially-induced order of accesses [33]. Authorization in HCAP depends on the history of access, while authorization in SEPD is dependent on the history of presence (Sect. 4.1). The chief security challenge of HCAP is to prevent the replay of security tokens, while the main security challenge of SEPD are half-truth attacks (Sect. 4.2). HCAP policies are specified as Security Automata [31], while SEPD policies are specified via Temporal Constraint Networks (Sect. 5).

3 System Overview

3.1 System Participants and Trust Assumptions

SEPD assumes the existence of a public key infrastructure (PKI). When two parties communicate, they know the public key of the other party. It is assumed that mutual authentication is performed prior to all communications, which occur through secure channels. In SEPD are three types of participants.

(1) Public Space. The first participant is a public space (or simply space), which is a real-world environment with physical boundaries and accessible to users. A space provides an arena for strangers to interact and share experiences. Each space is operationally defined by one or more location verifier (LV). A user agent may prove to an LV that she is present at the space, and the LV will issue a presence certificate attesting to that fact. Further details concerning presence certificates are given in Sect. 3.2.

While a location proof system can be realized using different approaches [16, 29, 36, 39], an implementation of the LV can make use of secure Distance-Bounding (DB), where a prover tries to convince a verifier that they are within a certain physical distance, by solving a challenge within a limited amount of time [7, 8, 13]. Multiple DB protocols have been proposed, including public-key based protocols that do not assume an online connection to a trusted server nor a shared secret between the prover and the verifier [20]. Using a public-key DB protocol would allow the LV to be a self-contained entity, and require little additional computing capabilities to issue the presence certificates. This technology is currently available for consumers, with commercial solutions available from different vendors, such as 3db-Access. A study on different DB protocols, possible attacks, and their security properties is presented in [1].

To simplify discussion, we assume that each space has exactly one LV. We assume that the LV is physically secure, so that other participants (including the space owner) may not tamper with the private key of the LV as well as its software configuration. We assume that the LV is not equipped with general-purpose communication capability for Internet access, but is equipped only with enough communication capability to perform distance bounding. The LV does not track location history of users. The LV can be seen as part of the infrastructure of the environment, like a street light.

(2) Space Owner. Another participant is the owner of the space, whose responsibility is to specify and publicize access control policies that govern how resources are to be shared when users enter into the space. Doing so establishes a publicly aware expectation of sharing for that space (the E in SEPD). The owner defines a number of resource identifiers, such as “radio,” “pictures for meditation,” etc. Each resource identifier names a group of resources that a visitor may want to share when she enters into the space. Resource identifiers are therefore akin to the standard profile items in social media platforms. The space owner also specifies an access control policy for each resource identifier. These access control policies are then published by a policy and authorization server (PAS), who acts as an agent of the space owner. User agents (i.e., devices, see below) obtain the latest policies from the PAS. Section 3.3 gives an overview of such policies.

In our design, presence certificates are never passed to the PAS, and the PAS is not aware of users’ access history. The PAS is not required to track user state: there is no notion of a user having to “log on” prior to access. There is not even a need for the user to “register for an account” with the PAS, just like we do not ask a citizen to register before entering a park. All these contribute to scalability, privacy, and openness.

(3) Users. A third group of participants are users, who bring along user agents, which are devices such as smartphones, wearables, hearables, etc. Each user agent encapsulates resources named by resource identifiers. By entering the space, the users physically gesture that they are willing to share those resources under policies set out by the space owner. The authorization scheme is described in Sect. 3.4. As we shall see, the authorization scheme takes the form of a distributed trust management system, and thus authorization checks are performed by user agents when they receive access requests from one another (rather than conducted centrally in a cloud). Consequently, the space owner’s policies are merely recommendations. A user agent may still choose not to honor those policies, or choose to impose additional authorization checks.

The space owner may install fixture devices in the public space. For example, a smart wall may probe nearby users, and project a sample of their “pictures for meditation” to the wall. A smart jukebox may play a sample of songs streamed by the “radio” resources of nearby users. These devices are just like any other user agents, and thus subject to the same access control as others. Since fixture devices are always present in the space, they would eventually acquire the status of “familiar faces” after installation.

3.2 Establishing a History of Presence

Access control policies in SEPD are formulated in terms of the requestor’s history of presence at the space. This provides a means for complete strangers to build trust. When a user U visits a space S, her user agent A will prove to the LV of S that U is currently present. The LV will in turn issue presence certificates to U to testify for her presence. We write $Presence _{\mathrm {LV}}(U,t _1,t _2)$ to denote the presence certificate issued by the LV (i.e., signed by the private key $K^{-1}_{\mathrm {LV}}$) to assert that user U (more precisely, the public key $K_{ U }$) was present in some time interval $[t _1, t _2]$.

Obviously, U cannot prove her presence in a continuous manner. If U proves her presence at successive time points $t_1$, $t_2$, ..., $t_n$, where $t_{i+1} - t_i \le \delta$ for some small $\delta$, then we accept that U is present continuous during the interval $[t_1, t_n]$. There is still a risk that U lies by exiting S momentarily. The smaller $\delta$ is, the less risk we have to bear. Choosing $\delta$ to be, say, 15 min would result in a manageable risk for a university campus spanning hundreds of acres of land. More specifically, when U first arrives at S at time $t$, she will request the LV to initiate a visitation, and the latter will issue the presence certificate $Presence _{\mathrm {LV}}(U,t,t +\delta )$. Once U has been issued a presence certificate $Presence _{\mathrm {LV}}(U,t _1,t _2)$, she may request to extend a visitation at any time $t$ before the clock reaches $t_2$ (i.e., $t \in [t _1, t _2]$), by (a) sending to LV the existing certificate $Presence _{\mathrm {LV}}(U,t _1,t _2)$, and (b) obtaining from the LV a new presence certificate $Presence _{\mathrm {LV}}(U,t _1,t +\delta )$. When the visitation terminates, U simply does not further extend her visitation. Consequently, the LV does not need to track the state of users.

As a result, user U ends up receiving a series of presence certificates after a single visitation:

$$\begin{aligned} Presence _{\mathrm {LV}}(U,t _1,t _2), Presence _{\mathrm {LV}}(U,t _1,t _3), \ldots Presence _{\mathrm {LV}}(U,t _1,t _n). \end{aligned}$$

(1)

Note that the presence certificates that testify to only parts of a visitation (e.g., $Presence _{\mathrm {LV}}(U,t _1,t _3)$) are not revoked. Here, we have adopted the monotonic interpretation of certificates as advocated by Li and Feigenbaum [24]. All presence certificates are valid; they just do not necessarily tell the whole truth. Adopting a monotonic interpretation of presence certificates allows us to avoid dealing with inefficient revocation schemes involving, for example, Certificate Revocation Lists (CRLs) and Merkle hash trees [23]. Designed for devices that are not computationally well endowed, our scheme reduces both communications and complexity. The downside is that our design leads to the possibility of half-truth attacks, a problem to be addressed in Sects. 4.2–4.3.

3.3 Publishing Presence Policies

The SEPD model shifts the responsibilities of crafting and maintaining access control policies from the individual users to the space owner. Access control policies are authored by the space owner and published by the PAS. In particular, the owner assigns a policy to each resource identifier $r$ she wants to support. These policies are called presence policies, as the requestors are required to demonstrate physical presence in order for access to be granted. The simplest policy is this: “Grant access if the requestor is currently present.” A more demanding policy $\mathcal {P}$ may also require the requestor to have been present in the past, so as to privilege the “known faces”: “Grant access if the requestor is currently present, and had visited this space on at least three different days in the previous week.” Note that the operational meaning of $\mathcal {P}$ is dependent on the current time. For example, at noon on April 29, 2019, the requirement of $\mathcal {P}$ is operationalized into the following presence predicate (): “Access may be granted if the requestor is present in the interval , and had visited this space on at least three different days during the interval .” Presence policies and presence predicates are formally defined in Sect. 4. Each presence predicate $P _t$ is encoded in some machine-readable format $Q$ to facilitate processing by user agents. The design of this machine-readable policy language is the topic of Sect. 5.

If a user is interested in accessing resources in devices currently present in the space, she will request the PAS to issue a policy certificate for the current time $t$. We write $Policy _{\mathrm {PAS}}(r, t, \varDelta , Q)$ to denote the policy certificate issued by the PAS (i.e., signed by the private key $K^{-1}_{\mathrm {PAS}}$) to assert that resource $r$ can be accessed within the time window $[t, t +\varDelta ]$ on the condition that the requestor satisfies the presence predicate specified in $Q$. The user may reuse the same policy certificate repeatedly during the time interval $[t, t +\varDelta ]$.

Note that the presence predicate in the example above () grants access only for a limited time window (12:00–12:30). There are a few reasons for this design: (1) This supports the evolution of policies. (2) Different access requirements can be imposed at a different time of the day (or a different day of the week, etc.). (3) Again, this design is influenced by Li and Feigenbaum [24], so that we do not need to revoke policy certificates.

3.4 Authorizing Access Requests

SEPD authorization is performed in a distributed manner, rather than mediated by a centralized Policy Decision Point (PDP). When the user agent $A_1$ of user $U_1$ requests to access resource $r$ in the user agent $A_2$ of user $U_2$, the following events occur.

• 1. User agent $A_1$ would have already contacted the PAS to obtain a policy certificate $Policy _{ \mathrm {PAS}}( r, t, \varDelta , Q)$. In addition, $A_1$ would have already constructed a proof of compliance $\varPi$, which is a subset of the presence certificates issued by the LV for $U_1$ in the past. The set $\varPi$ provides sufficient evidence that $U_1$ satisfies the conditions specified in $Q$. The construction of $\varPi$ also produces a short explanation m of why $\varPi$ satisfies $Q$.

• 2. $A_1$ now sends to $A_2$ an access request consisting of: (a) the resource identifier $r$, (b) the policy certificate $Policy _{ \mathrm {PAS}}( r, t, \varDelta , Q)$, (c) the proof of compliance $\varPi$, and (d) the explanation m.

• 3. $A_2$ now validates the following before granting access: (i) the current time is within the time interval $[t, t +\varDelta ]$, (ii) the policy certificate is issued by the PAS, and is about the accessibility of resource $r$, (iii) every presence certificate in $\varPi$ is issued by the LV, and is about $U_1$ (more precisely, about $K_{ U_1 }$), (iv) m properly explains how $\varPi$ satisfies $Q$.

As we shall see, the validation of $\varPi$ and m in Step 3 can be conducted efficiently (Sect. 5.3); their construction (Step 1), even though a computationally hard problem (Sect. 5.3), has acceptable performance in practice (Sect. 6).

Again, even if the authorization checks are satisfied, user agent $A_2$ may still choose to refuse the request of $A_1$ or impose additional checks on top of the requirements of SEPD.

4 Presence Policies

4.1 Presence Policies and Proofs of Compliance

Neither the LV nor the PAS track location history. Users are responsible for storing their own presence certificates. When the client requests a device to grant access, it presents to the latter a proof of compliance, which is made up of presence certificates issued by the LV in the past. The resource-bearing device will authorize access only if the proof of compliance satisfies the presence policy announced by the PAS. We make these notions formal in the following.

Definition 1

A time interval $I$ is a bounded and closed interval $[ x , y ] = \{ z \in \mathbb {R} \mid x \le z \le y \}$, where $x, y \in \mathbb {R}$ and $x \le y$. We write $min (I)$ and $max (I)$ for x and y respectively, $len (I)$ for $y - x$, and $\mathsf {Int}$ for the family of all time intervals.

In the following we do not differentiate a presence certificate and the time interval it asserts, unless such a differentiation is necessary.

Definition 2

A proof of compliance $\varPi$ is a finite set of time intervals. We write $\mathsf {PoC}$ for the family of all proofs of compliance.

A presence policy specifies when a client has presented enough evidence to be granted access. Such evidence takes the form of a proof of compliance $\varPi$.

Definition 3

A presence predicate $P: \mathsf {PoC} \rightarrow \mathbb {B}$ maps a proof of compliance to a boolean authorization decision. A presence policy $\mathcal {P}$ is an indexed family of presence predicates, $\{ P _t \}_{t \in \mathbb {R}}$, such that for every time point $t \in \mathbb {R}$, $P _t (\varPi )$ is true only if there exists $I \in \varPi$ such that $t \in I$.

Since the semantics of a presence policy is parameterized by the current time (e.g., “grant access if the requestor is present now as well as one week ago”), the time index $t$ informs the presence predicate $P _t$ of the current time. In addition, the requestor is required to be currently present in order to be granted access. Of course, a presence predicate may impose further presence requirements on top of this minimum requirement.

In a public sphere, users are not necessarily known by one another, nor by the space owner. We, therefore, use past presence as a criterion of trust.

Example 1

We list in the following several ways by which past presence could be employed to inspire trust. In each of the following presence policies, we assume the implicit requirement that the client must be present currently, and list the additional criterion required by that policy.

• 1. Heavy user ($\mathcal {P} _1$). “The total amount of time in which the requestor was present last week exceeds T hours.” We do not care if the requestor visits one time or a hundred times. So long as the total duration of stay is long enough, we consider her a heavy user, and thus deserved to be trusted.

• 2. Long stay ($\mathcal {P} _2$). “The requestor has made at least one continuous stay of over T hours last week.” Unlike the previous example, we want the T hours to constitute a single, continuous visitation. A long stay reflects the requestor’s commitment, which forms the basis of trust in this type of policy.

• 3. Spread ($\mathcal {P} _3$). “The requestor has made at least 3 separate visitations last month, each in a different week.” The requestor is required to distribute her stay over multiple visitations across a wide spread of time. Spread demonstrates another form of commitment.

• 4. Frequency ($\mathcal {P} _4$). “The requestor has made k separate visitations, all within last week, and no two consecutive visitations are apart by more than T hours.” Frequent visits are yet another demonstration of commitment.

• 5. Regularity ($P _5$). “There is a day in the week for which the requestor always makes a visit every week during the last month.” The requestor has formed a habit of visiting.

• 6. Non-monotonicity ($\mathcal {P} _6$). “The requestor only visits in the morning during the last year (i.e., never visits in the afternoon).” Again, this policy is about visitation habits. What is unique about his policy is that it uses negative information (“never”).

All the policies above require the user to demonstrate past “commitments,” while the sorts of commitment required are different for different policies.

4.2 Resiliency Against Half-Truth Attacks

Since neither the PAS nor the LV tracks the location history of the users, a resource-bearing device relies on the proof of compliance presented by the requestor to determine if authorization is granted. The requestor may withhold information (e.g., omitting a certificate) in order to gain access. Consider, for example, policy $\mathcal {P} _6$ (“visits only in the morning”) in Example 1. No set of certificates can give conclusive evidence that the requestor has never visited in the afternoon, for the client may withhold certificates that testify to afternoon visits. Policies that are resilient to the malicious withholding of information by the clients must be monotonic in nature: such policies consume only positive information. While the inability to support presence policies that consume negative information can be seen as a limitation of SEPD, this requirement of monotonicity is commonplace in distributed trust management systems [9].

Recall that a user may present a presence certificate to the LV and request that the latter issues a new presence certificate that testifies to a longer stay. By the end of a visitation, the user ends up collecting the series of presence certificates displayed in (1). Such a feature necessitates a unique requirement for monotonicity. Consider, for example, policy $\mathcal {P} _4$ in Example 1. The policy requires that consecutive stays to be apart for T hours. The client receives certificates that testify to longer and longer stays, but it could choose to present only the shorter ones to give the impression that the stays are very far apart, but in reality, a new visit starts only seconds after a former visit finishes. Such malicious disclosure of only a part of a longer stay is what we call half-truth attacks. Preventing half-truth attacks is a unique challenge of our authorization system.

Not all presence policies are resilient to the withholding of information in general, and the selective presentation of half-truth in particular. We characterize in the following presence policies that are resilient to half-truth attacks.

Definition 4

(1) Given $\varPi \in \mathsf {PoC}$, we write $\cup \varPi$ for the set $\bigcup _{I \in \varPi } I$. (2) An interval $I _2$ is a right extension of interval $I _1$, written $I _1 \subseteq _R I _2$, whenever $I _1 \subseteq I _2$ and $min ( I _1 ) = min ( I _2 )$. (3) Given $\varPi _1, \varPi _2 \in \mathsf {PoC}$, we say that $\varPi _2$ R-subsumes $\varPi _1$, written $\varPi _1 \sqsubseteq _R \varPi _2$, whenever there exists a function $f : \varPi _1 \rightarrow \varPi _2$ such that for every $I \in \varPi _1$, $I \subseteq _R f(I)$.

(It is easy to check that both $\subseteq _R$ and $\sqsubseteq _R$ are partial orderings.) Suppose a proof of compliance $\varPi _1$ contains an interval $I _1$, and a presence predicate $P$ authorizes access for $\varPi _1$ (the reader may find it helpful to think of $P$ as corresponding to $\mathcal {P} _2$ in Example 1). But it turns out that $I _1$ is a half-truth, meaning that the actual stay is captured by another certificate $I _2$, where $I _1 \subseteq _R I _2$. Intuitively, the presence predicate $P$ is resilient to half-truth attacks if $P$ still authorizes access when it is presented with another proof of compliance $\varPi _2$ that is obtained from $\varPi _1$ by replacing $I _1$ with $I _2$. This is a special case of $\varPi _1 \sqsubseteq _R \varPi _2$.

The definition below enumerates four candidate notions that can be used for capturing the idea of resiliency against half-truth attacks. Their relationships are outlined in the following theorem (see Appendix B.1 for a proof).

Definition 5

Suppose $P: \mathsf {PoC} \rightarrow \mathbb {B}$ is a presence predicate. (1) $P$ is semantically monotonic if and only if, for every $\varPi , \varPi ' \in \mathsf {PoC}$, $\cup \varPi \subseteq \cup \varPi '$ implies that $P ( \varPi ) \rightarrow P ( \varPi ' )$. (2) $P$ is syntactically monotonic if and only if, for every $\varPi , \varPi ' \in \mathsf {PoC}$, $\varPi \subseteq \varPi '$ implies that $P ( \varPi ) \rightarrow P ( \varPi ' )$. (3) $P$ is R-reducible if and only if, for every $\varPi \in \mathsf {PoC}$, if there exists distinct intervals $I _1, I _2 \in \varPi$ such that $I _1 \subseteq _R I _2$, then $P ( \varPi ) \rightarrow P ( \varPi \setminus \{ I _1 \} )$. (4) $P$ is R-resilient if and only if, for every $\varPi , \varPi ' \in PoC$, $\varPi \sqsubseteq _R \varPi '$ implies that $P ( \varPi ) \rightarrow P ( \varPi ' )$

A presence policy $\mathcal {P} = \{ P _t \}_{t \in \mathbb {R}}$ is semantically monotonic (resp. syntactically monotonic, R-reducible, R-resilient) if and only if $P _t$ is semantically monotonic (resp. syntactically monotonic, R-reducible, R-resilient) for every $t \in \mathbb {R}$.

Theorem 1

Suppose $P$ is a presence predicate. (1) If $P$ is semantically monotonic, then $P$ is R-resilient. (2) $P$ is R-resilient if and only if $P$ is both syntactically monotonic and R-reducible. The same can be said about presence policies.

Among the four notions in Definition 5, R-resiliency best captures the idea of resiliency against half-truth attacks. Semantic monotonicity is too stringent. It ignores the notion of a visitation. Of all the policies in Example 1, only $\mathcal {P} _1$ is semantically monotonic. Specifically, $\mathcal {P} _2$, which is intuitively resilient to half-truth attacks, is R-resilient but not semantically monotonic. Theorem 1 tells us that R-resiliency can be factorized into two requirements: syntactic monotonicity and R-reducibility. R-resiliency is thus weaker than semantic monotonicity but stronger than syntactic monotonicity. R-reducibility implies that the client needs to store only one presence certificate for each visitation: i.e., the one with the longest duration. Hereafter, we use the terms “resiliency against half-truth attacks” and “R-resiliency” interchangeably.

4.3 A Policy Idiom to Ensure R-Resiliency

Some presence policies are not resilient to half-truth attacks: e.g., $\mathcal {P} _3$, $\mathcal {P} _4$, and $\mathcal {P} _5$ from Example 1. Yet the notions of spread, frequency, and regularity exemplified by these policies are valuable ways to inspire trust. We would like to craft presence policies that on the one hand approximate these notions, and on the other hand guarantee resiliency against half-truth attacks.

A careful analysis of Example 1 would reveal that the notions of spread ($\mathcal {P} _3$), frequency ($\mathcal {P} _4$), and regularity ($\mathcal {P} _5$) are not R-resilient because they are framed in terms of “separate visitations.” Extending an interval to the right could potentially cause it to overlap with other existing intervals, and thus visitations are no longer “separate.” We, therefore, outline below a policy idiom that can be used for crafting an R-resilient policy while allowing notions such as spread, frequency, and regularity to be approximated. The key is to work with “time windows” rather than “separate visitations.”

Definition 6

An admissible-window scheme is a triple $\chi = (\mathsf {wd}, \mathsf {ad}, \mathsf {ag})$, where:

• The windowing function $\mathsf {wd} : \mathbb {R} \rightarrow 2^{\mathsf {Int}}$ divides the timeline into intervals called windows. The argument to the windowing function is the current time. The window set $\mathsf {wd}(t)$ satisfies the following three properties. (1) The set $\mathsf {wd}(t)$ is finite. (2) For every $W \in \mathsf {wd}(t)$, $max (W) \le t$. In other words, given the current time t, the windowing function defines windows over the past timeline. (3) For intervals $W _1, W _2 \in \mathsf {wd}(t)$, exactly one of the following holds: (a) $W _1 \cap W _2 = \emptyset$, (b) $W _1 = W _2$, or (c) $W _1 \cap W _2$ is a singleton set. In other words, the windows returned by $\mathsf {wd}$ do not overlap with one another except perhaps at the borders. Lastly, the windows returned by $\mathsf {wd}$ are not necessarily of the same size, but uniform window size is a typical case.

• The admissibility predicate $\mathsf {ad} : \mathsf {PoC} \rightarrow \mathbb {B}$ is an R-resilient presence predicate. The intention is to use $\mathsf {ad}$ to classify the windows as either admissible or not. More precisely, given a window $W \in \mathsf {Int}$ and a proof of compliance $\varPi \in \mathsf {PoC}$, we define $\varPi /W$ to be the set $\{ I \cap W \mid I \in \varPi , I \cap W \ne \emptyset \}$. A window $W$ is admissible whenever $\mathsf {ad} ( \varPi /W)$ is true.

• The aggregation predicate $\mathsf {ag} : \mathsf {PoC} \rightarrow \mathbb {B}$ is a syntactically monotonic presence predicate. The intention is to use $\mathsf {ag}$ to capture notions such as frequency, spread, and regularity (which are syntactically monotonic but not necessarily R-resilient).

The presence policy $\mathcal {P} _\chi$ is the family of presence predicates $\{ P _t \}_{t \in \mathbb {R}}$ such that:

$$ P _t(\varPi ) = \mathsf {ag}( admissible (\varPi , t)) $$

where $admissible (\varPi , t) = \{ W \in \mathsf {wd}(t) \mid \mathsf {ad}( \varPi /W) \}$.

The next theorem ensures that the policy constructed from an admissible-window scheme is resilient to half-truth attacks (see Appendix B.2 for a proof).

Theorem 2

Suppose $\chi$ is an admissible-window scheme. Then the presence policy $\mathcal {P} _\chi$ is R-resilient.

Example 2

$\mathcal {P} _5$ from Example 1, which is not R-resilient, can be approximated by the R-resistant policy $\mathcal {P} ^\star _5$: “There is a day of the week such that for every week in last month, there is a continuous visitation that intersects with that day of the week for at least T hours.” This approximation is obtained by the admissible-window scheme $\chi = (\mathsf {wd}, \mathsf {ad}, \mathsf {ag})$ defined as follows. The windowing function $\mathsf {wd}(t)$ returns a set of windows, one for each day in the last month (relative to the current time $t$). The admissibility predicate $\mathsf {ad}(\varPi )$ returns true if and only if $\varPi$ contains an interval $I$ such that $len (I) \ge T$. It is easy to check that $\mathsf {ad}$ is R-resilient. The aggregation predicate $\mathsf {ag}(\varPi )$ returns true when there exists a day of the week D and a month M in the timeline, such that all the day-windows in M that correspond to D are members of $\varPi$. It is easy to check that $\mathsf {ag}$ is syntactically monotonic (but not R-resilient). $\mathcal {P} ^\star _5$ is actually the presence policy $\mathcal {P} _\chi$ induced by the admissible-window scheme $\chi = (\mathsf {wd}, \mathsf {ad}, \mathsf {ag})$. According to Theorem 2, $\mathcal {P} ^\star _5$ is R-resilient.

Similarly, $\mathcal {P} _3$ and $\mathcal {P} _4$ can also be approximated by the admissible-window policy idiom. There is no need to pretend that $\mathcal {P} ^\star _5$ is equivalent to $\mathcal {P} _5$. They are not. Nevertheless, the admissible-window policy idiom allows one to translate notions such as frequency, spread, and regularity, which are not resilient to half-truth, to R-resilient policies that approximate their meanings.

5 A Policy Language

The owner of a public space needs a policy language for specifying presence policies. Such a language should (a) offer enough expressiveness to capture a wide range of presence policies, (b) provide efficient means for the authorization server to verify a proof of compliance, and (c) support the authoring of policies that are resilient against half-truth attacks. We have based our design of such a policy language on the temporal constraint network (TCN) [2, 26, 35], and augmented TCN with a number of extensions. Knowledge of TCNs is assumed in the rest of the paper. Readers who are new to TCNs and Allen’s algebra are directed to Appendix A for a brief introduction.

5.1 Presence Predicate Specifiers

Recall that a TCN is a graph structure in which every node is a placeholder for a time interval, and every directed edge prescribes a temporal relation that must hold between the time intervals represented by the two ends of the directed edge (Appendix A). An extended temporal constraint network (ETCN) essentially is a TCN augmented with two additional types of nodes. A floating node can only be instantiated to a time interval with a specific duration. An anchored node can only be instantiated to a pre-selected time interval.

Definition 7

An extended temporal constraint network (ETCN) $\varTheta$ is a tuple (N, R, F, A, C, L, M), where the components are described as follows. The pair (N, C) is a TCN. The node set $N = R \uplus A \uplus F$ is partitioned into three disjoint sets: R is the set of regular nodes, F is the set of floating nodes, and A is the set of anchored nodes. $L: F \rightarrow \mathbb {R}$ maps each floating node to a duration. $M: A \rightarrow \mathsf {Int}$ maps each anchored node to a time interval. We write $N_\varTheta$, $R_\varTheta$, $F_\varTheta$, $A_\varTheta$, $C_\varTheta$, $L_\varTheta$, and $M_\varTheta$ for the components of $\varTheta$.

An instantiation of an ETCN $\varTheta$ is a function $m : N_\varTheta \rightarrow \mathsf {Int}$. Instantiation m satisfies $\varTheta$ if and only if (a) m satisfies the TCN $(N_\varTheta , C_\varTheta )$, (b) $len (m(v)) = L_\varTheta (v)$ for every $v \in F_\varTheta$, and (c) $m(v) = M_\varTheta (v)$ for every $v \in A_\varTheta$.

Definition 8

A presence predicate specifier (PPS) $Q$ is a syntactic means for specifying a presence predicate. It is defined inductively as follows, together with the functions $nodes (Q)$ and $regulars (Q)$.

• An ETCN $\varTheta$ is a PPS, with $nodes (\varTheta ) = N_\varTheta$ and $regulars (\varTheta ) = R_\varTheta$.

• If $Q _1$, ..., $Q _n$ are PPSs, such that $nodes (Q _1)$, ..., $nodes (Q _n)$ are pairwise disjoint, and $1 \le m \le n$, then the threshold construct $Q = (Q _1, \ldots , Q _n)_{\ge m}$ is a PPS. In addition, $nodes (Q) = \cup _{1 \le i \le n} nodes (Q _i)$, and $regulars (Q) = \cup _{1 \le i \le n} regulars (Q _i)$.

Function $m : X \rightarrow \mathsf {Int}$ is an instantiation of $Q$ if $X \subseteq nodes (Q)$. Instantiation m satisfies $Q$ if and only if the following holds:

• If $Q$ is an ETCN $\varTheta$, then $dom (m) = N_\varTheta$, and m satisfies $\varTheta$ as an ETCN.

• If $Q$ is a threshold construct $(Q _1, \ldots , Q _n)_{\ge m}$, then there exists at least m distinct PPSs $Q _i$ among $\{ Q _1, \ldots , Q _n \}$ such that $m|_{ nodes (Q _i)}$ satisfies $Q _i$.

The disjunction $Q _1 \vee Q _2$ and the conjunction $Q _1 \wedge Q _2$ denote $(Q _1, Q _2)_{\ge 1}$ and $(Q _1, Q _2)_{\ge 2}$ respectively.

We say that a PPS $Q$ represents a presence predicate $P$ if and only if, for every $\varPi \in \mathsf {PoC}$, $P ( \varPi )$ is true whenever $Q$ is satisfied by an instantiation m such that for every $v \in dom (m)$, either $v \not \in regulars ( Q)$ or $m(v) \in \varPi$.

Checking if a given instantiation m satisfies a predicate specifier $Q$ takes time polynomial to the size of $Q$.

Example 3

Suppose the presence policy $\mathcal {P} _2$ in Example 1 is $\{ P _t \}_{t \in \mathbb {R}}$. Then $P _t$ can be represented by the PPS $\varTheta$ defined as follows. (1) $R_\varTheta = \{ u \}$. (2) $F_\varTheta = \{ v \}$. (3) $A_\varTheta = \{ w \}$. (4) $L_\varTheta ( v )$ corresponds to T hours. (5) $A_\varTheta ( w )$ is the time interval that spans the last week (relative to the current time $t$). (6) $C_\varTheta (v, u) = C_\varTheta (v, w) = \{ s, d, f, eq \}$.

5.2 Supporting the Admissible-Window Policy Idiom

One of the benefits of basing presence policy specification on ETCNs is that the latter supports the authoring of R-resilient policies. The admissible-window policy idiom defined in Sect. 4.3 can be captured by a PPS in which every component ETCN $\varTheta = (N, R, F, A, C, L, M)$ has the following structural properties (the disjunctive relation $\mathbf B$ is the universal relation defined in Appendix A):

• If $u, v \in R$, or $u, v \in A$, then $C(u, v) = C(v, u) = \mathbf B$. If $u, v \in F$, then C(u, v) and C(v, u) can be any disjunctive relations.

• There is an injective function $flt : R \rightarrow F$, such that for every $u \in R$, $C( flt (u), u) = \{ s, d, f, eq \}$ and $C(u, flt (u)) = \{ si, di, fi, eq \}$. For $u \in R$ and $v \in F$, if $v \ne flt (u)$, then $C(u, v) = C(v, u) = \mathbf B$.

• There is a surjective function $anc : F \rightarrow A$. For every $u \in F$, $C(u, anc (u)) = \{ s, d, f, eq \}$ and $C( anc (u), u) = \{ si, di, fi, eq \}$. For $v \in F$ and $w \in A$, if $w \ne anc (v)$, then $C(v, w) = C(w, v) = \mathbf B$.

Intuitively, each anchored node encodes a window. Contained within each window is a set of floating nodes. The floating nodes can be related to one another via any temporal relations. It is required that each regular node u “covers” a distinct floating node $flt (u)$, meaning that the regular node u is required to intersect with the window $anc ( flt (u))$ for at least a duration of $L( flt (u))$. The duration requirements encode an R-resilient admissibility condition, while the threshold constructs encode a syntactically monotonic aggregation condition. Therefore, the presence predicate represented by such a PPS is R-resilient.

An ETCN $\varTheta$ that satisfies the above structural properties is said to be idiomatic. Every idiomatic ETCN $\varTheta$ with m anchored nodes represents the same presence predicate as the conjunction of m idiomatic ETCNs, each with only one anchored node. From now on we only consider idiomatic ETCNs with one anchored node.

Example 4

Consider $\mathcal {P} ^\star _5 = \{ P _t \}_{t \in \mathbb {R}}$ from Example 2. The presence predicate $P _t$ is represented by the disjunction $Q _{ Mon } \vee Q _{ Tue } \vee \ldots \vee Q _{ Sun }$. The PPS $Q _{ Mon }$ is the conjunction (assuming there are four Mondays in the previous month). is the ETCN $\varTheta$ defined as follows. (1) $A_\varTheta = \{ w \}$ contains a single window w where $M_\varTheta (w)$ is the interval spanning the first Monday of the previous month (relative to the current time $t$). (2) $F_\varTheta = \{ v \}$ contains a floating node v with duration $L_\varTheta (v)$ corresponding to T hours. (3) $R_\varTheta = \{ u \}$ contains a regular node u. (4) $C_\varTheta$ is formulated according to the structural properties above. The rest of the PPS can be formulated in an analogous manner.

5.3 Constructing a Proof of Compliance

A second benefit of adopting an ETCN-based policy language is that a proof of compliance can be validated to satisfy a presence predicate in a very efficient manner (with the help of a short witness). Note that constructing a proof of compliance is computationally hard, as the corresponding decision problem is $\mathsf {NP}$-complete (see Appendix B.3 for a proof).

• Problem:

• Instance: A PPS $Q$ and a finite set $DB$ of time intervals (previously issued by the location verifier).

• Question: Is there an instantiation m of $Q$ such that (a) m satisfies $Q$, and (b) for every $v \in dom (m)$, $v \in regulars (Q)$ implies $m(v) \in DB$?

Theorem 3

is $\mathsf {NP}$-complete.

In the above, the proof of compliance $\varPi$ is essentially $ran ( m|_{ regulars (Q) } )$, and m provides a “witness” explaining how $\varPi$ satisfies the policy predicate represented by $Q$. While constructing $\varPi$ and m is hard, checking if $\varPi$ satisfies the presence predicate represented by $Q$ when m is given is very efficient.

Although the requestor must now solve an $\mathsf {NP}$-complete problem (Sect. 3.4), the task is less formidable than it appears. First, according to Sect. 3.3 a policy certificate is effective for a duration of $\varDelta$, meaning that m can be reused before the policy certificate expires. Second, since the presence predicate represented by $Q$ is R-reducible (Theorem 1), the client does not need to store all the presence certificates ever issued to her, but only the one corresponding to the longest interval of each visitation. That means $DB$ has a manageable size. Third, the construction of a satisfying instantiation for $Q$ can be modularized by solving one idiomatic ETCN at a time. For each idiomatic ETCN $\varTheta$, we do not need to consider all the intervals in $DB$, but only those intervals that intersect with the anchored node of $\varTheta$. For typical window sizes like days, weeks, and months, the number of intersecting intervals is at best moderate if not small.

  instances can be solved by using a Mixed Integer Programming (MIP) solver. Mature implementations of MIP solvers are available (e.g., the Google CP-SAT Solver). We sketch below a Karp reduction that takes as input a instance consisting of (a) an idiomatic ETCN $\varTheta$, and (b) a finite set $DB$ of time intervals (previously certified by the location verifier), and returns an equivalent MIP instance. Suppose $DB = \{ I _1, \ldots , I _p \}$, $R_\varTheta = \{ u_1, \ldots , u_m \}$, $F_\varTheta = \{ v_1, \ldots , v_n \}$, and $A_\varTheta = \{ w \}$. A disjunctive relation $\mathbf{R }$ is restrictive if it does not contain all the 13 basic relations. For each restrictive $C_\varTheta (v_i, v_j)$, we enumerate its members as $\{ \mathbf{r } ^{i,j}_1, \ldots , \mathbf{r } ^{i,j}_{q(i,j)} \}$, where $q(i,j) = |C_\varTheta (v_i, v_j)|$. The output MIP instance consists of the following set of variables:

• 1. For $1 \le i \le m$ and $1 \le j \le p$, the boolean variable $b_{i,j}$ indicates whether the regular node $u_i$ is instantiated with time interval $I _j$.

• 2. For each restrictive $C_\varTheta (v_i, v_j)$, and $1 \le k \le q(i,j)$, the boolean variable $c_{i,j,k}$ indicates whether the time interval assigned to $v_i$ and the one assigned to $v_j$ are related by the basic relation $\mathbf{r } ^{i,j}_k$.

• 3. For $1 \le i \le n$, real variables $x^r_i$ and $y^r_i$ are the two boundary points of the time interval that is assigned to regular node $u_i$. Similarly, real variables $x^f_i$, $y^f_i$, $x^w$, $y^w$ are boundary points of the floating and anchored intervals.

The output MIP instance contains the following constraints:

• For $1 \le i \le m$, impose constraints (a) $\varSigma ^p_{j=1} b_{i,j} = 1$, (b) $x^r_i = \varSigma ^p_{j=1} min (I _j) \times b_{i,j}$, and (c) $y^r_i = \varSigma ^p_{j=1} max (I _j) \times b_{i,j}$.

• For $1 \le i \le m$ and $v_j = flt (u_i)$, impose (a) $x^r_i \le x^f_j$, and (b) $y^f_j \le y^r_i$.

• For $1 \le i \le n$, impose (a) $x^w \le x^f_i$, (b) $y^f_i \le y^w$, and (c) $y^f_i - x^f_i = L(v_i)$.

• Impose constraints $x^w = min (M(w))$ and $y^w = max (M(w))$.

• For each restrictive $C_\varTheta (v_i, v_j)$, impose constraint $\varSigma _{k = 1}^{q(i,j)} c_{i,j,k} = 1$.

• For each basic relation $\mathbf{r } ^{i,j}_k$ in a restrictive $C_\varTheta (v_i, v_j)$, impose a constraint to simulate the semantics of $\mathbf{r } ^{i,j}_k$ when $c_{i,j,k} = 1$. For example, if $\mathbf{r } ^{i,j}_k$ is the basic relation p (precedes), then impose the constraint $c_{i,j,k} \times y^f_i < c_{i,j,k} \times x^f_j + (1 - c_{i,j,k})$. If $c_{i,j,k} = 1$, then the constraint requires $y^f_i < x^f_j$ (i.e., the interval assigned to $v_i$ precedes the interval assigned to $v_j$). Otherwise, $c_{i,j,k} = 0$, and the constraint is trivially satisfied. The other 12 basic relations can be simulated in a similar manner.

Given a solution to the output MIP instance, one can construct a satisfying instantiation m of $\varTheta$ by consulting $x^r_i$, $y^r_i$, $x^f_i$, $y^f_i$, $x^w$, and $y^w$.

6 Performance Evaluation

An apparent challenge to our proposed authorization scheme is whether the requestor can efficiently construct a proof of compliance out of the set of presence certificates issued by the LV in the past. We conducted controlled experiments to demonstrate that constructing proofs of compliance using the MIP reduction in Sect. 5.3 can be performed with acceptable efficiency. All experiments were executed on an Intel Core i5 6200U 2.4 GHz PC with 8 GB DDR3 RAM, 512 GB SSD, running Windows 10 64-Bit. We used Python 3.6 to implement the MIP reduction (Sect. 5.3), and the Google CP-SAT Solver to solve the MIP instances and to collect timing statistics.

Experiment 1 - Increasing Policy Size: The first experiment was designed to assess the performance impact of different policy sizes. To that end, we fixed the number of presence certificates used for constructing proofs of compliance. Recall that the PPS can be solved modularly, one idiomatic ETCN at a time. The presence certificates considered for each idiomatic ETCN are only those that intersect with the anchored node. This number, in practice, is much smaller than the total number of presence certificates owned by the user. Suppose the window is a year, and the client visits her workplace once per day for 50 weeks during that year, we would expect her to accumulate approximately $50 \times 5 = 250$ presence certificates that intersect with the window (by R-resiliency, only one presence certificate needs to be kept for each visitation). We, therefore, constructed a timeline of 23 discrete time points and generated an interval set $DB$ containing all the $\left( {\begin{array}{c}23\\ 2\end{array}}\right) = 253 \approx 250$ distinct intervals on that timeline.

For each n from 5 to 50, in increments of 5, we generated 100 ETCNs. Each ETCN $\varTheta$ is generated according to the admissible-window structural properties (Sect. 5.2), with n regular nodes, n floating nodes ($v_1, \ldots , v_n$), and one anchored node (w). We set $M_\varTheta (w)$ to an interval covering all the 23 discrete time points. Then n intervals ($I _1, \ldots , I _n$) are randomly sampled from $DB$, with each sampled interval $I _i$ corresponding to a floating node $v_i$. We set $L_\varTheta (v_i) = len (I _i)$. For $v_i, v_j \in F_\varTheta$, we set $C_\varTheta (v_i, v_j) = \{ \mathbf{r } \}$, where $\mathbf{r }$ is the basic relation relating $I _i$ to $I _j$. The resulting instance $(\varTheta , DB )$ is thus satisfiable.

The 1,000 instances are reduced to MIP instances (Sect. 5.3). Each MIP instance is solved, and the solving time is recorded. If the MIP solver fails to obtain a solution within 2 s, we terminate the constraint-solving session. For only 5 out of the 1,000 MIP instances (0.5%) did the solver fail to complete within 2 s. We compute the average constraint-solving time for those completed instances. Figure 1a shows that policy size has a direct impact on the running time of the solver: the bigger n is, the more variables and constraints will there be in the MIP instance. Nevertheless, even with $n=50$ (and with 253 presence certificates to consider), the running time is still within 1.5 s, which is quite acceptable as the computed instantiation can be reused throughout the period $[t, t+\varDelta ]$ (Sect. 3.3 gives an example $\varDelta$ of 30 min).

Fig. 1.

Results: (a) Experiment 1; (b) Experiment 2

Experiment 2 - Increasing Certificate Number: This experiment was designed to evaluate the performance impact of increasing the number of presence certificates. Let $DB _m$ be the set of all $\left( {\begin{array}{c}m\\ 2\end{array}}\right)$ intervals from a timeline consisting of m discrete time points. For each integer m from 11 to 32, we generated 100 ETCNs in the same way we did in Experiment 1, but fixed $n = 30$. Again, the 2,200 MIP instances are solved, and the average constraint-solving time for each m is computed, excluding 3 of the 2,200 times ($0.14\%$) in which the MIP solver fails to complete in 2 seconds. See Fig. 1b. Increasing the number of certificates had a smaller effect than increasing the policy size, as the number of constraints added to the MIP instance when more certificates are used is much lower than the number of constraints added when the ETCN size is increased.

7 Conclusion and Future Work

A new access control model, SEPD, has been proposed for easing policy administration and facilitate trust inspiration in an open IoT environment. The architecture of the SEPD model is based on the metaphor of public spheres. We studied the security properties of presence policies, their expression in temporal constraint networks, and the efficiency of constructing proofs of compliance.

We are exploring a number of extensions to the SEPD model. First, we would like to extend SEPD with mechanisms for bootstrapping trust, so that newcomers (who have never been present) to a space can still inspire some level of trust when accompanied by a trusted escort. Second, we are working on a decentralized approach to resource discovery in a public sphere. Third, we are examining how reputation and presence history can be combined in a single distributed trust management framework.

Appendices

A Temporal Constraint Networks

Allen identifies 13 basic relations between any two time intervals [2, 26]. Those relations are precedes (p), meets (m), overlaps (o), starts (s), during (d), finishes (f), and their respective converse relations (i.e., preceded by [si], met by [mi], overlapped by [o], started by [si], contains [di], and finished by [fi]), as well as equality (eq). Table 1 gives the definition of these relations. These 13 basic relations capture all the possible relations between two intervals.

Let $\mathbf B = \{p, pi, m, mi, o, oi, s, si, d, di, f, fi, eq\}$ be the set of all basic relations. $\mathbf B$ is called the universal relation. We write $X \mathbf{r } Y$ to assert that interval X is related to interval Y in the basic relation $\mathbf{r }$. Given $X, Y \in \mathsf {Int}$, there exists exactly one basic relation $\mathbf{r } \in \mathbf B$ such that $X \mathbf{r } Y$. Given $\mathbf{R } \subseteq \mathbf B$, we write $X \mathbf{R } Y$ to assert that there exists $\mathbf{r } \in \mathbf{R }$ such that $X \mathbf{r } Y$. The set $\mathbf{R }$ is called a disjunctive relation.

A temporal constraint network (TCN) is an edge-labeled, complete, directed graph $\varTheta = (N, C)$, so that each directed edge $(u, v) \in N \times N$ is associated with a disjunctive relation $C(u, v) \subseteq \mathbf B$. An instantiation of $\varTheta$ is a function $m : N \rightarrow \mathsf {Int}$. Instantiation m satisfies $\varTheta$ if and only if $m(u) \,C(u, v)\, m(v)$ for every edge $(u, v) \in N \times N$. We say that $\varTheta$ is consistent if and only if there exists an instantiation that satisfies $\varTheta$.

Table 1. Allen’s 13 basic relations between intervals $X = [x_1, x_2]$ and $Y = [y_1, y_2]$.

B Proofs

1.1 B.1 Proof of Theorem 1

Statement (1): Suppose $P$ is semantically monotonic. Consider $\varPi , \varPi ' \in \mathsf {PoC}$ and $t \in \mathbb {R}$. If $\varPi \sqsubseteq _R \varPi '$ via the function $f : \varPi \rightarrow \varPi '$, then we have the following containment:

$$ \cup \varPi = \bigcup _{I \in \varPi } I \subseteq \bigcup _{I \in \varPi } f(I) \subseteq \bigcup _{I ' \in \varPi '} I ' \subseteq \cup \varPi ' $$

which, by semantic monotonicity, implies $P ( \varPi ) \rightarrow P ( \varPi ' )$. $P$ is therefore R-resilient.

Statement (2): We begin by proving that R-resiliency implies syntactic monotonicity. Suppose $P$ is R-resilient. Consider $\varPi , \varPi ' \in \mathsf {PoC}$ where $\varPi \subseteq \varPi '$. Construct $f : \varPi \rightarrow \varPi '$ so that $f(I) = I$. Thus $\varPi \sqsubseteq _R \varPi '$. By the R-resiliency of $P$, we have $P ( \varPi ) \rightarrow P ( \varPi ' )$ as required by syntactic monotonicity.

Next, we demonstrate that R-resiliency implies R-reducibility. Suppose $P$ is R-resilient. Consider $\varPi \in \mathsf {PoC}$ where there exists distinct intervals $I _1, I _2 \in \varPi$ such that $I _1 \subseteq _R I _2$. Construct $f : \varPi \rightarrow \varPi \setminus \{ I _1 \}$ so that:

$$ f( I) = {\left\{ \begin{array}{ll} I _2 &{} \text {if } I = I _1 \\ I &{} \text {otherwise} \end{array}\right. } $$

Function f thus witnesses to the fact that $\varPi \sqsubseteq _R \varPi \setminus \{ I _1 \}$. By R-resiliency, we know that $P ( \varPi ) \rightarrow P ( \varPi \setminus \{ I _1 \} )$.

So far, we have demonstrated that R-resiliency implies the conjunction of syntactic monotonicity and R-reducibility. We complete the proof of Statement (1) by showing that syntactic monotonicity and R-reducibility jointly imply R-resiliency. Suppose $P$ is both syntactically monotonic and R-reducible. Consider $\varPi , \varPi ' \in \mathsf {PoC}$. If $\varPi \sqsubseteq _R \varPi '$ via the function $f : \varPi \rightarrow \varPi '$, then the following implication holds:

1.2 B.2 Proof of Theorem 2

Let $\chi = (\mathsf {wd}, \mathsf {ad}, \mathsf {ag})$, and $\mathcal {P} ^\chi = \{ P _t \}_{t \in \mathbb {R}}$. Suppose $\varPi \sqsubseteq _R \varPi '$ via the function $f : \varPi \rightarrow \varPi '$. We show in the three steps below that $P _t (\varPi ) \rightarrow P _t (\varPi ')$.

Step 1. We show that $\varPi /W \sqsubseteq _R \varPi '/W$ for every $W \in \mathsf {Int}$. To this end, we construct a function $g : \varPi /W \rightarrow \varPi '/W$ so that $X \subseteq _R g(X)$ for every $X \in \varPi /W$.

Consider an interval $I \in \varPi$. Since $I \subseteq _R f(I)$, we know the following two facts: (1) If $I \cap W \ne \emptyset$, then $f(I) \cap W \ne \emptyset$. (2) $I \cap W \subseteq _R f(I) \cap W$. Therefore, by having g maps $I \cap W$ to $f(I) \cap W$ when $I \cap W \ne \emptyset$, the requirement of $X \subseteq _R g(X)$ will be satisfied.

The problem with the above construction is that the resulting mapping g may not be functional. The latter happens when there are distinct intervals $I _1, I _2 \in \varPi$ for which $I _1 \cap W = I _2 \cap W$. To correct this, observe that if $X \subseteq _R Y _1$ and $X \subseteq _R Y _2$, then either $Y _1 \subseteq _R Y _2$ or $Y _2 \subseteq _R Y _1$, and thus we have (a) $X \subseteq _R Y _1 \cup Y _2$, and (b) either $Y _1 = Y _1 \cup Y _2$ or $Y _2 = Y _1 \cup Y _2$. We therefore define g as follows:

$$ g(X) = \bigcup _{I \in \varPi ,\,I \cap W = X} f(I) \cap W $$

The function g witnesses to the fact that $\varPi /W \sqsubseteq _R \varPi '/W$.

Step 2. We demonstrate that $admissible ( \varPi , t) \subseteq admissible ( \varPi ', t )$. By definition, a window $W$ belongs to $admissible ( \varPi , t )$ whenever $\mathsf {ad} (\varPi /W)$. But we showed in Step 1 that $\varPi /W \sqsubseteq _R \varPi '/W$. Therefore, by the R-resiliency of $\mathsf {ad}$, we also have $\mathsf {ad}(\varPi '/W)$ as a result, meaning $W \in admissible ( \varPi ', t )$. Consequently, every member of $admissible ( \varPi , t)$ is also a member of $admissible ( \varPi ', t )$.

Step 3. We can now conclude that $P _t (\varPi ) \rightarrow P _t (\varPi ')$, because the syntactic monotonicity of $\mathsf {ag}$ guarantees that $\mathsf {ag}( admissible ( \varPi , t) ) \rightarrow \mathsf {ag}( admissible ( \varPi ', t) )$.

1.3 B.3 Proof of Theorem 3

That is in $\mathsf {NP}$ is obvious. We demonstrate $\mathsf {NP}$-hardness by a reduction from graph k-colorability [17]. Given an instance $G = (V, E)$ of graph k-colorability, the reduction produces an instance $(\varTheta , DB )$ of , where $DB$ contains k distinct intervals, and $\varTheta$ is the ETCN $(V, V, \emptyset , \emptyset , C, \emptyset , \emptyset )$, such that $C(u, v) = \mathbf B \setminus \{ eq \}$ if $uv \in E$, but $C(u, v) = \mathbf B$ if $uv \not \in E$. It is easy to see that G is k-colorable if and only if .