Canonical Completeness in Lattice-Based Languages for Attribute-Based Access Control

TL;DR

This paper explores canonical completeness in lattice-based attribute-based access control languages, extending previous work to partially ordered decision sets, and introduces a new logic and language extension for improved policy normal forms.

Contribution

It extends canonical completeness to lattice-structured truth values, constructs a new four-valued logic, and proposes an extended ABAC language, PTaCL_4^{≤}, for better policy representation.

Findings

Belnap logic-based ABAC languages are not canonically complete.

A new four-valued logic achieves canonical completeness.

The proposed language enhances policy normal forms and expressiveness.

Abstract

The study of canonically complete attribute-based access control (ABAC) languages is relatively new. A canonically complete language is useful as it is functionally complete and provides a "normal form" for policies. However, previous work on canonically complete ABAC languages requires that the set of authorization decisions is totally ordered, which does not accurately reflect the intuition behind the use of the allow, deny and not-applicable decisions in access control. A number of recent ABAC languages use a fourth value and the set of authorization decisions is partially ordered. In this paper, we show how canonical completeness in multi-valued logics can be extended to the case where the set of truth values forms a lattice. This enables us to investigate the canonical completeness of logics having a partially ordered set of truth values, such as Belnap logic, and show that ABAC languages based on Belnap logic, such as PBel, are not canonically complete. We then construct a canonically complete four-valued logic using connections between the generators of the symmetric group (defined over the set of decisions) and unary operators in a canonically suitable logic. Finally, we propose a new authorization language $\text{PTaCL}_{\sf 4}^{\leqslant}$, an extension of PTaCL, which incorporates a lattice-ordered decision set and is canonically complete. We then discuss how the advantages of $\text{PTaCL}_{\sf 4}^{\leqslant}$ can be leveraged within the framework of XACML.

Tables

Table 1. Table 1 : Properties of ABAC languages

Language	Decisions	Unary Ops	Binary Ops
XACML	$\{0,1,\perp \}$	$0$	$12$
PTaCL	$\{0,1,\perp \}$	$2$	$1$
PTaCL(E)	$\{0,1,\perp \}$	$2$	$1$
PBel	$\{0,1,\perp ,\top \}$	$1$	$2$

Equations

$$S_{(a_1,\dots ,a_n)}^j(x_1,\dots ,x_n)=\{\begin{array}{ll}j& \text{if (x1,…,xn)=(a1,…,an)},\\ 0& \text{otherwise}.\end{array}$$

$$\begin{array}[]{r|@{~}r@{~}r@{~}r@{~}r}S_{(0,2)}^{1}\lx@intercol\vrule~{}&0~{}&1~{}&2~{}&3\\ \hline\cr 0\lx@intercol\vrule~{}&0~{}&0~{}&1~{}&0\\ 1\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 2\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 3\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ \end{array}\qquad\begin{array}[]{r|@{~}r@{~}r@{~}r@{~}r}S_{(1,1)}^{2}\lx@intercol\vrule~{}&0~{}&1~{}&2~{}&3\\ \hline\cr 0\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 1\lx@intercol\vrule~{}&0~{}&2~{}&0~{}&0\\ 2\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 3\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ \end{array}\qquad\begin{array}[]{r|@{~}r@{~}r@{~}r@{~}r}S_{(3,0)}^{3}\lx@intercol\vrule~{}&0~{}&1~{}&2~{}&3\\ \hline\cr 0\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 1\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 2\lx@intercol\vrule~{}&0~{}&0~{}&0~{}&0\\ 3\lx@intercol\vrule~{}&3~{}&0~{}&0~{}&0\\ \end{array}$$

$$f(x,y)=\{\begin{array}{ll}1& \text{if x=0, y=2},\\ 2& \text{if x=y=1},\\ 3& \text{if x=3, y=0},\\ 0& \text{otherwise}.\end{array}$$

$$f(x,y)\equiv S_{(0,2)}^1(x,y)⋎S_{(1,1)}^2(x,y)⋎S_{(3,0)}^3(x,y).$$

$$f(x,y)\equiv (S_0^1(x)⋏S_2^1(y))⋎(S_1^2(x)⋏S_1^2(y))⋎(S_3^3(x)⋏S_0^3(y))$$

$$A=\left\{\mathbf{a}\in V^n:f(\mathbf{a})>0\right\};$$

$$f(\mathbf{x})={\text{bigcurlyvee}}_{\mathbf{a}\in A}{S}_{\mathbf{a}}^{f(\mathbf{x})}(\mathbf{x}).$$

$${\text{bigcurlyvee}}_{i=1}^r{\text{bigcurlywedge}}_{j=1}^s{♯}_{i,j}{x}_{i,j}$$

$${\delta }_q(t,p)$$

$${\delta }_q(d)$$

$${\delta }_q(-p)$$

$${\delta }_q(p\oplus p^{\prime })$$

$$\big{(}t_{6},(t_{4},-(t_{3},((t_{1},1)\oplus_{1}(t_{2},0))))\oplus_{2}(t_{5},0)\big{)}$$

$$d{\vee }_{\mathrm{p}}{d}^{\prime }\stackrel{\mathrm{def}}{=}\neg ((\neg d){\wedge }_{\mathrm{p}}(\neg d^{\prime })).$$

$$d\mathsf{po}{d}^{\prime }$$

$$d\mathsf{do}{d}^{\prime }$$

$$S_{\mathbf{a}}^j(\mathbf{x})=\{\begin{array}{ll}j& \text{if x=a},\\ \underline{v}& \text{otherwise.}\end{array}$$

$$S_{\mathbf{a}}^j(\mathbf{x})=\{\begin{array}{ll}j& \text{if }\mathbf{x}=\mathbf{a},\\ \perp & \text{otherwise.}\end{array}$$

$$\begin{array}[]{c|c|c}x&S_{0}^{0}&S_{1}^{\top}\\ \hline\cr\bot&\bot&\bot\\ 0&0&\bot\\ 1&\bot&\top\\ \top&\bot&\bot\\ \end{array}\qquad\begin{array}[]{c|cccc}S_{(1,\top)}^{0}&\bot&0&1&\top\\ \hline\cr\bot&\bot&\bot&\bot&\bot\\ 0&\bot&\bot&\bot&\bot\\ 1&\bot&\bot&\bot&0\\ \top&\bot&\bot&\bot&\bot\\ \end{array}$$

$$-\perp =\top ,-\top =\perp ,-0=0,\text{and }-1=1.$$

$$d{\oplus }_{\mathrm{b}}{d}^{\prime }\equiv -(-d{\otimes }_{\mathrm{b}}-d^{\prime }).$$

$$({\pi }_1\circ {\pi }_2)(x)\stackrel{\mathrm{def}}{=}{\pi }_1({\pi }_2(x)).$$

$$\pi (x)=\{\begin{array}{ll}b& \text{if }x=a,\\ a& \text{if }x=b,\\ x& \text{otherwise},\end{array}$$

$$\pi (x)=\{\begin{array}{ll}b& \text{if }x=a,\\ c& \text{if }x=b,\\ a& \text{if }x=c,\\ x& \text{otherwise},\end{array}$$

$$\begin{array}[]{c|c|c|c}~{}d{}&\mathop{\sim_{0}}d{}&\mathop{\sim_{1}}d&\mathop{\sim_{\top}}d\\ \hline\cr\bot&0&1&\top\\ 0&\bot&0&0\\ 1&1&\bot&1\\ \top&\top&\top&\bot\\ \end{array}$$

$$(\varphi (\perp ),\varphi (0),\varphi (1),\varphi (\top ))=(a,b,c,d).$$

$${\varphi }_x^y(z)=\{\begin{array}{ll}x& \text{if z=y},\\ \perp & \text{otherwise}.\end{array}$$

$$\varphi (x)={\varphi }_a^{\perp }(x){\oplus }_{\mathrm{b}}{\varphi }_b^0(x){\oplus }_{\mathrm{b}}{\varphi }_c^1(x){\oplus }_{\mathrm{b}}{\varphi }_d^{\top }(x).$$

$${\varphi }_a^{\perp }\equiv {\varphi }_{a,0}{\otimes }_{\mathrm{b}}{\varphi }_{a,1}{\otimes }_{\mathrm{b}}{\varphi }_{a,\top }$$

$$\begin{array}[]{c|c|c|c|c|c|c|c|c|c}x&\phi_{a,0}&\phi_{a,1}&\phi_{a,\top}&\phi_{a,0}\mathbin{\otimes_{\rm b}}\phi_{a,1}\mathbin{\otimes_{\rm b}}\phi_{a,\top}&\phi_{a}^{\bot}&\phi_{b}^{0}&\phi_{c}^{1}&\phi_{d}^{\top}&\phi_{a}^{\bot}\mathbin{\oplus_{\rm b}}\phi_{b}^{0}\mathbin{\oplus_{\rm b}}\phi_{c}^{1}\mathbin{\oplus_{\rm b}}\phi_{d}^{\bot}\\ \hline\cr\bot&a&a&a&a&a&\bot&\bot&\bot&a\\ 0&\bot&b_{2}&b_{3}&\bot&\bot&b&\bot&\bot&b\\ 1&b_{1}&\bot&c_{3}&\bot&\bot&\bot&c&\bot&c\\ \top&c_{1}&c_{2}&\bot&\bot&\bot&\bot&\bot&d&d\end{array}$$

$$d{\oplus }_{\mathrm{b}}{d}^{\prime }\equiv -(-d{\otimes }_{\mathrm{b}}-d^{\prime })\equiv {\sim }_{\top }({\sim }_{\top }d{\otimes }_{\mathrm{b}}{\sim }_{\top }{d}^{\prime }).$$

$$\begin{array}[]{c|cccc}\mathsf{ooa}&\bot&0&1&\top\\ \hline\cr\bot&\bot&0&1&\top\\ 0&0&\top&\top&\top\\ 1&1&\top&\top&\top\\ \top&\top&\top&\top&\top\\ \end{array}$$

Full text

††conference: CODASPY’17, March 22-24, 2017, Scottsdale, AZ, USA

1 Introduction

Access control is one of the most important security services in multi-user computer systems, providing a mechanism for constraining the interaction between (authenticated) users and protected resources. Generally, access control is implemented by an authorization service, which includes an authorization decision function for deciding whether a user request to access a resource (an “access request”) should be permitted or not. In its simplest form an authorization decision function either returns an $\sf{allow}$ or $\sf{deny}$ decision.

Most implementations of access control use authorization policies, where a user request to access a resource is evaluated with respect to a policy that defines which requests are authorized. Many recent languages for the specification of authorization policies are designed for “open”, distributed systems (rather than the more traditional “closed”, centralized systems in which the set of users was assumed to be known in advance). Such languages do not necessarily rely on user identities to specify policies; instead, policies are defined in terms of other user and resource attributes. The most widely used attribute-based access control (ABAC) language is XACML [14, 17]. However, XACML suffers from poorly defined and counterintuitive semantics [10, 15], and is inconsistent in its articulation of policy evaluation. PTaCL is a more formal language for specifying authorization policies [6], providing a concise syntax for policy targets and precise semantics for policy evaluation.

Crampton and Williams [7] recently introduced the notion of canonical completeness for ABAC languages, showing that XACML and PTaCL are not canonically complete and developing a variant of PTaCL that is canonically complete. These results apply to languages that support three decision values, which are assumed to be totally ordered. However, there are certain situations where it is useful to have four decisions available, and some languages, such as PBel [4], BelLog [18] and Rumpole [12], use four decisions, which are partially ordered.

In this paper, we extend existing results to languages that support four decision values, which need not be totally ordered. We show that PBel [4], perhaps the best-known four-valued ABAC language, is not canonically complete. We then develop a canonically complete ABAC language, based on PTaCL syntax and semantics. The language is abstract, but its operators could be implemented as combining algorithms in XACML, thereby leveraging the features that XACML provides for specifying attribute-based requests and targets, the evaluation of targets with respect to requests, and the storage and evaluation of policies.

In Section 2 we discuss background material and related work, which provides us with the primary motivation for this paper: to develop a canonically complete $4$-valued logic to support a tree-structured authorization language. The main contributions of this work are:

• •

to extend Jobe’s work on canonical completeness in multi-valued logics to the case where the set of truth values forms a lattice (Section 3.2);

• •

to establish that existing $4$-valued logics are not canonically complete (Section 3.3);

• •

to construct a canonically complete $4$-valued logic (Section 4);

• •

to construct a $4$-valued, canonically complete authorization language for ABAC (Section 5).

We conclude the paper with a summary of our contributions and a discussion of future work.

2 Background and Related Work

In this section, we summarize background material and related work, including tree-structured ABAC languages, canonical completeness, and four-valued languages for ABAC, thereby providing motivation for the work in the remainder of the paper.

2.1 Completeness in Multi-valued Logics

Let $V$ be a set of truth values. The set of formulae $\Phi(L)$ that can be written in a (multi-valued) propositional logic $L=(V,{\sf Ops})$ is defined by $V$ and the set of operators $\sf Ops$. For brevity, we will write $L$ when $V$ and $\sf Ops$ are obvious from context.

Let $V$ be a totally ordered set of $m$ truth values, $\left\{0,\dots,m-1\right\}$, with $0<1<\dots<m-1$. Then we say $L=(V,{\sf Ops})$ is canonically suitable if and only if there exist two formulas $\phi_{\max}$ and $\phi_{\min}$ of arity $2$ in $\Phi(L)$ such that $\phi_{\max}(x,y)$ returns $\max\left\{x,y\right\}$ and $\phi_{\min}(x,y)$ returns $\min\left\{x,y\right\}$. We will usually write $\phi_{\max}$ and $\phi_{\min}$ using the infix operators $\curlyvee$ and $\curlywedge$ respectively.

Example 1

Standard propositional logic with truth values [math] and $1$, and operators $\vee$ and $\neg$, representing disjunction and negation, respectively, is canonically suitable: $\phi_{\max}(x,y)$ is simply $x\vee y$, while $\phi_{\min}(x,y)$ is $\neg(\neg x\vee\neg y)$ (that is, conjunction).

A function $f:V^{n}\rightarrow V$ is completely specified by a truth table containing $n$ columns and $m^{n}$ rows. However, not every truth table can be represented by a formula in a given logic $L=(V,{\sf Ops})$. $L$ is said to be functionally complete if for every function $f:V^{n}\rightarrow V$, there is a formula $\phi\in\Phi(L)$ of arity $n$ whose evaluation corresponds to the truth table. In Section 2.2, we explain why we may regard a tree-structured authorization language as a logic defined by a set of decisions and the set of policy-combining operators. In this sense, XACML is not functionally complete [7], while PTaCL [6] and PBel are [4].

A selection operator $S_{(a_{1},\dots,a_{n})}^{j}$ is an $n$-ary operator defined as follows:

[TABLE]

We will write ${\bf a}$ to denote the tuple $(a_{1},\dots,a_{n})\in V^{n}$ when no confusion can occur. Note that $S_{{\bf a}}^{0}$ is the same for all ${\bf a}\in V^{n}$, and $S_{{\bf a}}^{0}({\bf x})=0$ for all ${\bf x}\in V^{n}$. Illustrative examples of binary selection operators (for a $4$-valued logic) are shown in Figure 1.

Selection operators play a central role in the development of canonically complete logics because an arbitrary function $f:V^{n}\rightarrow V$ can be expressed in terms of selection operators. Consider, for example, the function

[TABLE]

Then it is easy to confirm that

[TABLE]

Moreover, $S_{(a,b)}^{c}(x,y)\equiv S_{a}^{c}(x)\curlywedge S_{b}^{c}(y)$ for any $a,b,c,x,y\in V$. Thus,

[TABLE]

In other words, we can express $f$ as the “disjunction” ($\curlyvee$) of “conjunctions” ($\curlywedge$) of unary selection operators.

More generally, given the truth table of function $f:V^{n}\rightarrow V$, we can write down an equivalent function in terms of selection operators. Specifically, let

[TABLE]

then, for all ${\bf x}\in V^{n}$,

[TABLE]

Jobe established a number of results connecting the functional completeness of a logic with the unary selection operators, summarized in the following theorem.

Theorem 1** (Jobe [9, Theorems 1, 2; Lemma 1])**

A logic $L$ is functionally complete if and only if each unary selection operator is equivalent to some formula in $L$.

The normal form of formula $\phi$ in a canonically suitable logic is a formula $\phi^{\prime}$ that has the same truth table as $\phi$ and has the following properties:

• •

the only binary operators it contains are $\curlyvee$ and $\curlywedge$;

• •

no binary operator is included in the scope of a unary operator;

• •

no instance of $\curlyvee$ occurs in the scope of the $\curlywedge$ operator.

In other words, given a canonically suitable logic $L$ containing unary operators $\sharp_{1},\dots,\sharp_{\ell}$, a formula in normal form has the form

[TABLE]

where $\sharp_{i,j}$ is a unary operator defined by composing the unary operators in $\sharp_{1},\dots,\sharp_{\ell}$. In the usual $2$-valued propositional logic with a single unary operator (negation) this corresponds to disjunctive normal form.

A canonically suitable logic is canonically complete if every unary selection operator can be expressed in normal form. It is known that there are canonically suitable $3$-valued logics that are:

(i) not functionally complete [9, 11];

(ii) functionally complete but not canonically complete [9, Theorem 4]; and

(iii) canonically complete (and hence functionally complete) [9, Theorem 6].

Jobe defined a canonically complete $3$-valued logic [9]. The operators and the construction of the unary selection operators using these operators are given in Appendix A. The expression for $f$ above could be expressed in normal form, providing we could find suitable unary operators for a $4$-valued logic. In Section 4.3 we explain how to produce a suitable set of unary operators for an $m$-valued logic.

2.2 Tree-structured Languages for ABAC

Let $D$ be a set of authorization decisions. Typically, we assume $D$ contains the values [math], $1$ and $\bot$ representing “deny”, “allow” and “not-applicable”, respectively. We call [math] and $1$ conclusive decisions. Let $\oplus$ be an associative binary operator defined on $D$ and $-$ be a unary operator defined on $D$. Then

• •

an atomic policy is a pair $(t,d)$, where $d$ is a decision in $D$ and $t$ is a target predicate;

• •

an atomic policy is a policy;

• •

if $p$ and $p^{\prime}$ are policies, then $(t,p\oplus p^{\prime})$ and $(t,-p)$ are policies.

We will write $p$ to denote the policy $(\mathsf{true},p)$.

The first stage in policy evaluation for a request $q$ is to determine whether a policy is “applicable” to $q$ or not. Every (well-formed) request $q$, allows us to assign a truth value to the target $t$. Specifically, $t$ may evaluate to true, in which case the associated policy is applicable; otherwise the policy is not applicable.111The evaluation of requests is not relevant to the exposition of this paper. XACML provides a means of specifying requests and targets and an evaluation architecture for determining whether a target is applicable or not. Then, writing $\nu_{q}(t)$ to denote the truth value assigned to $t$ by $q$ and $\delta_{q}(p)$ to denote the decision assigned to policy $p$ for request $q$, we define:

[TABLE]

It is easy to see that we may represent a policy as a tree. Hence, we describe policy languages of this nature as tree-structured. The first stage in policy evaluation corresponds to labeling the nodes of tree applicable or not applicable. We then compute a decision for non-leaf nodes in the tree by combining the decisions assigned to their respective children. Figure 2 shows the tree for the policy

[TABLE]

and the evaluation of that policy for a request $q$ such that $\nu_{q}(t_{i})={\sf true}$ for all $i$ except $i=2$.

There are several tree-structured ABAC languages in the literature, including the OASIS standard XACML, PBel and PTaCL [17, 6, 4].222A number of policy algebras have also been defined, which have some similarities with tree-structured languages. The semantics of a policy are defined in terms of sets of authorized and denied requests [3, 19, 15, 16], and policy operators are defined in terms of set operations such as intersection and union. These languages differ to some extent in the choices of $D$ and the set of operators that are used. XACML, for example, defines several rule- and policy-combining algorithms (which may be regarded as binary operators), but no unary operators.333An XACML rule is equivalent to an atomic policy. PBel and PTaCL prefer to define a rather small set of operators: PTaCL defines a single binary operator and two unary operators, whereas PBel defines two binary operators and a single unary operator. XACML and PTaCL use a three-valued decision set comprising [math], $1$ and $\bot$, to which PBel adds $\top$, which represents “conflict”.

The main difference between existing languages, however, is the extent to which they are complete in the senses defined in Section 2.1 [7]. We summarize these differences in Table 1, where CS, FC and CC denote canonically suitable, functionally complete and canonically complete, respectively. In Section 3.3, we prove that PBel is canonically suitable but not canonically complete.

2.3 The Value of Canonical Completeness

One of the main difficulties with using a tree-structured language is writing the desired policy using the operators provided by the language. In particular, if it is not possible to express a policy using a single target and decision, the policy author must engineer the desired policy by combining sub-policies using the set of operators specified in the given language. This is a non-trivial task, in general. Moreover, in XACML it may be impossible to write the desired policy due to its functional incompleteness. Thus, a policy author may be forced to write a policy that approximates the desired policy, which may lead to unintended or undesirable decisions for certain requests.

An alternative approach, supported by XACML, is to define custom combining algorithms. However, there is no guarantee that the addition of a new combining algorithm will make XACML functionally complete. Thus, more and more custom algorithms may be required over time. This, in turn, will make the design decisions faced by policy authors ever more complicated, thereby increasing the chances of errors and misconfigurations.

In other words, we believe it is preferable to define a small number of operators having unambiguous semantics and providing functional completeness. A functionally complete ABAC language, such as PTaCL, can be used to construct any conceivable policy using the operators provided by the language. However, policy authors still face the challenge of finding the correct way to combine sub-policies using those operators to construct the desired policy.

For example, PTaCL defines three policy operators $\mathbin{\wedge_{\rm p}},\neg$ and $\sim$. To express XACML’s deny- and permit-overrides in PTaCL requires significant effort. For convenience, we introduce the operator $\mathbin{\vee_{\rm p}}$:

[TABLE]

It is then possible to show that

[TABLE]

The operators $\mathbin{\mathsf{po}}$ and $\mathbin{\mathsf{do}}$ are equivalent to the permit- and allow-overrides policy-combining algorithms in XACML. As can be seen, the definitions of these operators in terms of the PTaCL operators are complex, and, more generally, it is a non-trivial task to derive such formulae.

Disjunctive normal form in propositional logic makes it trivial to write down a logical formula, using only conjunction, disjunction and negation, that is equivalent to an arbitrary Boolean function expressed in the form of a truth table. Similarly, a canonically complete ABAC language, such as PTaCL(E) [7], makes it possible to write down a policy in normal form from its decision table. In this paper, we show that there exist $4$-valued canonically complete logics in which the set of truth values forms a lattice. We discuss why and how this can simplify policy generation in Section 5.2.

In addition, policies in normal form may be more efficient to evaluate. Given a formula in a 3-valued logic expressed in normal form, any literal that evaluates to 0 causes the entire clause to evaluate to 0, while any clause evaluating to 1 means the entire formula evaluates to 1. In short, the time required for policy evaluation may be reduced in many cases. (This is similar to the way in which algorithms such as first-applicable in XACML work: once an applicable policy is found policy evaluation terminates, even if there are additional policies that could be evaluated.)

2.4 The Value of a Fourth Decision

The XACML 2.0 standard includes a fourth authorization decision “indeterminate” [14]. This is used to indicate errors have occurred during policy evaluation, meaning that a decision could not be reached. The XACML 3.0 standard extends the definition of the indeterminate decision to indicate decisions that might have been reached, had evaluation been possible [17]. However, the indeterminate decision is used in XACML 3.0 for more than reporting errors. It is also used as a decision in the “only-one-applicable” combining algorithm, which returns indeterminate if two or more sub-policies are applicable.

More generally, a conflict decision is used in PBel (and languages such as Rumpole and BelLog) to indicate that two sub-policies return different conclusive decisions. PBel is functionally complete. In the remainder of this paper, we show that PBel is not canonically complete and then develop a canonically complete $4$-valued ABAC language.

3 Lattice-based Multi-valued

Logics

We first recall the definition of a lattice. Suppose $(X,\leqslant)$ is a partially ordered set. Then for a subset $Y$ of $X$, we say $u$ is an upper bound of $Y$ if $y\leqslant u$ for all $y\in Y$. We say $u^{\prime}$ is a least upper bound or supremum of $Y$ if $u^{\prime}\leqslant u$ for all upper bounds $u$ of $Y$. Note that a least upper bound of $Y$ (if it exists) is unique. We define greatest lower bound or infimum in an analogous way. A lattice $(X,\leqslant)$ is a partially ordered set such that for all $x,y\in X$ there exists a least upper bound of $x$ and $y$, denoted $\sup\left\{x,y\right\}$, and a greatest lower bound of $x$ and $y$, denoted by $\inf\left\{x,y\right\}$. The least upper bound of $x$ and $y$ is written as $x\vee y$ (the “join” of $x$ and $y$) and the greatest lower bound is written as $x\wedge y$ (the “meet” of $x$ and $y$). If $(X,\leqslant)$ is a finite lattice, as we will assume henceforth, then $(X,\leqslant)$ has a maximum element (that is, a unique maximal element) and a minimum element.

In the remainder of this section we

(i) describe Belnap logic [2], a well-known $4$-valued lattice-based logic;

(ii) extend the definitions of canonical suitability, selection operators and canonical completeness to lattices; and

(iii) show that Belnap logic and PBel are not canonically complete.

3.1 Belnap Logic

Belnap logic was developed with the intention of defining ways to handle inconsistent and incomplete information in a formal manner. It uses the truth values [math], $1$, $\bot$, and $\top$, representing “false”, “true”, “lack of information” and “too much information”, respectively. In the remainder of this paper, we will denote the four valued decision set $\left\{\bot,0,1,\top\right\}$ by $\mathsf{4}$.

The truth values [math], $1$, $\bot$ and $\top$ have an intuitive interpretation in the context of access control: [math] and $1$ are interpreted as the standard “deny” and “allow” decisions, $\bot$ is interpreted as “not-applicable” and $\top$ represents a conflict of decisions. PBel is a $4$-valued tree-structured ABAC language [4] based on Belnap logic.

The set of truth values in Belnap logic admits two orderings: a truth ordering $\leqslant_{t}$ and a knowledge ordering $\leqslant_{k}$. In the truth ordering, [math] is the minimum element and $1$ is the maximum element, while $\bot$ and $\top$ are incomparable indeterminate values. In the knowledge ordering, $\bot$ is the minimum element, $\top$ is the maximum element while [math] and $1$ are incomparable. Both $(\mathsf{4},\leqslant_{t})$ and $(\mathsf{4},\leqslant_{k})$ are lattices, forming the interlaced bilattice illustrated in Figure 3.

We write the meet and join in $(\mathsf{4},\leqslant_{t})$ as $\mathbin{\wedge_{\rm b}}$ and $\mathbin{\vee_{\rm b}}$, respectively; and the meet and join in $(\mathsf{4},\leqslant_{k})$ as $\mathbin{\otimes_{\rm b}}$ and $\mathbin{\oplus_{\rm b}}$, respectively. (We use the subscript $\rm b$ to differentiate the Belnap operators from the PTaCL operators $\mathbin{\wedge_{\rm p}}$ and $\mathbin{\vee_{\rm p}}$.)

We may interpret values in $V$ as operators of arity [math] (that is, constants). Then it is known that $L(\mathsf{4},\left\{\neg,\mathbin{\wedge_{\rm b}},\mathbin{\vee_{\rm b}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot,0,1,\top\right\})$ is functionally complete [1, Theorem 12] and that $\left\{\neg,\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot\right\}$ is a minimal functionally complete set of operators [1, Proposition 17]. The truth tables for the binary operators $\mathbin{\wedge_{\rm b}}$, $\mathbin{\vee_{\rm b}}$, $\mathbin{\otimes_{\rm b}}$, $\mathbin{\oplus_{\rm b}}$ and $\supset_{\rm b}$ are shown in Figure 11 (in Appendix B). The unary operator $\neg$ has the effect of switching the values [math] and $1$, leaving $\bot$ and $\top$ fixed; in other words, it acts like “classical” negation.

3.2 Canonical Completeness

Jobe’s definition of canonical suitability for multi-valued logics assumes a total ordering on the set of truth values. Given that Belnap logic [1], on which PBel is based, is a $4$-valued logic in which the set of truth values forms a lattice, we seek to extend the definition of canonical suitability to lattice-based logics.

Let $L$ be a logic associated with a lattice $(V,\leqslant)$ of truth values. Then $L$ is canonically suitable if and only if there exist in $L$ two formulas $\phi_{\max}$ and $\phi_{\min}$ of arity $2$ such that $\phi_{\max}(x,y)$ returns sup$\left\{x,y\right\}$ and $\phi_{\min}(x,y)$ returns inf$\left\{x,y\right\}$. If a logic is canonically suitable, we will write $\phi_{\max}(x,y)$ and $\phi_{\min}(x,y)$ using infix binary operators as $x\curlyvee y$ and $x\curlywedge y$, respectively.

Remark 1

The existence of $\sup\left\{x,y\right\}$ and $\inf\left\{x,y\right\}$ is guaranteed in a lattice; this is not true in general for partially ordered sets. And for a totally ordered (finite) set, $\sup\left\{x,y\right\}=\max\left\{x,y\right\}$ and $\inf\left\{x,y\right\}=\min\left\{x,y\right\}$, so our definitions are compatible with those of Jobe’s for totally ordered sets of truth values.

We now extend the definition of selection operators to a lattice-based logic. Let $L$ be a logic associated with a lattice $(V,\leqslant)$ of truth values, with minimum truth value $\underline{v}$. Then, for ${\bf a}\in V^{n}$, the $n$-ary selection operator $S_{{\bf a}}^{j}$ is defined as follows:

[TABLE]

Note $S_{{\bf a}}^{\underline{v}}(x)=\underline{v}$ for all ${\bf a},{\bf x}\in V^{n}$.

The definitions for normal form and canonically completeness for lattice-based logics are identical to total-ordered logics. Nevertheless, we reiterate the definitions here in the interests of clarity. The normal form of formula $\phi$ in a canonically suitable logic is a formula $\phi^{\prime}$ that has the same truth table as $\phi$ and has the following properties:

• •

the only binary operators it contains are $\curlyvee$ and $\curlywedge$;

• •

no binary operator is included in the scope of a unary operator;

• •

no instance of $\curlyvee$ occurs in the scope of the $\curlywedge$ operator.

A canonically suitable logic is canonically complete if every unary selection operator can be expressed in normal form.

3.3 Completeness of Belnap Logic and PBel

Having extended the definitions of canonical suitability, selection operators and canonical completeness to lattices, we now investigate how these concepts can be applied to Belnap logic [2]. The meet and join operators of the two lattices $(\mathsf{4},\leqslant_{t})$ and $(\mathsf{4},\leqslant_{k})$ defined in Belnap logic are different. Canonical suitability for a $4$-valued logic, defined as it is in terms of the ordering on the set of truth values, will thus depend on the ordering we choose on $\mathsf{4}$. Consequently, the $\curlywedge$ and $\curlyvee$ operators, along with the selection operators, will differ depending on the lattice that we choose.

In Section 5, we will argue in more detail for the use of a lattice-based ordering on $\mathsf{4}$ to support a tree-structured ABAC language. For now, we state that we will use knowledge-ordered lattice $(\mathsf{4},\leqslant_{k})$.444It is worth noting that results analogous to those presented in this paper can be obtained for the truth ordering. Results for a total ordering on $\mathsf{4}$ can be derived using existing methods [7, 9]. The intuition is that the minimum value in this lattice is $\bot$ (rather than [math] in $(\mathsf{4},\leqslant_{t})$) and that this value should be the default value for a policy (being returned when the policy is not applicable to a request). In the interests of brevity, we will henceforth write $\mathsf{4}_{k}$, rather than $(\mathsf{4},\leqslant_{k})$.

It follows from the functional completeness of $\left\{\mathbin{\neg},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot\right\}$ that $L(\mathsf{4}_{k},\left\{\mathbin{\neg},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot\right\})$ is canonically suitable. A similar argument applies to $\left\{\neg,\mathbin{\wedge_{\rm b}},\supset_{\rm b},\bot,\top\right\}$, the set of operators used in PBel.

As $\bot$ is the minimum truth value in the lattice $\mathsf{4}_{k}$, the $n$-ary selection operator $S_{\bf a}^{j}$ for $\mathsf{4}_{k}$ is defined by the following function:

[TABLE]

Examples of selection operators are shown in Figure 4.

Functional completeness also implies all unary selection operators can be expressed as formulas in the logics $L(\mathsf{4}_{k},\left\{\mathbin{\neg},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot\right\})$ and $L(\mathsf{4}_{k},\left\{\neg,\mathbin{\wedge_{\rm b}},\supset_{\rm b},\bot,\top\right\})$. However, we have the following result, from which it follows that neither of these logics is canonically complete.

Proposition 1

$L(\mathsf{4}_{k},\left\{\neg,\mathbin{\wedge_{\rm b}},\mathbin{\vee_{\rm b}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot,0,1,\top\right\})$* is not canonically complete.*

Proof 3.2**.**

*It is impossible to represent all unary selection operators in normal form. The statement follows from the following observations:

(i) Belnap logic defines one unary operator $\mathbin{\neg}$;

(ii) the only binary operators that may be used in normal form are $\mathbin{\oplus_{\rm b}}$ ($\curlywedge$) and $\mathbin{\otimes_{\rm b}}$ ($\curlyvee$); and

(iii) for any operator $\oplus\in\left\{\mathbin{\neg},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\}$ we have $\bot\oplus\bot=\bot$.

Thus it is impossible to construct a unary operator of the form $S_{\bot}^{d}$ for any $d\neq\bot$.*

Corollary 3.3**.**

PBel is not a canonically complete authorization language.

Proof 3.4**.**

PBel uses the set of operators $\left\{\mathop{\neg},\mathbin{\wedge_{\rm b}},\supset_{\rm b},\bot,\top\right\}$, which is a subset of $\left\{\neg,\mathbin{\wedge_{\rm b}},\mathbin{\vee_{\rm b}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot,0,1,\top\right\}$. Thus, by Proposition 1, this is not a canonically complete set of operators, so $L(\mathsf{4}_{k},\left\{\mathop{\neg},\mathbin{\wedge_{\rm b}},\supset_{\rm b},\bot,\top\right\})$ is not canonically complete either. Hence, we may conclude that PBel is not a canonically complete authorization language.

4 A Canonically Complete

4-valued Logic

In the proof of Proposition 1, we were unable to construct all unary selection operators using operators from the set $\left\{\mathop{\neg},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\}$, because there is no operator in which $\bot\oplus\bot\neq\bot$. This suggests that we will require at least one additional unary operator $-$, say, such that $-\bot\neq\bot$. Accordingly, we start with the unary operator, sometimes called “conflation” [8], such that

[TABLE]

Conflation is analogous to negation $\mathop{\neg}$, but inverts knowledge values rather than truth values. In addition to $\mathop{-}$, we include the operator $\mathbin{\otimes_{\rm b}}$ in our set of operators, since this is the join operator for $\mathsf{4}_{k}$.

Proposition 4.5**.**

$L(\mathsf{4}_{k},\left\{\mathop{-},\mathbin{\otimes_{\rm b}}\right\})$* is canonically suitable.*

Informally, the proof follows from the fact that $\mathop{-}$ and $\mathbin{\otimes_{\rm b}}$ have exactly the same effect on $\mathsf{4}_{k}$ as $\neg$ and $\mathbin{\wedge_{\rm b}}$ have on $(\mathsf{4},\leqslant_{t})$. More formally, the following equivalence holds [1]:

[TABLE]

The decision table establishing this equivalence is given in Figure 12 (in Appendix C). Hence, we conclude that the set of operators $\left\{\mathop{-},\mathbin{\otimes_{\rm b}}\right\}$ is canonically suitable, since $\curlywedge$ corresponds to $\mathbin{\otimes_{\rm b}}$ and $\curlyvee$ corresponds to $\mathbin{\oplus_{\rm b}}$.

Proposition 4.6**.**

$L(\mathsf{4}_{k},\left\{\mathop{-},\mathbin{\otimes_{\rm b}}\right\})$* is not functionally complete.*

Proof 4.7**.**

*The proof follows from the following observations:

(i) for the operators $\mathop{-}$ and $\mathbin{\otimes_{\rm b}}$, $\mathop{-}(0)=0$ and $0\mathbin{\otimes_{\rm b}}0=0$; and

(ii) any operator $\circ$ which is a combination of $\mathop{-}$ and $\mathbin{\otimes_{\rm b}}$, we have $0\circ 0=0$.

Thus it is impossible to construct an operator in which $0\circ 0\neq 0$.*

To summarize: $L(\mathsf{4}_{k},\left\{\neg,\mathbin{\wedge_{\rm b}},\mathbin{\vee_{\rm b}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}},\supset_{\rm b},\bot,0,1,\top\right\})$ is not canonically complete and $L(\mathsf{4}_{k},\left\{\mathop{-},\mathbin{\otimes_{\rm b}}\right\})$ is not functionally complete. We now investigate what additional operators should be defined to construct a set of operators which is canonically complete (and hence functionally complete).

Given that we cannot use any operators besides $\curlyvee$ and $\curlywedge$ in normal form, we focus on defining additional unary operators on $\mathsf{4}_{k}$. An important observation at this point is that any permutation (that is, a bijection) $\pi:\mathsf{4}\rightarrow\mathsf{4}$ defines a unary operator on $\mathsf{4}$. Accordingly, we now explore the connections between the group of permutations on $\mathsf{4}$ and unary operators on $\mathsf{4}$.

4.1 The Symmetric Group and Unary

Operators

The symmetric group $(S_{X},\circ)$ on a finite set of $|X|$ symbols is the group whose elements are all permutations of the elements in $X$, and whose group operation $\circ$ is function composition. In other words, given two permutations $\pi_{1}$ and $\pi_{2}$, $\pi_{1}\circ\pi_{2}$ is a permutation such that

[TABLE]

We write $\pi^{k}$ to denote the permutation obtained by composing $\pi$ with itself $k$ times.

A transposition is a permutation which exchanges two elements and keeps all others fixed. Given two elements $a$ and $b$ in $X$, the permutation

[TABLE]

is a transposition, which we denote by $(a\,b)$. A cycle of length $k\geqslant 2$ is a permutation $\pi$ for which there exists an element $x$ in $X$ such that $x,\pi(x),\pi^{2}(x),\dots,\pi^{k}(x)=x$ are the only elements changed by $\pi$. Given $a$, $b$ and $c$ in $X$, for example, the permutation

[TABLE]

is a cycle of length $3$, which we denote by $(a\,b\,c)$. (Cycles of length two are transpositions.) The symmetric group $S_{X}$ is generated by its cycles. That is, every permutation may be represented as the composition of some combination of cycles.

In fact, stronger results are known. We first introduce some notation. Let $X=\left\{x_{1},\dots,x_{n}\right\}$ and let $S_{n}$ denote the symmetric group on the set of elements $\left\{1,\dots,n\right\}$. Then $(S_{X},\circ)$ is trivially isomorphic to $(S_{n},\circ)$ (via the mapping $x_{i}\mapsto i$).

Theorem 4.8**.**

For $n\geqslant 2$, $S_{n}$ is generated by the transpositions $(1\,2),(1\,3),\dots,(1\,n).$

Theorem 4.9**.**

For $1\leqslant a<b\leqslant n$, the transposition $\left(a\,b\right)$ and the cycle $(1\,2\,\dots\,n)$ generate $S_{n}$ if and only if the greatest common divisor of $b-a$ and $n$ equals $1$.

In other words, it is possible to find a generating set comprising only transpositions, and it is possible to find a generating set containing only two elements.

4.2 New Unary Operators

We now define three unary operators $\mathop{\sim_{0}},\mathop{\sim_{1}}$ and $\mathop{\sim_{\top}}$, which swap the value of $\bot$ and the truth value in the operator’s subscript. The truth tables for these operators are shown in Figure 5. Note that $\mathop{\sim_{\top}}$ is identical to the conflation operator $\mathop{-}$. However, in the interests of continuity and consistency we will use the $\mathop{\sim_{\top}}$ notation in the remainder of this section.

Notice that $\mathop{\sim_{0}}$, $\mathop{\sim_{1}}$ and $\mathop{\sim_{\top}}$ permute the elements of $\mathsf{4}$ and correspond to the transpositions $(\bot\,0)$, $(\bot\,1)$ and $(\bot\,\top)$, respectively. Thus we have the following elementary result.

Proposition 4.10**.**

Any permutation on $\mathsf{4}$ can be expressed using only operators from the set $\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}}\right\}$.

Proof 4.11**.**

*The operators $\mathop{\sim_{0}},\mathop{\sim_{1}}$ and $\mathop{\sim_{\top}}$ are the transpositions $(\bot\,0),(\bot\,1)$ and $(\bot\,\top)$ respectively. By Theorem 4.8, these operators generate all the permutations in $S_{\mathsf{4}}$. *

Lemma 4.12**.**

It is possible to express any function $\phi:\mathsf{4}\rightarrow\mathsf{4}$ as a formula in $L(\mathsf{4}_{k},\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\})$.

Proof 4.13**.**

For convenience, we represent the function $\phi:\mathsf{4}\rightarrow\mathsf{4}$ as the tuple

[TABLE]

Then, given $x,y,z\in\mathsf{4}$, we define the function

[TABLE]

Thus, for example, $\phi_{a}^{\bot}=(a,\bot,\bot,\bot)$. Then it is easy to see that for all $x\in\mathsf{4}$

[TABLE]

That is $\phi=\phi_{a}^{\bot}\mathbin{\oplus_{\rm b}}\phi_{b}^{0}\mathbin{\oplus_{\rm b}}\phi_{c}^{1}\mathbin{\oplus_{\rm b}}\phi_{d}^{\top}$.

Thus, it remains to show that we can represent $\phi_{a}^{\bot}$, $\phi_{b}^{0}$, $\phi_{c}^{1}$ and $\phi_{d}^{\top}$ as formulas using the operators in $\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\}$. First consider the permutations $\phi_{a,0}$, $\phi_{a,1}$ and $\phi_{a,\top}$, represented by the tuples $(a,\bot,b_{1},c_{1})$, $(a,b_{2},\bot,c_{2})$ and $(a,b_{3},c_{3},\bot)$, respectively.555Note that the specific values of $b_{i}$ and $c_{i}$ are not important: it suffices that each of $\phi_{a,0}$, $\phi_{a,1}$ and $\phi_{a,\top}$ are permutations; once $b_{i}$ is chosen such that $b_{i}\not\in\left\{a,\bot\right\}$, then $c_{i}$ is fixed. Since $\phi_{a,0}$, $\phi_{a,1}$ and $\phi_{a,\top}$ are permutations, we know they can be written as some combination of the unary operators. Moreover,

[TABLE]

Clearly, we can construct $\phi_{b}^{0}$, $\phi_{c}^{1}$ and $\phi_{d}^{\top}$ in a similar fashion. The result now follows.

The decision tables showing the construction of $\phi_{a}^{\bot}$ (column 5) and $\phi$ (column 10) are shown in Figure 6.

Theorem 4.14**.**

$L(\mathsf{4}_{k},\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\})$* is functionally and canonically complete.*

Proof 4.15**.**

By Lemma 4.12, it is possible to express any function $\phi:\mathsf{4}\rightarrow\mathsf{4}$ as a formula using operators from the set $\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\}$. In particular, all unary selection operators can be expressed in this way. Hence by Theorem 1, the set of operators $\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}},\mathbin{\oplus_{\rm b}}\right\}$ is functionally complete.

Moreover, all formulae constructed in the proof of Lemma 4.12 contain only the binary operators $\mathbin{\oplus_{\rm b}}(\curlyvee)$ and $\mathbin{\otimes_{\rm b}}(\curlywedge)$, and unary operators defined as compositions of $\mathop{\sim_{0}},\mathop{\sim_{1}}$ and $\mathop{\sim_{\top}}$. Thus, by definition, the unary selection operators are in normal form.

Corollary 4.16**.**

$L(\mathsf{4}_{k},\left\{\mathop{\sim_{0}},\mathop{\sim_{1}},\mathop{\sim_{\top}},\mathbin{\otimes_{\rm b}}\right\})$* is functionally and canonically complete.*

Proof 4.17**.**

The conflation operator $\mathop{-}$ and $\mathop{\sim_{\top}}$ are identical. Hence

[TABLE]

Therefore, the set of operators is canonically suitable, and, by Theorem 4.14, it is functionally and canonically complete (since we can construct $\mathbin{\oplus_{\rm b}}$).

Corollary 4.18**.**

Let $\diamond$ be the unary operator corresponding to the permutation given by the cycle $(\bot\,0\,1\,\top)$. Then $L(\mathsf{4}_{k},\left\{\mathop{\sim_{\top}},\diamond,\mathbin{\otimes_{\rm b}}\right\})$ is functionally and canonically complete.

Proof 4.19**.**

By Theorem 4.9, $\mathop{\sim_{\top}}$ and $\mathop{\diamond}$ generate all permutations in $S_{\mathsf{4}}$. The remainder of the proof follows immediately from Lemma 4.12 and Theorem 4.14.

It is important to note that we could choose any transposition $\left(a\,b\right)$, such that $\mathsf{gcd}(b-a,n)=1$. We specifically selected the transposition $\left(\bot\,\top\right)$, as this has the effect of reversing the minimum and maximum knowledge values. Another choice for this transposition is one which swaps 0 and 1, specifically the transposition $\left(0\,1\right)$. This transposition is the truth negation operator $\mathop{\neg}$, which in the context of access control is a useful operator, since it swaps allow and deny decisions.

4.3 Unary Operators for Totally Ordered

Logics

Having shown the construction for a canonically complete 4-valued logic, in which the set of logical values forms a lattice, we briefly return to totally ordered logics. We construct a totally ordered, canonically complete $m$-valued logic (thus extending the work of Jobe, who only showed how to construct a canonically complete $3$-valued logic).

Let $V$ be a totally ordered set of $m$ truth values, $\left\{1,\dots,m\right\}$, with $1<\dots<m$. We define two unary operators $\mathop{\dagger}$ and $\mathop{\diamond}$, which are the transposition $(1\,m)$ and the cycle $(1\,2\,\dots\,m)$, respectively. In addition, we define one binary operator $\mathbin{\wedge_{t}}$, where $x\mathbin{\wedge_{t}}y=\max\left\{x,y\right\}$.

Proposition 4.20**.**

Any permutation on $V$ can be expressed using only operators from the set $\left\{\mathop{\dagger},\mathop{\diamond}\right\}$.

Proof 4.21**.**

The operator $\mathop{\dagger}$ is the transposition $(1\,m)$ and the operator $\mathop{\diamond}$ is the cycle $(1\,2\,\dots\,m)$. By Theorem 4.9, these operators generate all the permutations in $S_{V}$.

Proposition 4.22**.**

$L(V,\left\{\mathop{\dagger},\mathop{\diamond},\mathbin{\wedge_{t}}\right\})$* is canonically suitable.*

Proof 4.23**.**

Clearly $x\curlywedge y\equiv x\mathbin{\wedge_{t}}y$, it remains to show the operator $\curlyvee$ can be expressed in $L$. By Proposition 4.20 we can express any permutation of $V$ in terms of $\mathop{\dagger}$ and $\mathop{\diamond}$. In particular, we can express the permutation $f$, where $f(i)=m-i+1$, which swaps the values $1$ and $m$, $2$ and $m-1$, and so on. We denote the unary operator which realizes this permutation by $\mathop{\updownarrow}$. Then $x\curlyvee y\equiv x\vee_{t}y\equiv\mathop{\updownarrow}(\mathop{\updownarrow}x\mathbin{\wedge_{t}}\mathop{\updownarrow}y)$.

Theorem 4.24**.**

$L(V,\left\{\mathop{\dagger},\mathop{\diamond},\mathbin{\wedge_{t}}\right\}$* is functionally and canonically complete.*

We omit the proof, as it proceeds in an analogous manner to those for Lemma 4.12 and Theorem 4.14. It is interesting to note that we have constructed a canonically complete $m$-valued logic which uses only two unary operators. This is somewhat unexpected; intuition would suggest that $m-1$ unary operators are required for a canonically complete $m$-valued logic.

5 A Canonically Complete

4-valued ABAC Language

Having identified a canonically complete set of operators for Belnap logic, we now investigate how this set of operators can be used in an ABAC language, and consider the advantages in doing so. Crampton and Williams [7] showed the operators in PTaCL can be replaced with an alternative set of operators, taken from Jobe’s logic $E$, to obtain a canonically complete $3$-valued ABAC language. In the remainder of this section, we describe a 4-valued lattice-ordered version of PTaCL, based on the lattice $\mathsf{4}_{k}$, which we denote by $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$.

5.1 The Decision Set

We first reiterate there is value in having an ABAC language for which policy evaluation can return a fourth value $\top$. Such a value is used in both XACML and PBel, although its use in XACML is somewhat ad hoc and confusing since it can be used to indicate

(a) an error in policy evaluation, or

(b) a decision that arises for a particular operator during normal policy evaluation.

We will use this fourth value to denote that (normal) policy evaluation has led to conflicting decisions (and we do not wish to use deny-overrides or similar operators to resolve the conflict at this point in the evaluation). (We explain how we handle indeterminacy arising from errors in policy evaluation in Section 5.3.) Two specific operators, “only-one-applicable” (ooa) and “unanimity” (un) could make use of $\top$: the ooa operator returns the value of the applicable sub-policy if there is only one such policy, and $\top$ otherwise; whereas the un operator returns $\top$ if the sub-policies return different decisions, and the common decision otherwise. The decision tables for these operators are shown in Figure 7.

In establishing canonical completeness for PTaCL(E), Crampton and Williams assumed a total order on the set of decisions ($0<\bot<1$). This ordering does not really reflect the intuition behind the use of [math], $1$ and $\bot$ in ABAC languages. In the context of access control, [math] and $1$ are incomparable conclusive decisions, and $\bot$ and $\top$ are decisions that reflect the inability to reach a conclusive decision either because a policy or its sub-policies are inapplicable ($\bot$) or because a policy’s sub-policies return conclusive decisions that are incompatible in some sense ($\top$). Moreover, we can subsequently resolve $\bot$ and $\top$ into one of two (incomparable) conclusive decisions using unary operators such as “deny-by-default” and “allow-by-default”. (The truth-based ordering on $\mathsf{4}$ does not correspond nearly so well to the above intuitions.)

5.2 Operators and Policies

We define the set of operators for $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ to be $\left\{\mathop{\sim_{\top}},\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$, which we established is canonically complete in Corollary 4.18. Recall that $\mathop{\sim_{\top}}$ is equivalent to conflation $-$; we will use the simpler notation $-$ in the remainder of this section. An atomic policy has the form $(t,d)$, where $t$ is a target and $d\in\left\{0,1\right\}$. (There is no reason for an atomic policy to return $\top$ – which signifies a conflict has taken place – in an atomic policy.) Then we have the following policy semantics.

[TABLE]

We now show how to represent the operator only-one-applicable ($\mathsf{ooa}$) in normal form. (Recall that it is possible to represent this operator as a formula in PBel; however, it is non-trivial to derive such a formula.) Using the truth table in Figure 7 and by definition of the selection operators and $\curlyvee$, we have $x\mathbin{\mathsf{ooa}}y$ is equivalent to

[TABLE]

Moreover, $S_{(x,y)}^{z}=S_{x}^{z}\curlywedge S_{y}^{z}$ and $S_{x}^{y}$ is a function $\phi:\mathsf{4}\rightarrow\mathsf{4}$, which can be represented as a composition of unary operators. Hence, we can derive a formula in normal form for $\mathbin{\mathsf{ooa}}$.

Functional completeness implies we can write any binary operator (such as XACML’s deny-overrides policy-combining algorithm) as a formula in $L(\mathsf{4}_{k},\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$, and hence we can use any operator we wish in $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ policies. However, canonical completeness and the decision set $(\mathsf{4},\leqslant_{k})$ allows for a completely different approach to constructing ABAC policies. Suppose a policy administrator has identified three sub-policies $p_{1}$, $p_{2}$ and $p_{3}$ and wishes to define an overall policy $p$ in terms of the decisions obtained by evaluating these sub-policies. Then the policy administrator can tabulate the desired decision for all relevant combinations of decisions for the sub-policies, as shown in the table below. The default decision is to return $\bot$, indicating that $p$ is “silent” for other combinations.

[TABLE]

Then, treating $p$ as a function of its sub-policies, we have

[TABLE]

The construction of $p$ as a “disjunction” ($\curlyvee$) of selection operators ensures that the correct value is returned for each combination of values (in much the same as disjunctive normal form may be used to represent the rows in a truth table). Note that if $p_{1}$, $p_{2}$ and $p_{3}$ evaluate to a tuple of values other than one of the rows in the table, each of the selection operators will return $\bot$ and thus $p$ will evaluate to $\bot$. Each operator of the form $S_{(a,b,c)}^{d}$ can be represented as the “conjunction” ($\curlywedge$) of unary selection operators (specifically $S_{a}^{d}\curlywedge S_{b}^{d}\curlywedge S_{c}^{d}$).

Of course, one would not usually construct the normal form by hand, as we have done above. Indeed, we have developed an algorithm which takes an arbitrary policy expressed as a decision table as input, and outputs the equivalent normal form expressed in terms of the operators $\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$. In order to develop this algorithm, we also derived expressions for the unary selection operators in terms of the operators $\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$. (In Lemma 4.12 we only showed that such expressions exist.) Our implementation of the algorithm, comprising just less than $150$ lines of Python code, shows the ease with which construction of policies can be both automated and simplified, utilizing the numerous advantages that have been discussed throughout this paper.666Code and test results available at goo.gl/0TM0RD.

5.3 Indeterminacy

XACML uses the indeterminate value in two distinct ways:

as a decision returned (during normal evaluation) by the “only-one-applicable” policy-combining algorithm; and 2. 2.

as a decision returned when some (unexpected) error has occurred in policy evaluation has occurred.

In the second case, the indeterminate value is used to represent alternative outcomes of policy evaluation (had the error not occurred). We believe that the two situations described are quite distinct and require different policy semantics. However, the semantics of indeterminacy in XACML are confused because

(i) the indeterminate value is used in two different ways, as described above, and

(ii) there is no clear and uniform way of establishing the values returned by the combining algorithms when an indeterminate value is encountered.

We have seen how $\top$ may be used to represent decisions for operators such as $\mathbin{\mathsf{ooa}}$ and $\mathsf{un}$. We handle errors in target evaluation (and thus indeterminacy) using sets of possible decisions [5, 6, 10]. (This approach was adopted in a rather ad hoc fashion in XACML 3.0, using an extended version of the indeterminate decision.) Informally, when target evaluation fails, denoted by $\nu_{q}(t)=\ ?$, PTaCL assumes that either $\nu_{q}(t)=1$ or $\nu_{q}(t)=0$ could have been returned, and returns the union of the (sets of) decisions that would have been returned in both cases. The formal semantics for policy evaluation in $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ in the presence of indeterminacy are defined in Figure 8.

The semantics for the operators $\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$ operate on sets, rather than single decisions, in the natural way. A straightforward induction on the number of operators in a policy establishes that the decision set returned by these extended semantics will be a singleton if no target evaluation errors occur; moreover, that decision will be the same as that returned by the standard semantics.

5.4 Leveraging the XACML Architecture

XACML is a well-known, standardized language, and many of the components and features of XACML are well-defined. However, it has been shown that the rule- and policy-combining algorithms defined in the XACML standard suffer from some shortcomings [10], notably inconsistencies between the rule- and policy-combining algorithms. PTaCL, on which $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ is based, is a tree-structured ABAC language that is explicitly designed to use the same general policy structure and evaluation methods as XACML. However, PTaCL differs substantially from XACML in terms of policy combination operators and semantics.

Thus, we suggest that $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ operators could replace the rule- and policy-combining algorithms of XACML, while those parts of the language and architecture that seem to function well may be retained. Specifically, we use the XACML architecture to:

(i) specify requests;

(ii) specify targets;

(iii) decide whether a policy target is applicable to a given request; and

(iv) use the policy decision point to evaluate policies.

In addition, we would retain the enforcement architecture of XACML, in terms of the policy decision, policy enforcement and policy administration points, and the relationships between them.

We believe it would be relatively easy to modify the XACML PDP to

• •

handle four decisions, extending the current set of values (“allow”, “deny” and “not-applicable”) to include “conflict”;

• •

implement the policy operators $\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$ as custom combining algorithms; and

• •

work with decision sets, in order to handle indeterminacy in a uniform manner.

For illustrative purposes, Appendix D specifies the modified decision set and pseudocode for the operator $\mathbin{\otimes_{\rm b}}$ in the format used by the XACML standard.

The main difference to end-users would be in the simplicity of policy authoring. Using standard XACML, policy authors must decide which rule- and policy-combining algorithms should be used to develop a policy or policy set that is equivalent to the desired policy. This is error-prone and it may not even be possible to express the desired policy using only the XACML combining algorithms. Using XACML with the policy-combining mechanisms of $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$, we can present an entirely different interface for policy authoring to the end-user. The policy author would first specify the atomic policies (XACML rules), then combine atomic policies using decision tables to obtain more complex policies (as illustrated in Section 5.2). Those policies can be further combined by specifying additional decision tables. At each stage a back-end policy compiler can be used to convert those policies into policy sets (using $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ operators) that can be evaluated by the XACML engine.

6 Concluding Remarks

Attribute-based access control is of increasing importance, due to the increasing use of open, distributed, interconnected and dynamic systems. The introduction of canonically complete ABAC languages [7] provides the ability to express any desired policy in a normal form, which allows for the possibility of specifying policies in the form of a decision table and then automatically compiling them into the language.

In this paper, we make important contributions to the understanding of canonical completeness in multi-valued logics and thus in ABAC languages. First, we extend Jobe’s work on canonical completeness to multi-valued logics to the case where the set of truth values forms a lattice. We show that the Belnap set of operators [2] (and thus any subset thereof) is not canonically complete, hence any ABAC language based on these operators cannot be canonically complete. In particular, PBel [4], probably the most well known $4$-valued ABAC language, is not canonically complete. We introduce a new four-valued logic $L(\mathsf{4}_{k},\left\{-,\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\})$ which is canonically complete, without having to explicitly construct the unary selection operators in normal form (unlike Jobe [9] and Crampton and Williams [7]). By identifying the connection between the generators of the symmetric group and the unary operators of logics, we have developed a simple and generic method for identifying a set of unary operators that will guarantee the functional and canonical completeness of an $m$-valued lattice-based logic. We also showed that there is a set of operators containing only three connectives which is functionally complete for Belnap logic, in contrast to the set of size four identified by Arieli and Avron [1].

Second, we show in $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ how the canonically complete set of operators $\left\{\mathop{-},\mathop{\diamond},\mathbin{\otimes_{\rm b}}\right\}$ can be used in an ABAC language, and present the advantages of doing so. In particular, we are no longer forced to use a totally ordered set of three decisions to obtain canonical completeness (as in the case in PTaCL(E)). Moreover, the overall design of PTaCL and hence $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ is compatible with the overall structure of XACML policies. We discuss how the XACML decision set and rule-combining algorithms can be modified to support $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$. Doing so enables us to retain the rich framework provided by XACML for ABAC (in terms of its languages for representing targets and requests) and its enforcement architecture (in terms of the policy enforcement, policy decision and policy administration points). Thus, we are able to propose an enhanced XACML framework within which any desired policy may be expressed. Moreover, the canonical completeness of $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$, means that the desired policy may be represented in simple terms by a policy author (in the form of a decision table) and automatically compiled into a PDP-readable equivalent policy.

Our work paves the way for a considerable amount of future work. In particular, we intend to develop a modified XACML PDP that implements the $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ operators. We also hope to develop a policy authoring interface in which users can simply state what decision a policy should return for particular combinations of decisions from sub-policies. This would enable us to evaluate the usability of such an interface and compare the accuracy with which policy authors can generate policies using standard XACML combining algorithms compared with the methods that $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ can support.

On the more technical side, we would like to revisit the notion of monotonicity [6] in targets and how this affects policy evaluation in ABAC languages. The definition of monotonicity is dependent on the ordering chosen for the decision set and existing work on monotonicity assumes the use of a totally ordered $3$-valued set (comprising [math], $\bot$ and $1$). So it will be interesting to consider how the use of a $4$-valued lattice-ordered decision set affects monotonicity. We also intend to investigate methods of policy compression, analogous to the minimization of Boolean functions [13], where we take the canonical form of a policy (generated from a decision table) and rewrite it in such a way as to minimize the number of terms in the policy.

Appendix A Jobe’s Canonically Complete 3-valued logic

Consider the 3-valued logic $J$ [9], whose operators $\wedge_{\rm e},\mathop{\sim_{1}}$ and $\mathop{\sim_{2}}$ are defined in Figure 9.

It is easy to establish that

[TABLE]

Thus $J$ is canonically suitable [9, Theorem 6]. The normal-form formulas for the unary selection operators are shown in Figure 10. (Note that $S_{i}^{0}$ is the same for all $i$.) Thus $J$ is functionally and canonically complete [9, Theorem 7]. Hence, it is possible to construct a canonically complete $3$-valued logic using the operators $\left\{\wedge_{\rm e},\sim_{0},\sim_{1}\right\}$.

Appendix B Operators in Belnap Logic

Appendix C Proof of Proposition 2

The decision table in Figure 12 establishes the equivalence of $x\mathbin{\oplus_{\rm b}}y$ and $-(x\mathbin{\otimes_{\rm b}}-y)$, which proves that $L((\mathsf{4},\leqslant_{k}),\left\{-,\mathbin{\otimes_{\rm b}}\right\})$ is a canonically suitable logic (Proposition 4.5).

Appendix D Encoding PTaCL Decisions and

Operators

In Figures 13 and 14 we illustrate how $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ extensions could be incorporated in XACML by encoding the $\text{PTaCL}_{\mathsf{4}}^{\leqslant}$ decisions and $\mathbin{\otimes_{\rm b}}$ operator using the syntax of the XACML standard.