{-| 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