auth-toy.agda

module auth where

open import Data.String
open import Data.Nat
open import Level
open import Data.Product
open import  Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as Het


-- SignedBy will be a magic built in type that requires type checker support
-- seems likely in practice that i'll need to have some singleton structures
record SignedBy {ℓ } (t : Set ℓ  ) ( identity : String )  : Set ℓ  where
  field
    val : t
    uniqueCounter : ℕ --- unique natural number th
    hashOfVal : ℕ   --- nat number thats a Cryptographically Strong Hash of the canonical serialization of val
    signature  : String --- signature of concatenation of
                       ---(hashfOfVal , uniqueCounter), using the public key denotated by identity





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


record TypeSing {ℓ : Level} { tau : Set ℓ } (v : tau) : Set ℓ  where
       field
         singVal : tau
         singIsSing : singVal ≡ v


record Pair {tx ty : Level} ( x : Set tx ) (y : Set ty ) : Set ( (tx Level.⊔ ty )) where
  constructor mkPair
  field
    one : x
    two : y

data OnBehalfOf : String -> String -> AsDelegate -> Set  where
  Self : { x : String } ->  OnBehalfOf x x IsDelegate
  DelegatedTo : {root mid : String} -> (end : String)
                -> SignedBy  (  (OnBehalfOf mid root IsDelegate) × (TypeSing  end) × TypeSing IsDelegate ) mid
                -> OnBehalfOf end root IsDelegate
  LeafAuth : {root mid : String} -> (end : String)
                       -> SignedBy (OnBehalfOf mid root IsDelegate × TypeSing end × TypeSing IsLeaf) mid
                       -> 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)
-}