-- The basic notions to define an access control policy.

-- The objects having access to the system (persons, programs):
data Principal = Alice | Bob | Carol
 deriving (Eq,Show)

-- The resources of the system:
data Resource = PasswdFile | SalesDB | AccountingDB
 deriving (Eq,Show)

-- The action to be performed on resources:
data Action = Edit | View
 deriving (Eq,Show)

-- Results of authorization requests:
data Authorization = Grant | Deny
 deriving (Eq,Show)

-- Hierarchical categories to classify persons, roles, etc:
data Category = Administrative | Accounting | Sales
 deriving (Eq,Show)


-- Specification of authorization policy:

-- The categories contained in a given category:
subCats :: Category -> [Category]
subCats Administrative = [Accounting, Sales]
subCats Accounting     = []
subCats Sales          = []

-- The roles of principals: the categories associated to a principal:
roles :: Principal -> [Category]
roles Alice = [Administrative]
roles Bob   = [Sales]
roles Carol = [Accounting]

-- The permissions given for a category:
permits :: Category -> [(Action,Resource)]
permits Administrative = [(Edit, PasswdFile),   (View, PasswdFile)]
permits Accounting     = [(Edit, AccountingDB), (View, SalesDB)]
permits Sales          = [(Edit, SalesDB),      (View, AccountingDB)]

----------------------------------------------------------------------
-- Operation to compute authorizations for a given principal, action,
-- and resource. The authorization is granted if the principal
-- has (directly or indirectly) a role which permits the required
-- access.

auth :: Principal -> Action -> Resource -> Authorization
auth p a r | (a,r) `elem` concatMap permits (allCats (roles p)) = Grant
           | otherwise                                          = Deny
 where
  -- Transitive closure of categories w.r.t. subcategory relation
  allCats :: [Category] -> [Category]
  allCats []       = []
  allCats (c : cs) = c : allCats (subCats c ++ cs)

-- Functional programming: use this to check authorizations:
-- > auth Alice Edit SalesDB

-- Functional logic programming: analyse control policies
--
-- Query: what is Alice allowed to Edit?
-- > solve $ auth Alice Edit r == Grant where r free
-- {r=PasswdFile} True
-- {r=SalesDB} True
-- {r=AccountingDB} True
--
-- Query: who can edit the SalesDB resource?
-- > solve $ auth p Edit SalesDB == Grant where p free
-- {p=Alice} True
-- {p=Bob} True

----------------------------------------------------------------------
-- We evolce the set of policies:

-- The Administrative is no longer allowed to take role Sales:
subCats' :: Category -> [Category]
subCats' Administrative = [Accounting]
subCats' Accounting     = []
subCats' Sales          = []

-- We parameterize the authorization operation over policy specifications:
authP :: (Category -> [(Action,Resource)])
      -> (Principal -> [Category])
      -> (Category -> [Category])
      -> Principal -> Action -> Resource -> Authorization
authP car pc cc p a r
  | (a,r) `elem` concatMap car (allCats (pc p)) = Grant
  | otherwise                                   = Deny
 where
  -- Transitive closure of categories w.r.t. subcategory relation
  allCats :: [Category] -> [Category]
  allCats []       = []
  allCats (c : cs) = c : allCats (cc c ++ cs)

-- auth = authP permits roles subCats
auth' :: Principal -> Action -> Resource -> Authorization
auth' = authP permits roles subCats'


-- What are the consequences of authorization changes w.r.t.
-- different policies?
diffAuth :: Principal -> Action -> Resource
         -> (Authorization,Authorization) -- (old auth, new auth)
diffAuth p a r
  | authP permits roles subCats  p a r == oldauth &&
    authP permits roles subCats' p a r == newauth && oldauth /= newauth
  = (oldauth, newauth)
 where oldauth,newauth free

-- Compare the changes between our two policies:
-- > diffAuth p a r where p,a,r free
-- {p=Alice, a=Edit, r=SalesDB} (Grant,Deny)
-- {p=Alice, a=View, r=AccountingDB} (Grant,Deny)