This module implements a ``nano`

`, very simple, embedded domain specific
language to create `Label`

s and `Priv`

ilages from conjunctions of
principal disjunctions.

A 'Label'/'Priv' is created using the (`.\/.`

) and (`./\.`

) operators.
The disjunction operator (`.\/.`

) is used to create a category from
`Principal`

s, `String`

s, or a disjunctive sub-expression. For example:

p1 =`principal`

"p1" p2 =`principal`

"p2" p3 =`principal`

"p3" e1 = p1`.\/.`

p2 e2 = e1`.\/.`

"p4"

Similarly, the conjunction operator (`./\.`

) is used to create category-sets
from `Principals`

, `Strings`

, and conjunctive or disjunctive sub-expressions.
For example:

e3 = p1`.\/.`

p2 e4 = e1`./\.`

"p4"`./\.`

p3

*Note* that because a category consists of a disjunction of principals, and a
category set is composed of the conjunction of categories, (`.\/.`

) binds
more tightly than (`./\.`

).

Given two `Label`

s, one for secrecy and one for integrity, you can
create a `DCLabel`

with `newDC`

. And, similarly, given a `TCBPriv`

and `Priv`

you can create a new minted privilege with `newTCBPriv`

.

Consider the following, example:

l1 = "Alice"`.\/.`

"Bob"`./\.`

"Carla" l2 = "Alice"`./\.`

"Carla" dc1 =`newDC`

l1 l2 dc2 =`newDC`

"Deian" "Alice" pr =`createPrivTCB`

$`newPriv`

("Alice"`./\.`

"Carla")

where

dc1 = <{["Alice" ⋁ "Bob"] ⋀ ["Carla"]} , {["Alice"] ⋀ ["Carla"]}>

dc2 = <{["Deian"]} , {["Alice"]}>

`canflowto`

dc1 dc2 = False`canflowto_p`

pr dc1 dc2 = True