owned this note
owned this note
Published
Linked with GitHub
$\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\grant}{\mathtt{grant}}
\newcommand{\deny}{\mathtt{deny}}
\newcommand{\ifrule}{\mathtt{if}}
\newcommand{\elserule}{\mathtt{else}}
\newcommand{\cond}{cond}
\newcommand{\guard}{guard}
\newcommand{\undefined}{\mathtt{undef}}
\newcommand{\conflict}{\mathtt{conflict}}
\newcommand{\decision}[1]{\mathtt{decision}\!\left({#1}\right)}
\newcommand{\dec}{dec}
\newcommand{\policy}{pol}
\newcommand{\eval}{\mathtt{eval}}
\newcommand{\casepolicy}{\mathtt{case}}
\newcommand{\goc}[1]{\mathsf{GoC}(\vphantom{g_{-}}{#1})}
\newcommand{\doc}[1]{\mathsf{DoC}(\vphantom{g_{-}}{#1})}
\newcommand{\gobl}[1]{\mathsf{GObl}(\vphantom{g_{-}}{#1})}
\newcommand{\dobl}[1]{\mathsf{DObl}(\vphantom{g_{-}}{#1})}
\newcommand{\TrueGuard}[1]{\mathsf{T}(\vphantom{g_{-}}{#1})}
\newcommand{\ReachGuard}[1]{\mathsf{R}(\vphantom{g_{-}}{#1})}
\newcommand{\obligation}[3]{\mathsf{oblg}(\vphantom{g_{-}}{#1},\,{#2},\,{#3})}
\newcommand{\obligationguard}[3]{\mathsf{oblg'}(\vphantom{g_{-}}{#1},\,{#2},\,{#3})}
\newcommand{\dand}{\;\&\&\;}
\newcommand{\dor}{\;||\;}
\newcommand{\accesscontrolname}{\textsf{FROST}}
\newcommand{\mergepol}{\mathtt{join}}
\newcommand{\refast}[1]{(\ast_{#1})}$
:::info
Latest update: 04.01.2019
:::
# Compilation of Policies with Obligations
The focus of this document is on the description and illustration of the compilation of an example policy with obligations into the respective circuits, also under incomplete information. Starting from the $\accesscontrolname{}$ language and the compilation rules of the yellow paper, JSON code is used to represent the circuits of the intermediate language. Hence, the example is quite simplified to avoid bloating the derivation steps and the JSON code, but nevertheless an instance of every part of the $\accesscontrolname{}$ language's grammar ($\dec,\, term,\, \cond,\, rule,\, \guard,\,$ $\policy,\, obl$) is represented.
**Documents**
- [Revisions to the Policy Language](https://hackmd.io/b8uIzrcMRsmNU3Wa8Z924w)
- [Term and Attribute Language](https://hackmd.io/QBb2HDjcRu-MOOGnqOD1BA)
- [Test vectors for EPIC use cases](https://hackmd.io/r8hnR8daRmy596FMdSoK-Q)
- [Intermediate Language](https://hackmd.io/_TtM9qoQTxuXtdaE6uE4Jg)
- [JSON syntax documentation](https://hackmd.io/HxW7d_XBStaSE_5PBEZfSg)
- [Properties of Obligations](https://hackmd.io/1Jq4sTXQRES46THhvKq0jg)
| Author(s) | Year | Title |
|:-:|:-:|:-|
| Xain | '18 | The $\accesscontrolname{}$ Language v0.8.1 |
| Xain | '18 | Evaluating $\accesscontrolname{}$ Policies Under Incomplete Information |
**Contents**
- [Compilation of Policies with Obligations](#Compilation-of-Policies-with-Obligations)
- [Example Policy in the $\accesscontrolname{}$ language](#Example-Policy-in-the-accesscontrolname-Language)
- [Policy Compilation](#Policy-Compilation)
- [$\goc{\cdot}$ Policy Compilation](#goccdot-Policy-Compilation)
- [$\doc{\cdot}$ Policy Compilation](#doccdot-Policy-Compilation)
- [Simplification of Policy Circuits](#Simplification-of-Policy-Circuits)
- [Obligation Compilation](#Obligation-Compilation)
- [$\gobl{\cdot}$ Obligation Compilation](#goblcdot-Obligation-Compilation)
- [$\dobl{\cdot}$ Obligation Compilation](#doblcdot-Obligation-Compilation)
- [Simplification of Obligation Circuits](#Simplification-of-Obligation-Circuits)
- [Incomplete Information for Policy and Obligation Circuits](#Incomplete-Information-for-Policy-and-Obligation-Circuits)
- [Binary Decision Diagrams](#Binary-Decision-Diagrams)
- [Another Example Policy in the $\accesscontrolname{}$ Language and its Compilation](#Another-Example-Policy-in-the-accesscontrolname-Language-and-its-Compilation)
- [$\goc{\cdot}$ Policy Compilation and Simplification](#goccdot-Policy-Compilation-and-Simplification)
- [$\doc{\cdot}$ Policy Compilation and Simplification](#doccdot-Policy-Compilation-and-Simplification)
## Example Policy in the $\accesscontrolname{}$ Language
First, we define a policy $p$ which grants on the fulfillment of a simple condition, which is that the requesting subject needs to be the resource owner, and has the obligation to write to a log when granting:
\begin{align*}
p = \grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})
\end{align*}
```haskell
p = GrantIf (Const Subj =*= Entity "owner") ["log_event"]
```
where the former is written in the $\accesscontrolname{}$ language and the latter is the corresponding Haskell notation of the $\accesscontrolname{}$ language. Then this policy $p$ is embedded into a policy $q$ that behaves like a deny-by-default:
\begin{align*}
q = \casepolicy\,\{\, [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \,\}
\end{align*}
```haskell
q = case [(p `Eval` Grant, p)] (Truth, Deny)
```
The example policy $q$ covers the full set of grammatical clauses of the $\accesscontrolname{}$ language:
| $\accesscontrolname{}$ grammar | examples |
|:-|:-|
| decisions | $\grant$, $\deny$ |
| terms | $Subj$, $\text{"}owner\text{"}$ |
| conditions | $Subj == \text{"}owner\text{"}$ |
| rules | $\grant\ \ifrule\ (\ldots)$ |
| guards | $p\ \eval\ \grant$, $\true$ |
| policies | $\casepolicy\,\{\ldots\}$ |
| obligations | $\{ \text{"}log\_event\text{"} \}$ |
and this makes the example somewhat representative for the illustration of the compilation process.
Next, the policy $q$ and its associated obligation needs to be compiled into the respective circuits. Note that we wont apply any kind of simplification, like boolean identities, but we will merely follow the compilation rules in the sections [Policy compilation](#Policy-compilation) and [Obligation compilation](#Obligation-compilation). Simplification will be explained separately in the sections [Simplification of policy circuits](#Simplification-of-policy-circuits) and [Simplification of obligation circuits](#Simplification-of-obligation-circuits), as this is a supplementary functionality.
Thereafter we consider compilation of the policy and its obligation under incomplete information in section [Incomplete information for policy and obligation circuits](#Incomplete-information-for-policy-and-obligation-circuits) as well as efficient data structures for policy representations in section [Binary Decision Diagrams](#Binary-Decision-Diagrams).
Also, in section [Another Example Policy in the $\accesscontrolname{}$ Language and its Compilation](#Another-Example-Policy-in-the-accesscontrolname-Language-and-its-Compilation) we show another example to demonstrate the different outcomes of the compilation procedure, especially regarding the differences between the $\goc{\cdot}$ and $\doc{\cdot}$ circuits of non-trivial content.
## Policy Compilation
For the compilation of policies we follow the rules for $\goc{\policy}$ ("grant-or-conflict" for policies $\policy$), $\doc{\policy}$ ("deny-or-conflict" for policies $\policy$) and $\TrueGuard{\guard}$ ("is-true" for guards $\guard$) defined in the yellow paper and their corresponding formal definition in Haskell. For convenience, recall that the basic policy compilation rules for $\goc{\policy}$ are
\begin{align*}
\goc\grant &\;\equiv\; \true & \goc\deny &\;\equiv\; \false \\
\goc\conflict &\;\equiv\; \true & \goc\undefined &\;\equiv\; \false \\
\goc{\grant\ \ifrule\ \cond} &\;\equiv\; \cond & \goc{\deny\ \ifrule\ \cond} &\;\equiv\; \false
\end{align*}
as well as
\begin{align*}
\goc{\casepolicy\, \{\, [g_1\colon p_1]\, \ldots \, [g_{n-1}\colon p_{n-1}]\, [\true\colon p_n]\, \}} \;\equiv\; \left( \ReachGuard{g_1} \dand \goc{p_1} \right) \dor \cdots \\
\cdots \dor \left( \ReachGuard{g_{n-1}} \dand \goc{p_{n-1}} \right) \dor \left( \ReachGuard{\true} \dand \goc{p_n} \right)
\end{align*}
for the $\casepolicy$-clause. The basic policy compilation rules for $\doc{\policy}$ are
\begin{align*}
\doc\deny &\;\equiv\; \true & \doc\grant &\;\equiv\; \false \\
\doc\conflict &\;\equiv\; \true & \doc\undefined &\;\equiv\; \false \\
\doc{\deny\ \ifrule\ \cond} &\;\equiv\; \cond & \doc{\grant\ \ifrule\ \cond} &\;\equiv\; \false
\end{align*}
as well as
\begin{align*}
\doc{\casepolicy\, \{\, [g_1\colon p_1]\, \ldots \, [g_{n-1}\colon p_{n-1}]\, [\true\colon p_n]\, \}} \;\equiv\; \left( \ReachGuard{g_1} \dand \doc{p_1} \right) \dor \cdots \\
\cdots \dor \left( \ReachGuard{g_{n-1}} \dand \doc{p_{n-1}} \right) \dor \left( \ReachGuard{\true} \dand \doc{p_n} \right)
\end{align*}
for the $\casepolicy$-clause. The additional guard compilation rules for $\ReachGuard{\guard}$ and $\TrueGuard{\guard}$ are
\begin{align*}
\ReachGuard{g_1} &\;\equiv\; \TrueGuard{g_1} \\
\forall\; 1<i<n :\quad \ReachGuard{g_i} &\;\equiv\; \lnot\TrueGuard{g_1} \dand \ldots \dand \lnot\TrueGuard{g_{i-1}} \dand \TrueGuard{g_i} \\
\ReachGuard{\true} &\;\equiv\; \lnot\TrueGuard{g_1} \dand \ldots \dand \lnot\TrueGuard{g_{n-1}} \\[0.75em]
\TrueGuard\true &\;\equiv\; \true \\
\TrueGuard{g_1 \dand g_2} &\;\equiv\; \TrueGuard{g_1} \dand \TrueGuard{g_2} \\
\TrueGuard {\policy\ \eval\ \conflict} &\;\equiv\; \hphantom{\lnot}\goc\policy \dand \hphantom{\lnot}\doc\policy \\
\TrueGuard {\policy\ \eval\ \deny} &\;\equiv\; \lnot\goc\policy \dand \hphantom{\lnot}\doc\policy \\
\TrueGuard {\policy\ \eval\ \grant} &\;\equiv\; \hphantom{\lnot}\goc\policy \dand \lnot\doc\policy \\
\TrueGuard {\policy\ \eval\ \undefined} &\;\equiv\; \lnot\goc\policy \dand \lnot\doc\policy
\end{align*}
and note that these compilation rules for $\goc{\policy}$, $\doc{\policy}$ and $\TrueGuard{\guard}$ are mutually recursive.
To give an illustration of the steps that get carried out during compilation from the $\accesscontrolname{}$ language into the intermediate language, we will give a step-by-step description in a shorthand mathematical notation and describe the main steps in the JSON representation of the circuits.
### $\goc{\cdot}$ Policy Compilation
The $\goc{q}$ compilation of policy $q$ starts with
\begin{align*}
\goc{q} &= \goc{ \casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \} } \\
&= \left( \ReachGuard{p\ \eval\ \grant} \dand \goc{p} \right) \dor \left( \ReachGuard{\true} \dand \goc{\deny} \right)
\end{align*}
Compiling the several subterms yield
\begin{align*}
\ReachGuard{p\ \eval\ \grant} &= \TrueGuard{p\ \eval\ \grant} = \goc{p} \dand \lnot\doc{p} \\[0.5em]
\ReachGuard{\true} &= \lnot\TrueGuard{p\ \eval\ \grant} = \lnot\left( \goc{p} \dand \lnot\doc{p} \right) \\[0.5em]
\goc{\deny} &= \false
\end{align*}
and plugging this in we get
\begin{align*}
\goc{q} &= \left( \goc{p} \dand \lnot\doc{p} \dand \goc{p} \right) \dor \left( \lnot\! \left( \goc{p} \dand \lnot\doc{p} \right) \dand \false \right)
\end{align*}
At this state, the boolean circuit consists of conjunctions, disjunctions and negations of Boolean constants as well as the circuits for the policy $p$. The policy $p$ in turn compiles into
\begin{align*}
\goc{p} &= \goc{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})} \\
&= \left( Subj == \text{"}owner\text{"} \right) \\[0.5em]
\doc{p} &= \doc{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})} \\
&= \false
\end{align*}
and plugging this in yields
\begin{align*}
\goc{q} &= \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \dand \left( Subj == \text{"}owner\text{"} \right) \right) \dor \\
&\qquad \left( \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \right) \dand \false \right)
\end{align*}
Note that this compilation ignores any obligations which will be handled by different compilation rules later on.
This Boolean circuit is called `policy_goc` in the JSON representation and is part of the `policy_object`. The JSON notation employs the usual `and`, `or` and `not` statements with the following syntax:
```json
{
"operation": "and",
"attribute_list": [
// 1st and-argument
{
...
},
...
// Nth and-argument
{
...
}
]
}
```
```json
{
"operation": "or",
"attribute_list": [
// 1st or-argument
{
...
},
...
// Nth or-argument
{
...
}
]
}
```
```json
{
"operation": "not",
"attribute_list": [
// not-argument
{
...
}
]
}
```
Also, we make some assumptions about the types, e.g. that the resource owner possesses a public-private elliptic-curve key-pair and that the `request_object` is parsed in a way that enables us to access its values via the dot-notation of the attribute language. All values in the JSON notation are strings to provide a unified type-value pair approach to be interpreted by the calling language, even though this could be changed to employ the number and Boolean primitives of JSON.
Then the circuit for $\goc{q}$ can be stated as
```json
"policy_goc": {
"operation": "or",
"attribute_list": [
// 1st or-term: (subj==owner) && not(f) && (subj==owner)
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 3rd and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
// end of and
]
},
// 2nd or-term: not((subj==owner) && not(f)) && f
{
"operation": "and",
"attribute_list": [
// 1st and-term: not((subj==owner) && not(f))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
// end of and
]
}
]
},
// 2nd and-term: f
{
"type": "Boolean",
"value": "false"
}
// end of and
]
}
// end of or
]
}
```
### $\doc{\cdot}$ Policy Compilation
The $\doc{q}$ compilation of policy $q$ proceeds in a similar way and we only state the abbreviated compilation process and the corresponding JSON circuit `policy_doc` below:
\begin{align*}
\doc{q} &= \doc{ \casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \} } \\
&= \left( \ReachGuard{p\ \eval\ \grant} \dand \doc{p} \right) \dor \left( \ReachGuard{\true} \dand \doc{\deny} \right) \\
&= \left( \goc{p} \dand \lnot\doc{p} \dand \doc{p} \right) \dor \\
&\qquad \left( \lnot\! \left( \goc{p} \dand \lnot\doc{p} \right) \dand \true \right) \\
&= \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \dand \false \right) \dor \\
&\qquad \left( \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \right) \dand \true \right)
\end{align*}
and
```json
"policy_doc": {
"operation": "or",
"attribute_list": [
// 1st or-term: (subj==owner) && not(f) && f
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 3rd and-term: f
{
"type": "Boolean",
"value": "false"
}
// end of and
]
},
// 2nd or-term: not((subj==owner) && not(f)) && t
{
"operation": "and",
"attribute_list": [
// 1st and-term: not((subj==owner) && not(f))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
]
}
]
},
// 2nd and-term: t
{
"type": "Boolean",
"value": "true"
}
// end of and
]
}
// end of or
]
}
```
## Simplification of Policy Circuits
Obviously, the Boolean circuits above can be evaluated as they are, but evaluation will be much faster for simplified equivalent circuits. The simplification wants to exploit Boolean identities and will be done by a separate module and set of rules, therefore we just state manually simplified circuits and their derivation.
Simplification of $\goc{q}$ yields
\begin{align*}
\goc{q} &= \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \dand \left( Subj == \text{"}owner\text{"} \right) \right) \dor \\
&\qquad \left( \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \right) \dand \false \right) \\
&= \left( \left( Subj == \text{"}owner\text{"} \right) \dand \true \right) \dor \false \\
&= \left( Subj == \text{"}owner\text{"} \right)
\end{align*}
```json
"policy_goc": {
// subj==owner
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
```
and the simplification of $\doc{q}$ similarly yields
\begin{align*}
\doc{q} &= \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \dand \false \right) \dor \\
&\qquad \left( \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \right) \dand \true \right) \\
&= \false \dor \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \true \right) \\
&= \lnot\!\left( Subj == \text{"}owner\text{"} \right)
\end{align*}
```json
"policy_doc": {
// not(subj==owner)
"operation": "not",
"attribute_list": [
{
// subj==owner
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
}
```
## Obligation Compilation
For the compilation of obligations we follow the rules for $\obligation{\dec}{\policy}{\rho}$ ("obligations" for policies $\policy$ belonging to decisions $\dec$ in environments $\rho$) and $\obligationguard{\dec}{\guard}{\rho}$ ("obligations" for guards $\guard$ belonging to decisions $\dec$ in environments $\rho$) defined in the yellow paper and their corresponding formal definition in Haskell. For convenience, recall that the basic obligation compilation rules for $\obligation{\dec}{\policy}{\rho}$ are
\begin{align*}
\obligation{\dec}{\dec'}{\rho} &\;\equiv\; \{\,\} \\
\obligation{\dec}{\grant\, \{obl^*\}\ \ifrule\ \cond}{\rho} &\;\equiv\;
\begin{cases}
\{obl^*\} & \quad \text{if } \dec = \grant \text{ and } \rho\models\cond \\
\{\,\} & \quad \text{otherwise}
\end{cases} \\
\obligation{\dec}{\deny\, \{obl^*\}\ \ifrule\ \cond}{\rho} &\;\equiv\;
\begin{cases}
\{obl^*\} & \quad \text{if } \dec = \deny \text{ and } \rho\models\cond \\
\{\,\} & \quad \text{otherwise}
\end{cases} \\
\end{align*}
as well as
\begin{align*}
\obligation{\dec}{\casepolicy\, \{\, [g_1\colon p_1]\, \dots \, [g_{n-1}\colon p_{n-1}]\, [\true\colon p_n]\, \}}{\rho} \;\equiv\; \obligationguard{\dec}{g_i}{\rho} \cup \obligation{\dec}{p_i}{\rho}
\end{align*}
for the $\casepolicy$-clause, where $\rho\models\ReachGuard{g_i}$. The obligation compilation rules for $\obligationguard{\dec}{\guard}{\rho}$ are
\begin{align*}
\obligationguard{\dec}{\true}{\rho} &\;\equiv\; \{\,\} \\
\obligationguard{\dec}{\policy\ \eval\ \dec'}{\rho} &\;\equiv\;
\begin{cases}
\obligation{\dec}{\policy}{\rho} & \quad \text{if } \dec = \dec' \\
\{\,\} & \quad \text{otherwise}
\end{cases} \\
\obligationguard{\dec}{g_1 \dand g_2}{\rho} &\;\equiv\; \obligationguard{\dec}{g_1}{\rho} \cup \obligationguard{\dec}{g_2}{\rho}
\end{align*}
and note that these compilation rules for $\obligation{\dec}{\policy}{\rho}$ and $\obligationguard{\dec}{\guard}{\rho}$ are mutually recursive.
To give an illustration of the steps that get carried out during compilation, we will give a step-by-step description in a shorthand mathematical notation and describe the main steps in the JSON representation of the circuits.
### $\gobl{\cdot}$ Obligation Compilation
The $\gobl{q} = \obligation{\grant}{q}{\rho}$ compilation of policy $q$ starts with
\begin{align*}
& \obligation{\grant}{q}{\rho} \\
& \quad = \obligation{\grant}{\casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \}}{\rho} \\
& \quad = \begin{cases}
\obligationguard{\grant}{p\ \eval\ \grant}{\rho} \cup \obligation{\grant}{p}{\rho} & \text{if } \ReachGuard{p\ \eval\ \grant} \\
\obligationguard{\grant}{\true}{\rho} \cup \obligation{\grant}{\deny}{\rho} & \text{if } \ReachGuard{\true}
\end{cases}
\end{align*}
Compiling the several subterms yield
\begin{align*}
\obligationguard{\grant}{p\ \eval\ \grant}{\rho} &= \obligation{\grant}{p}{\rho} \\
\obligationguard{\grant}{\true}{\rho} &= \{\,\} \\
\obligation{\grant}{\deny}{\rho} &= \{\,\}
\end{align*}
as well as
\begin{align*}
\ReachGuard{p\ \eval\ \grant} &= \TrueGuard{p\ \eval\ \grant} = \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false & \refast{1} \\
\ReachGuard{\true} &= \lnot\TrueGuard{p\ \eval\ \grant} = \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right) \dand \lnot\false \right) & \refast{2}
\end{align*}
and plugging this in we get
\begin{align*}
\obligation{\grant}{q}{\rho} &= \begin{cases}
\obligation{\grant}{p}{\rho} \cup \obligation{\grant}{p}{\rho} & \text{if } \refast{1} \\
\{\,\} \cup \{\,\} & \text{if } \refast{2}
\end{cases} \\
&= \begin{cases}
\obligation{\grant}{p}{\rho} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases}
\end{align*}
At this state, the circuit consists of conditionals and the circuit for the obligations for granting of policy $p$. The obligations $\gobl{p}$ for granting of policy $p$ in turn compile into
\begin{align*}
\obligation{\grant}{p}{\rho} &= \obligation{\grant}{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})}{\rho} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases}
\end{align*}
and plugging this in yields
\begin{align*}
\obligation{\grant}{q}{\rho} &= \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases}
\end{align*}
This Boolean circuit is called `obligation_grant` in the JSON representation and is part of the `policy_object`. Next to the usual `and`, `or` and `not` statements the JSON notation also employs the `if` clause with the following syntax:
```json
{
"operation": "if",
"attribute_list": [
// if-condition
{
...
},
// if-statement
{
...
},
// else-statement (optional)
{
...
}
]
}
```
Besides, the `case` clause with the following syntax may be employed for chained `if` clauses, since the former is not more expressive than the latter and each of them can be rephrased as the respective other:
```json
{
"operation": "case",
"attribute_list": [
// 1st condition
{
...
},
// 1st statement
{
...
},
...
// (N-1)th condition
{
...
},
// (N-1)th statement
{
...
},
// Nth condition (true)
{
...
},
// Nth statement (default statement)
{
...
}
]
}
```
For instance, the `if` clause might be more convenient for compiled $\grant/\deny\ \ifrule\ \cond$-policies and the `case` clause for compiled $\casepolicy$-policies. Obligation sets $\{ obl_1,\, \ldots,\, obl_N \}$ can be represented as lists in the JSON notation like
```json
"obligations": [
// 1st obligation
{
...
},
...
// Nth obligation
{
...
}
]
```
Also see the document [Properties of Obligations](https://hackmd.io/1Jq4sTXQRES46THhvKq0jg) for different kinds of representation of obligations, especially the section on [Generalized Policy Objects](https://hackmd.io/1Jq4sTXQRES46THhvKq0jg#Generalized-Policy-Objects).
We make the same assumptions about types and attribute accessibility as for the policy circuits, then the circuit for $\gobl{q}$ can be stated as
```json
"obligation_grant": {
"operation": "case",
"attribute_list": [
// 1st case-condition: (*1)
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
// end of and
]
},
// 1st case-statement: if-statement
{
"operation": "if",
"attribute_list": [
// if-condition: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// if-statement: ``log_event`` obligation list
{
"obligations": [
{
"type": "Obligation",
"value": "log_event"
}
]
},
// else-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
// end of if
]
},
// 2nd-case-condition: (*2)
{
"operation": "and",
"attribute_list": [
// 1st and-term: not((subj==owner) && not(f))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
// end of and
]
}
]
},
// 2nd and-term: t
{
"type": "Boolean"
"value": "true"
}
// end of and
]
},
// 2nd case-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
// end of case
]
}
```
### $\dobl{\cdot}$ Obligation Compilation
The $\dobl{q} = \obligation{\deny}{q}{\rho}$ compilation of policy $q$ proceeds in a similar way and we only state the abbreviated compilation process and the corresponding JSON circuit `obligation_deny` below:
\begin{align*}
& \obligation{\deny}{q}{\rho} \\
& \quad = \obligation{\deny}{\casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \}}{\rho} \\
& \quad = \begin{cases}
\obligationguard{\deny}{p\ \eval\ \grant}{\rho} \cup \obligation{\deny}{p}{\rho} & \text{if } \ReachGuard{p\ \eval\ \grant} \\
\obligationguard{\deny}{\true}{\rho} \cup \obligation{\deny}{\deny}{\rho} & \text{if } \ReachGuard{\true}
\end{cases} \\
& \quad = \begin{cases}
\{\,\} \cup \obligation{\deny}{p}{\rho} & \text{if } \refast{1} \\
\{\,\} \cup \{\,\} & \text{if } \refast{2}
\end{cases} \\
& \quad = \begin{cases}
\obligation{\deny}{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})}{\rho} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases} \\
& \quad = \begin{cases}
\{\,\} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases}
\end{align*}
```json
"obligation_deny": {
"operation": "case",
"attribute_list": [
// 1st case-condition: (*1)
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
// end of and
]
},
// 1st case-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
},
// 2nd case-condition: (*2)
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(subj==owner && not(f))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// 2nd and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
}
// end of and
]
}
]
},
// 2nd and-term: t
{
"type": "Boolean"
"value": "true"
}
// end of and
]
},
// 2nd case-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
// end of case
]
}
```
## Simplification of Obligation Circuits
Obviously, the circuits above can be evaluated as they are, but evaluation will be much faster for simplified equivalent circuits. The simplification wants to exploit Boolean and conditional identities and will be done by a separate module and set of rules, therefore we just state manually simplified circuits and their derivation.
Simplification of $\obligation{\grant}{q}{\rho}$ yields
\begin{align*}
& \obligation{\grant}{q}{\rho} \\
&= \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases} \\
&= \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{cases} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \dand \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right) \dand \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \false \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases}
\end{align*}
```json
"obligation_grant": {
"operation": "if",
"attribute_list": [
// if-condition: subj==owner
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
},
// if-statement: ``log_event`` obligation list
{
"obligations": [
{
"type": "Obligation",
"value": "log_event"
}
]
},
// else-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
]
}
```
and the simplification of $\obligation{\deny}{q}{\rho}$ similarly yields
\begin{align*}
\obligation{\deny}{q}{\rho} &= \begin{cases}
\{\,\} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases} \\
&= \begin{cases}
\{\,\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{if } \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{cases} \\
&= \{\,\}
\end{align*}
```json
"obligation_deny": {
// empty obligation list
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
```
## Incomplete Information for Policy and Obligation Circuits
To evaluate policy circuits under incomplete information as in the technical note, we quote:
**Definition 3** (Partial Evaluation of Boolean Circuits). Let $\rho$ be a partial model. We may evaluate $\policy$ through its normal form and Kleene's strong 3-valued semantics as follows:
1. Evaluate $\goc\policy$ with Kleene's semantics to a truth value $v_{\mathsf{GoC}}$, which is $\true$, $\false$ or $\bot$.
2. Evaluate $\doc\policy$ with Kleene's semantics to a truth value $v_{\mathsf{DoC}}$, which is $\true$, $\false$ or $\bot$.
3. If $v_{\mathsf{GoC}}$ equals $\bot$, then we change the value of $v_{\mathsf{GoC}}$ to $\false$.
4. If $v_{\mathsf{DoC}}$ equals $\bot$, then we change the value of $v_{\mathsf{DoC}}$ to $\true$.
5. With these possibly overwritten values of $v_{\mathsf{GoC}}$ and $v_{\mathsf{DoC}}$, we compute the policy result as follows:
 $\bullet$ if both $v_{\mathsf{GoC}}$ and $v_{\mathsf{DoC}}$ are $\true$, return $\conflict$,
 $\bullet$ if both $v_{\mathsf{GoC}}$ and $v_{\mathsf{DoC}}$ are $\false$, return $\undefined$,
 $\bullet$ if $v_{\mathsf{GoC}}$ is $\true$ and $v_{\mathsf{DoC}}$ is $\false$, return $\grant$,
 $\bullet$ otherwise, return $\deny$.
Analogously, the calculation of obligations from policy circuits under incomplete information has to be adjusted and we quote the respective changes below:
**Definition 4** (Obligations from partially evaluated Boolean circuits). Let $\rho$ be a partial model. We may compute obligations for the partially evaluated policy through Kleene's strong 3-valued semantics as follows:
\begin{align*}
\obligation{\dec}{\grant\, \{obl^*\}\ \ifrule\ \cond}{\rho} &\;\equiv\;
\begin{cases}
\{obl^*\} & \quad \text{if } \dec = \grant \text{ and } \rho(\cond) = \true \\
\{\,\} & \quad \text{otherwise}
\end{cases} \\
\obligation{\dec}{\deny\, \{obl^*\}\ \ifrule\ \cond}{\rho} &\;\equiv\;
\begin{cases}
\{obl^*\} & \quad \text{if } \dec = \deny \text{ and } \rho(\cond) \in \{\true,\,\bot\} \\
\{\,\} & \quad \text{otherwise}
\end{cases} \\
\end{align*}
for the $rule$-clauses as well as
\begin{align*}
\obligation{\dec}{\casepolicy\, \{\, [g_1\colon p_1]\, \dots \, [g_{n-1}\colon p_{n-1}]\, [\true\colon p_n]\, \}}{\rho} \;\equiv\; \obligationguard{\dec}{g_i}{\rho} \cup \obligation{\dec}{p_i}{\rho}
\end{align*}
for the $\casepolicy$-clause, where $\rho\!\left(\overline{\ReachGuard{g_i}}\right) = \true$.
Here, $\overline{\ReachGuard{g}}$ denotes the evaluation of $\ReachGuard{g}$ under the application of the changes of Definition 3. That is to say, the truth value of guards $\policy\ \eval\ \dec$ is determined by computing the decision for $\policy$ as under Definition 3, and then we check equality of that result with $\dec$ in the usual 2-valued meaning of equations.
Since it holds from the previous sections that
\begin{align*}
\goc{p} &= (Subj == \text{"}owner\text{"}) & \doc{p} &= \false \\
\goc{q} &= (Subj == \text{"}owner\text{"}) & \doc{q} &= \lnot(Subj == \text{"}owner\text{"})
\end{align*}
we calculate the following 3-valued truth table and the resulting obligations table:
| $\rho(Subj == \text{"}owner\text{"})$ | $\goc{p}$ | $\doc{p}$ | $\goc{q}$ | $\doc{q}$ |
|:-:|:-:|:-:|:-:|:-:|
| $\true$ | $\true$ | $\false$ | $\true$ | $\false$ |
| $\false$ | $\false$ | $\false$ | $\false$ | $\true$ |
| $\bot$ | $\bot$ | $\false$ | $\bot$ | $\bot$ |
| $\rho(Subj == \text{"}owner\text{"})$ | $\text{computed decision}$ | $\gobl{q}$ | $\dobl{q}$ |
|:-:|:-:|:-:|:-:|
| $\true$ | $\grant$ | $\{\text{"}log\_event\text{"}\}$ | $\{\,\}$ |
| $\false$ | $\deny$ | $\{\,\}$ | $\{\,\}$ |
| $\bot$ | $\deny$ | $\{\,\}$ | $\{\,\}$ |
The first and second rows are the same as in the previous sections under a complete model, but the third row shows the evaluation under incomplete information. A detailed derivation of the obligations under the new compilation rules is shown below. The $\gobl{q}$ compilation of policy $q$ starts with
\begin{align*}
& \obligation{\grant}{q}{\rho} \\
& \quad = \obligation{\grant}{\casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \}}{\rho} \\
& \quad = \begin{cases}
\obligationguard{\grant}{p\ \eval\ \grant}{\rho} \cup \obligation{\grant}{p}{\rho} & \text{if } \overline{\ReachGuard{p\ \eval\ \grant}} = \true \\
\obligationguard{\grant}{\true}{\rho} \cup \obligation{\grant}{\deny}{\rho} & \text{if } \overline{\ReachGuard{\true}} = \true.
\end{cases}
\end{align*}
Before we used the shorthand notation "if $c$" for the conditional "if $c=\true$" when dealing with 2-valued truth semantics for some condition $c$, but now we will explicitly state the whole conditional to avoid any confusion in the 3-valued truth semantics. Therefore, we write "if $c=\true$" for the conditional checking whether $\rho(c)=\true$ and "if $c\neq\true$" for the conditional checking whether $\rho(c)\in\{false,\,\bot\}$, etc.
Compiling the several subterms yield
\begin{align*}
\obligationguard{\grant}{p\ \eval\ \grant}{\rho} &= \obligation{\grant}{p}{\rho} \\
\obligationguard{\grant}{\true}{\rho} &= \{\,\} \\
\obligation{\grant}{\deny}{\rho} &= \{\,\}
\end{align*}
as well as
\begin{align*}
\overline{\ReachGuard{p\ \eval\ \grant}} &= \overline{\TrueGuard{p\ \eval\ \grant}} & \\
&= \left( Subj == \text{"}owner\text{"} \right)\!\downarrow \dand \lnot\false & \refast{3} \\
\overline{\ReachGuard{\true}} &= \lnot\overline{\TrueGuard{p\ \eval\ \grant}} \dand \overline{\TrueGuard{\true}} & \\
&= \lnot\! \left( \left( Subj == \text{"}owner\text{"} \right)\!\downarrow \dand \lnot\false \right) \dand \true & \refast{4}
\end{align*}
where $c\!\downarrow$ and $c\!\uparrow$ denote the conversion of the value of a condition $c$ from $\bot$ to $\false$ and $\true$, respectively. Plugging this in we get
\begin{align*}
\obligation{\grant}{q}{\rho} &= \begin{cases}
\obligation{\grant}{p}{\rho} \cup \obligation{\grant}{p}{\rho} & \text{if } \refast{3} = \true \\
\{\,\} \cup \{\,\} & \text{if } \refast{4} = \true
\end{cases} \\
&= \begin{cases}
\obligation{\grant}{p}{\rho} & \text{if } \refast{3} = \true \\
\{\,\} & \text{if } \refast{4} = \true.
\end{cases}
\end{align*}
At this state, the circuit consists of conditionals and the circuit for the obligations for granting of policy $p$. The obligations $\gobl{p}$ for granting of policy $p$ in turn compile into
\begin{align*}
\obligation{\grant}{p}{\rho} &= \obligation{\grant}{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})}{\rho} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) = \true \\
\{\,\} & \text{otherwise}
\end{cases}
\end{align*}
and plugging this in yields
\begin{align*}
\obligation{\grant}{q}{\rho} &= \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) = \true \\
\{\,\} & \text{otherwise}
\end{cases} & \text{if } \refast{3} = \true \\
\{\,\} & \text{if } \refast{4} = \true.
\end{cases}
\end{align*}
We will only state simplified JSON circuits, therefore simplification of the above leads to
\begin{align*}
& \obligation{\grant}{q}{\rho} \\
&= \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) = \true \\
\{\,\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \neq \true
\end{cases} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{if } \lnot\! \left(\left( Subj == \text{"}owner\text{"} \right)\!\downarrow\right) = \true
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) = \true \dand \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \neq \true \dand \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{if } \lnot\! \left(\left( Subj == \text{"}owner\text{"} \right)\!\downarrow\right) = \true
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{if } \false \\
\{\,\} & \text{if } \lnot\! \left(\left( Subj == \text{"}owner\text{"} \right)\!\downarrow\right) = \true
\end{cases} \\
&= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{otherwise}.
\end{cases}
\end{align*}
Since we are now dealing with 2-valued circuits again, we can revert to shorthand notation for conditionals (the non-shorthand notation might sometimes be redundant at previous compilation steps as well, but this was maintained for the sake of clarity as mentioned before):
\begin{align*}
& \obligation{\grant}{q}{\rho}
= \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow \\
\{\,\} & \text{otherwise}.
\end{cases}
\end{align*}
We introduce two JSON idioms for the terms $c\!\downarrow$ and $c\!\uparrow$ called `indet2false` and `indet2true`, respectively. These can be expressed by `if`-clauses checking for 3-valued truth results and therefore don't expand the expressiveness of the language. They can also be equivalently expressed as $\lnot(c\!\downarrow) \equiv (\lnot c)\!\uparrow$ and $\lnot(c\!\uparrow) \equiv (\lnot c)\!\downarrow$ among themselves.
```json
{
"operation": "indet2false",
"attribute_list": [
// condition
{
...
}
]
}
```
```json
{
"operation": "indet2true",
"attribute_list": [
// condition
{
...
}
]
}
```
Then the JSON circuit `obligation_grant` for the simplified $\gobl{q}$ is
```json
"obligation_grant": {
"operation": "if",
"attribute_list": [
// if-condition: i2f(subj==owner)
{
"operation": "indet2false",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
},
// if-statement: ``log_event`` obligation list
{
"obligations": [
{
"type": "Obligation",
"value": "log_event"
}
]
},
// else-statement: empty obligation list
{
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
]
}
```
The $\dobl{q}$ compilation of policy $q$ proceeds in a similar way and we only state the abbreviated compilation process and the corresponding simplified JSON circuit `obligation_deny` below:
\begin{align*}
& \obligation{\deny}{q}{\rho} \\
& \quad = \obligation{\deny}{\casepolicy\, \{ [p\ \eval\ \grant \colon p] \, [\true \colon \deny] \}}{\rho} \\
& \quad = \begin{cases}
\obligationguard{\deny}{p\ \eval\ \grant}{\rho} \cup \obligation{\deny}{p}{\rho} & \text{if } \overline{\ReachGuard{p\ \eval\ \grant}} = \true \\
\obligationguard{\deny}{\true}{\rho} \cup \obligation{\deny}{\deny}{\rho} & \text{if } \overline{\ReachGuard{\true}} = \true
\end{cases} \\
& \quad = \begin{cases}
\{\,\} \cup \obligation{\deny}{p}{\rho} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} \cup \{\,\} & \text{if } \lnot\! \left(\left( Subj == \text{"}owner\text{"} \right)\!\downarrow\right) = \true
\end{cases} \\
& \quad = \begin{cases}
\obligation{\deny}{\grant\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}owner\text{"})}{\rho} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{if } \lnot\! \left(\left( Subj == \text{"}owner\text{"} \right)\!\downarrow\right) = \true
\end{cases} \\
& \quad = \begin{cases}
\{\,\} & \text{if } \left( Subj == \text{"}owner\text{"} \right)\!\downarrow = \true \\
\{\,\} & \text{otherwise}
\end{cases} \\
& \quad = \{\,\}
\end{align*}
```json
"obligation_deny": {
// empty obligation list
"obligations": [
{
"type": "Obligation",
"value": ""
}
]
}
```
## Binary Decision Diagrams
Employing Binary Decision Diagrams (BDDs; or to be more precize Reduced Ordered BDDs (ROBDDs)) we can derive a unique and minimal representation of the Boolean policy circuits (up to the ordering of the Boolean variables). Next to the constants $0$ for $\false$ and $1$ for $\true$ the only Boolean variable from $\goc{q}$ and $\doc{q}$ can be denoted as
\begin{align*}
x_1 \colon\; Subj == \text{"}owner\text{"}
\end{align*}
Rewriting both ciruits in terms of Boolean expressions yield
\begin{align*}
\goc{q} &= ( x_1 \land \lnot 0 \land x_1 ) \lor ( \lnot(x_1 \land \lnot 0) \land 1 \land 0 ) \\
\doc{q} &= (x_1 \land \lnot 0 \land 0) \lor (\lnot(x_1 \land \lnot 0) \land 1 \land 1)
\end{align*}
Hence, the corresponding BDDs calculated via the algorithms e.g. stated in [An Introduction to Binary Decision Diagrams](https://www.cmi.ac.in/~madhavan/courses/verification-2011/andersen-bdd.pdf) are
```graphviz
graph GoC {
0 [shape=box]
1 [shape=box]
x1 -- 0 [style=dashed]
x1 -- 1
}
```
for the circuit $\goc{q}$ and
```graphviz
graph DoC {
1 [shape=box]
0 [shape=box]
x1 -- 1 [style=dashed]
x1 -- 0
}
```
for the circuit $\doc{q}$. Here, the dashed edges denote the low/else branch and the solid edges denote the high/then branch of the if-then-else normal form (INF). When translated back from INF to other regular Boolean expression, we get exactly these terms of section [Simplification of Policy Circuits](#Simplification-of-Policy-Circuits) which were simplified manually.
\begin{align*}
x_1 \to 1,0 &\quad\equiv\quad \left( Subj == \text{"}owner\text{"} \right) \\
x_1 \to 0,1 &\quad\equiv\quad \lnot\! \left( Subj == \text{"}owner\text{"} \right)
\end{align*}
Abusing the notation of BDDs we can also derive minimal and unique circuits for $\gobl{q}$ and $\dobl{q}$. Next to the constants $0$ and $1$ and the Boolean variables $x_i,\, 1\leq i\leq n_b$, we introduce further constant variables for each obligation $o_i,\, 1\leq i\leq m$. Since $o_i$ are treated as constants the resulting BDD will have one or two terminal states
\begin{align*}
\left\{ o_i \right\}_{i \in \mathcal{I}_{\grant}} \qquad\qquad \text{and} \qquad\qquad \left\{ o_i \right\}_{i \in \mathcal{I}_{\deny}}
\end{align*}
which are lists of obligations and where the former can be identified with terminal $1$ and the latter with terminal $0$. Therefore, the same properties of common BDDs hold as well.
Note that the constant variables $o_i$ basically act like pointers, hence they can reference strings like in the example below or obligation policies from section [Generalized Policy Objects](https://hackmd.io/1Jq4sTXQRES46THhvKq0jg#Generalized-Policy-Objects) which in turn can be simplified with the BDD approach, too.
Regarding the obligation circuits $\gobl{q}$ and $\dobl{q}$ we denote by
\begin{align*}
x_1 &\colon\; Subj == \text{"}owner\text{"} \\
o_1 &\colon\; \text{"}log\_event\text{"} \\
o_2 &\colon\; \text{""}
\end{align*}
Then the circuit
\begin{align*}
\gobl{q} = \begin{cases}
\begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases}
\end{align*}
can be written as
\begin{align*}
\gobl{q} &= \refast{1} \to (x_1 \to o_1,o_2),(\refast{2} \to o_2,0) \\
&= \left( \vphantom{x_{-}} \refast{1} \land ((x_1 \land o_1) \lor (\lnot x_1 \land o_2)) \right) \lor \left( \vphantom{x_{-}} \lnot\refast{1} \land ((\refast{2} \land o_2) \lor (\lnot\refast{2} \land 0)) \right) \\
&= \left( \vphantom{x_{-}} (x_1 \land \lnot 0) \land ((x_1 \land o_1) \lor (\lnot x_1 \land o_2)) \right) \\
&\quad \lor \left( \vphantom{x_{-}} \lnot(x_1 \land \lnot 0) \land ((\lnot(x_1 \land \lnot 0) \land 1 \land o_2) \lor (\lnot(\lnot(x_1 \land \lnot 0) \land 1) \land 0)) \right)
\end{align*}
Treating $o_1,\ o_2$ as constants yields the BDD
```graphviz
graph GObl {
o2 [shape=box]
o1 [shape=box]
x1 -- o2 [style=dashed]
x1 -- o1
}
```
Similarly, the circuit
\begin{align*}
\dobl{q} = \begin{cases}
\{\,\} & \text{if } \refast{1} \\
\{\,\} & \text{if } \refast{2}
\end{cases}
\end{align*}
can be written as
\begin{align*}
\dobl{q} &= \refast{1} \to o_2,(\refast{2} \to o_2,0) \\
&= \left( \vphantom{x_{-}} \refast{1} \land o_2 \right) \lor \left( \vphantom{x_{-}} \lnot\refast{1} \land ((\refast{2} \land o_2) \lor (\lnot\refast{2} \land 0)) \right) \\
&= \left( \vphantom{x_{-}} x_1 \land \lnot 0 \land o_2 \right) \lor \left( \vphantom{x_{-}}\lnot(x_1 \land \lnot 0) \land ((\lnot(x_1 \land \lnot 0) \land 1 \land o_2) \lor (\lnot(\lnot(x_1 \land \lnot 0) \land 1) \land 0)) \right)
\end{align*}
which yields the BDD
```graphviz
graph DObl {
o2 [shape=box]
}
```
Note that even though the BDDs of $\goc{q}$ and $\gobl{q}$ are isomorphic, the BDDs of $\doc{q}$ and $\dobl{q}$ are not, which justifies the introduction of BDDs for obligation circuits.
When translated back from INF to other regular Boolean expression, we get exactly these terms of section [Simplification of Obligation Circuits](#Simplification-of-Obligation-Circuits) which were simplified manually.
\begin{align*}
x_1 \to o_1,o_2 &\quad\equiv\quad \begin{cases}
\{\text{"}log\_event\text{"}\} & \text{if } \left( Subj == \text{"}owner\text{"} \right) \\
\{\,\} & \text{otherwise}
\end{cases} \\
o_2 &\quad\equiv\quad \{\,\}
\end{align*}
Software packages for various languages (e.g. C, Haskell, Rust) can be found at this [tool list](https://github.com/johnyf/tool_lists/blob/master/bdd.md).
## Another Example Policy in the $\accesscontrolname{}$ Language and its Compilation
We define another example policy, in this case a more deny-focused policy, to show the differences in the compilation process of the $\goc{}$ and $\doc{}$ circuits.
Let $p$ be
\begin{align*}
p = \deny\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}unknown\text{"})
\end{align*}
the policy that denies whenever the requesting subject is not known to the resource (e.g. not on a locally stored public key list). Then this policy $p$ is embedded into a policy $q$ that behaves like a grant-by-default:
\begin{align*}
q = \casepolicy\,\{\, [p\ \eval\ \deny \colon p] \, [\true \colon \grant] \,\}
\end{align*}
To give an illustration of the steps that get carried out during compilation from the $\accesscontrolname{}$ language into the intermediate language, we will give a step-by-step description in a shorthand mathematical notation and describe the main steps in the JSON representation of the circuits, again according to the compilation rules recalled in section [Policy Compilation](#Policy-Compilation).
### $\goc{\cdot}$ Policy Compilation and Simplification
The $\goc{q}$ compilation of policy $q$ starts with
\begin{align*}
\goc{q} &= \goc{ \casepolicy\, \{ [p\ \eval\ \deny \colon p] \, [\true \colon \grant] \} } \\
&= \left( \ReachGuard{p\ \eval\ \deny} \dand \goc{p} \right) \dor \left( \ReachGuard{\true} \dand \goc{\grant} \right)
\end{align*}
Compiling the several subterms yield
\begin{align*}
\ReachGuard{p\ \eval\ \deny} &= \TrueGuard{p\ \eval\ \deny} = \lnot\goc{p} \dand \doc{p} \\
\ReachGuard{\true} &= \lnot\TrueGuard{p\ \eval\ \deny} = \lnot\!\left( \lnot\goc{p} \dand \doc{p} \right) \\
\goc{\grant} &= \true
\end{align*}
and plugging this in we get
\begin{align*}
\goc{q} &= \left( \lnot\goc{p} \dand \doc{p} \dand \goc{p} \right) \dor \\
&\qquad \left( \lnot\! \left( \lnot\goc{p} \dand \doc{p} \right) \dand \true \right)
\end{align*}
At this state, the boolean circuit consists of conjunctions, disjunctions and negations of Boolean constants as well as the circuits for the policy $p$. The policy $p$ in turn compiles into
\begin{align*}
\goc{p} &= \goc{\deny\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}unknown\text{"})} \\
&= \false \\
\doc{p} &= \doc{\deny\,\{\text{"}log\_event\text{"}\}\ \ifrule\ (Subj == \text{"}unknown\text{"})} \\
&= \left( Subj == \text{"}unknown\text{"} \right)
\end{align*}
and plugging this in yields
\begin{align*}
\goc{q} &= \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \dand \false \right) \dor \\
&\qquad \left( \lnot\! \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dand \true \right)
\end{align*}
Note that this compilation ignores any obligations which will be handled by different compilation rules. Denote by
\begin{align*}
\left( Subj == \text{"}unknown\text{"} \right) = \lnot\!\left( Subj == \text{"}known\text{"} \right)
\end{align*}
the negation of the unknown subjects. Then the Boolean circuit for $\goc{q}$ can be stated in JSON as
```json
"policy_goc": {
"operation": "or",
"attribute_list": [
// 1st or-term: not(f) && (subj==unknown) && f
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 2nd and-term: subj==unknown
{
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
},
// 3rd and-term: f
{
"type": "Boolean",
"value": "false"
}
// end of and
]
},
// 2nd or-term: not(not(f) && (subj==unknown)) && t && t
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(not(f) && (subj==unknown))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 2nd and-term: subj==unknown
{
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
}
// end of and
]
}
]
},
// 2nd and-term: t
{
"type": "Boolean",
"value": "true"
},
// 3rd and-term: t
{
"type": "Boolean",
"value": "true"
}
]
}
// end of or
]
}
```
Also, we state manually simplified circuits and their derivation.
Simplification of $\goc{q}$ yields
\begin{align*}
\goc{q} &= \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \dand \false \right) \dor \\
&\qquad \left( \lnot\! \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dand \true \right) \\
&= \false \dor \lnot\! \left( \true \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \\
&= \lnot\!\left( Subj == \text{"}unknown\text{"} \right)
\end{align*}
```json
"policy_goc": {
// not(subj==unknown)
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
```
### $\doc{\cdot}$ Policy Compilation and Simplification
The $\doc{q}$ compilation of policy $q$ proceeds in a similar way and we only state the abbreviated compilation process and the corresponding JSON circuit `policy_doc` below:
\begin{align*}
\doc{q} &= \doc{ \casepolicy\, \{ [p\ \eval\ \deny \colon p] \, [\true \colon \grant] \} } \\
&= \left( \ReachGuard{p\ \eval\ \deny} \dand \doc{p} \right) \dor \left( \ReachGuard{\true} \dand \doc{\grant} \right) \\
&= \left( \lnot\goc{p} \dand \doc{p} \dand \doc{p} \right) \dor \left( \lnot\! \left( \lnot\goc{p} \dand \doc{p} \right) \dand \false \right) \\
&= \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dor \\
&\qquad \left( \lnot\! \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dand \false \right)
\end{align*}
```json
"policy_doc": {
"operation": "or",
"attribute_list": [
// 1st or-term: not(f) && (subj==unknown) && (subj==unknown)
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 2nd and-term: subj==unknown
{
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
},
// 3rd and-term: subj==unknown
{
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
}
// end of and
]
},
// 2nd or-term: not(not(f) && (subj==unknown)) && f
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(not(f) && (subj==unknown))
{
"operation": "not",
"attribute_list": [
{
"operation": "and",
"attribute_list": [
// 1st and-term: not(f)
{
"operation": "not",
"attribute_list": [
{
"type": "Boolean",
"value": "false"
}
]
},
// 2nd and-term: subj==unknown
{
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
}
// end of and
]
}
]
},
// 2nd and-term: f
{
"type": "Boolean",
"value": "false"
}
// end of and
]
}
// end of or
]
}
```
Simplification of $\doc{q}$ yields
\begin{align*}
\doc{q} &= \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dor \\
&\qquad \left( \lnot\! \left( \lnot\false \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dand \false \right) \\
&= \left( \true \dand \left( Subj == \text{"}unknown\text{"} \right) \right) \dor \false \\
&= \left( Subj == \text{"}unknown\text{"} \right)
\end{align*}
```json
"policy_doc": {
// subj==unknown
"operation": "not",
"attribute_list": [
{
"operation": "eq",
"attribute_list": [
{
"type": "Ed25519",
"value": "0x1234..."
},
{
"type": "request.subject.type",
"value": "request.subject.value"
}
]
}
]
}
```