auth-toy.agda

module auth where

open import Data.String
open import Level



data AsDelegate : Set where
     IsDelegate : AsDelegate
     IsLeaf : AsDelegate
open AsDelegate

data OnBehalfOf : String -> String -> AsDelegate -> Set where
  Self : { x : String } ->  OnBehalfOf x x IsDelegate
  DelegatedTo : {root mid : String} -> (end : String) -> OnBehalfOf mid root IsDelegate -> OnBehalfOf end root IsDelegate
  LeafAuth : {root mid : String} -> (end : String) -> OnBehalfOf mid root IsDelegate -> OnBehalfOf end root IsLeaf


{-
equivalent datalog would be (roughly)

onBehalfOf(me,me,Delegate).
onBehalfOf(agent,originalPerson,Delegate) :- onBehalfOf(mid,originalPerson,Delegate),AddsDelegateFor(mid,originalperson,agent)
onBhealfOf(leafAgent,originalPerson,LEAF) :- onBehalfOf(mid,originalPerson,Delegate),AddsLeafFor(mid,originalperson,leafAgent)

-}