{-|

This module implements Disjunction Category labels.

A label consists on conjunctions of disjunctions of 
principals. Labels can be simply created by using the 
function 'singleton' (it creates a label with only one 
principal). Functions '(.\\\/.)' and '(.\/\\.)' create disjunction 
and conjunction of principals, respectively. To illustrate
the use of this functions, we have the following examples. 

>>> singleton "Alice"
[ Alice ]

>>> "Alice" .\/. "Bob"
[ Alice \/ Bob ]

>>> "Alice" .\/. ("Bob" ./\. "Carla")
[ Alice \/ Bob ] /\ [ Alice \/ Carla ]

A 'DCLabel' is simple two labels, one for confidentiality ('secrecy') 
and another one for integrity ('integrity'). DCLabels are created by 
function 'newDC', where the first argument is for secrecy and the second
one for integrity. 

>>> newDC (singleton "Alice") ("Bob" .\/. "Alice") 
S=[ Alice ] I=[ Bob \/ Alice ]

Given two 'DCLabel' it is possible to precisely compute the join 
and the meet by calling functions 'join' and 'meet', respectively. 

>>> join ( newDC (singleton "Alice") (singleton "Carla") ) (  newDC (singleton "Bob") (emptyLabel) ) 
S=[ Alice ] /\ [ Bob ] I=True

>>> meet ( newDC (singleton "Alice") (singleton "Bob") ) (  newDC (singleton "Carla") (singleton "Carla") )
S=[ Alice \/ Carla ] I=[ Bob ] /\ [ Carla ]

It is possible to compare if a 'DCLabel' is more restrictive than another one by
calling the function 'canflowto'. For instance,

>>> canflowto ( newDC (singleton "Bob") (emptyLabel) ) (newDC ("Alice" ./\. "Bob") (singleton "Carla"))
False

>>> canflowto ( newDC (singleton "Bob") (singleton "Carla") ) (newDC ("Alice" ./\. "Bob") (emptyLabel))
True

-}

module DCLabel.Trustworthy 

       ( -- Lattice
           Lattice (join, meet, top, bottom, canflowto)
         -- Label 
         , Label () 
         , Principal ()
         , principal
         , isPrincipal
         , labelToList
         -- DSL 
         , DisjunctionOf ( (.\/.) )  
         , ConjunctionOf ( (./\.) )
         , (<>)
         , singleton
         -- DC Label 
         , DCLabel()
         , integrityDC 
         , secrecyDC 
         , newDC
         -- Priviligies 
         , Priv() 
         , canflowto_p
         , own 
         , privToLabel
         , createPriv   -- Becareful where it is used
       )

where

import DCLabel.Lattice
import DCLabel.Core