Compare commits

...

No commits in common. 'master' and 'idris' have entirely different histories.

  1. 1
      .gitginore
  2. 3
      .gitignore
  3. 2
      :old/Setup.hs
  4. 2
      :old/default.nix
  5. 7
      :old/hydra.nix
  6. 107
      :old/src/Yggdrasil/Adversarial.hs
  7. 98
      :old/src/Yggdrasil/Distribution.hs
  8. 135
      :old/src/Yggdrasil/ExecutionModel.hs
  9. 110
      :old/src/Yggdrasil/Functionalities.hs
  10. 73
      :old/src/Yggdrasil/HList.hs
  11. 105
      :old/src/Yggdrasil/MetaProtocol.hs
  12. 83
      :old/src/Yggdrasil/Nat.hs
  13. 65
      :old/stack.yaml
  14. 35
      :old/tests/ExecTests.hs
  15. 49
      :old/tests/FunctTests.hs
  16. 11
      :old/tests/Spec.hs
  17. 53
      :old/yggdrasil.cabal
  18. 13
      :old/yggdrasil.nix
  19. 8
      ChangeLog.md
  20. 93
      Data/Dag.idr
  21. 22
      README.md
  22. 118
      Yggdrasil/Distribution.idr
  23. 257
      Yggdrasil/Examples/SecureChannel.agda
  24. 22
      Yggdrasil/ExecutionModel.idr
  25. 37
      Yggdrasil/Extensible.idr
  26. 33
      Yggdrasil/List.agda
  27. 116
      Yggdrasil/Probability.agda
  28. 96
      Yggdrasil/Rational.agda
  29. 156
      Yggdrasil/Security.agda
  30. 375
      Yggdrasil/World.agda
  31. 2
      yggdrasil.agda-lib
  32. 11
      yggdrasil.ipkg
  33. BIN
      yggdrasil.jpg

1
.gitginore

@ -0,0 +1 @@
*.ibc

3
.gitignore

@ -0,0 +1,3 @@
/dist
/.stack-work
*.ibc

2
:old/Setup.hs

@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain

2
:old/default.nix

@ -0,0 +1,2 @@
{ pkgs ? import <nixpkgs> { } }:
pkgs.haskellPackages.callPackage ./yggdrasil.nix { }

7
:old/hydra.nix

@ -0,0 +1,7 @@
{ nixpkgs ? <nixpkgs> }:
let
pkgs = import nixpkgs { };
in {
yggdrasil = import ./default.nix { inherit pkgs; };
}

107
:old/src/Yggdrasil/Adversarial.hs

@ -0,0 +1,107 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Exposes type for reasoning about adversaries. Generally speaking, a
-- 'Functionality' may request interfaces from an 'Adversary', which need to be
-- supplied for it to run. The adversary also exposes some power to the
-- environment to arbitrarily control these interfaces. Functionalities should
-- be aware that the adversary may respond with anything correctly typed, and
-- is explicitly permitted to returning 'Nothing'. 'WithAdversary'' provides
-- an interface to repair unacceptable responses before the functionality
-- itself is called.
module Yggdrasil.Adversarial
( Adversary
, MaybeMap
, WithAdversary
, WithAdversary'(..)
, NoAdversary(..)
, DummyAdversary(..)
, CreateAdversarial(..)
) where
import Control.Arrow (second)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces, Operation,
Operations)
import Yggdrasil.HList (type (+|+), HList ((:::), Nil),
HSplit (hsplit))
-- | Maps a list of @'(in, out)@ type tuples to @'(in, 'Maybe' out)@.
type family MaybeMap (bs :: [(*, *)]) = (ys :: [(*, *)]) | ys -> bs where
MaybeMap '[] = '[]
MaybeMap ('( a, b) ': xs) = '( a, Maybe b) ': MaybeMap xs
-- | Allows construction of @[email protected] given a list of interfaces @[email protected] from the
-- adversary. The adversarial interfaces return 'Maybe's on all interfaces.
newtype WithAdversary s (ts :: [(*, *)]) b =
WithAdversary (HList (Interfaces s (MaybeMap ts)) -> b)
-- | Allows construction of a 'Functionality' with state @[email protected] and interface @[email protected]
-- whjen given a list of interfaces @[email protected] from the adversary. The adversarial
-- interface is corrected, by passing it through a filter ensuring valid
-- responses.
data WithAdversary' s c (as :: [(*, *)]) (bs :: [(*, *)]) =
WithAdversary' (HList (Interfaces s (MaybeMap as)) -> HList (Operations s c as))
(HList (Operations s c as) -> Functionality s c bs)
-- | An adversary is a functionality that exposes some interfaces to the
-- environment, and some interfaces returning 'Maybe's to some other party.
type Adversary s c as bs = Functionality s c (as +|+ MaybeMap bs)
-- | The empty adversary returns 'Nothing'.
class NoAdversary s (bs :: [(*, *)]) where
nullOperations :: HList (Operations s () (MaybeMap bs))
noAdversary :: Adversary s () '[] bs
noAdversary = Functionality () (nullOperations @s @bs)
instance NoAdversary s '[] where
nullOperations = Nil
instance NoAdversary s xs => NoAdversary s ('( a, b) ': xs) where
nullOperations = (\_ -> return Nothing) ::: nullOperations @s @xs
-- | A dummy adversary executes the interfaces the environments hands it.
class DummyAdversary s (bs :: [(*, *)]) where
operations ::
HList (Interfaces s (MaybeMap bs))
-> HList (Operations s () (MaybeMap bs))
dummyAdversary ::
HList (Interfaces s (MaybeMap bs)) -> Adversary s () '[] bs
dummyAdversary = Functionality () . operations @s @bs
instance DummyAdversary s '[] where
operations _ = Nil
instance DummyAdversary s bs => DummyAdversary s ('( a, b) ': bs) where
operations (b ::: bs) =
(lift . b :: Operation s () a (Maybe b)) :::
operations @s @bs bs
-- | Creates an adversarial functionality given a suitable adversary.
class CreateAdversarial s c as bs adv b where
createAdversarial ::
( HSplit (Interfaces s (as +|+ MaybeMap bs)) (Interfaces s as) (Interfaces s (MaybeMap bs))
, InterfaceMap s c (as +|+ MaybeMap bs)
)
=> Adversary s c as bs
-> adv
-> Action s (HList (Interfaces s as), b)
instance CreateAdversarial s c as bs (WithAdversary s bs b) b where
createAdversarial adv (WithAdversary f) = second f . hsplit <$> Create adv
instance CreateAdversarial s c as bs (WithAdversary' s c bs cs) (Functionality s c cs) where
createAdversarial adv (WithAdversary' g f) =
(\(a, b) -> (a, f (g b))) . hsplit <$> Create adv

98
:old/src/Yggdrasil/Distribution.hs

@ -0,0 +1,98 @@
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
-- | Provides primitives for high-level cryptographic sampling.
module Yggdrasil.Distribution
( Distribution
, DistributionT(DistributionT, runDistT)
, Sampler(..)
, liftDistribution
, coin
, uniform
) where
import Control.Monad (ap, (>=>))
import Control.Monad.Trans.Class (MonadTrans (lift))
import Crypto.Random (SystemDRG, randomBytesGenerate)
import Data.Bits ((.&.))
import qualified Data.ByteArray as B
import Data.Functor.Identity (Identity (Identity), runIdentity)
import Data.Maybe (fromJust)
-- | Allows randomly sampling elements of type @[email protected]
type Distribution = DistributionT Identity
-- | Allows randomly sampling elements of type @[email protected] in the context of monad @[email protected]
newtype DistributionT m b = DistributionT
{ runDistT :: forall s. Sampler s =>
s -> m (b, s)
}
instance Monad m => Functor (DistributionT m) where
fmap f x = pure f <*> x
instance Monad m => Applicative (DistributionT m) where
pure x = DistributionT $ pure . (x, )
(<*>) = ap
instance Monad m => Monad (DistributionT m) where
a >>= b = DistributionT $ runDistT a >=> (\(a', s') -> runDistT (b a') s')
instance MonadTrans DistributionT where
lift m = DistributionT $ \s -> (, s) <$> m
-- | Provides randomness.
class Sampler s
where
-- | Produce a bit of randomness.
sampleCoin :: s -> (Bool, s)
-- | Samples a distribution.
sample :: s -> DistributionT m b -> m (b, s)
sample s d = runDistT d s
-- | Samples a distribution, discarding the result randomness.
sample' :: Monad m => s -> DistributionT m b -> m b
sample' s d = fst <$> sample s d
instance Sampler SystemDRG where
sampleCoin s = (b .&. 1 == 1, s')
where
(ba :: B.Bytes, s') = randomBytesGenerate 1 s
-- fromJust is safe, as the array is not empty.
(b, _) = fromJust $ B.uncons ba
-- | Lifts a 'Distribution' to an arbitrary monadic 'DistributionT'.
liftDistribution :: Monad m => Distribution b -> DistributionT m b
liftDistribution d = DistributionT $ return . runIdentity . runDistT d
-- | Tosses a fair coin.
coin :: Distribution Bool
coin = DistributionT (Identity . sampleCoin)
-- | A uniform 'Distribution' over all elements of @[a]@.
uniform :: [a] -> Distribution a
uniform xs = do
let l = length xs
let lg = ilog2 l
n <- samplen lg
if n > l
then uniform xs
else return (xs !! n)
where
ilog2 :: Int -> Int
ilog2 1 = 0
ilog2 n
| n > 1 = ilog2 (n `div` 2) + 1
ilog2 _ = error "attempted non-postive logarithm"
samplen :: Int -> Distribution Int
samplen 0 = return 0
samplen lg
| lg > 0 = do
n' <- samplen (lg - 1)
c <- coin
return $
(n' * 2) +
if c
then 1
else 0
samplen _ = error "attempted to sample negative logarithm"

135
:old/src/Yggdrasil/ExecutionModel.hs

@ -0,0 +1,135 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Defines the basic model of execution for Yggdrasil. This is modelled
-- after, but not directly equal to, the
-- <https://eprint.iacr.org/2000/068 Universal Composability framework by Ran Canetti>.
--
-- Usage typically involves constructing a complex 'Action', and then 'run'ning
-- it.
module Yggdrasil.ExecutionModel
( Operation
, Action(Abort, Sample, Create, SecParam)
, Operations
, Interfaces
, Functionality(..)
, InterfaceMap(..)
, ForceSample(forceSample)
, run
) where
import Control.Monad (ap)
import Control.Monad.Fail (MonadFail (fail))
import Control.Monad.ST (ST, runST)
import Control.Monad.State.Lazy (StateT, runStateT)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.STRef (STRef, newSTRef, readSTRef,
writeSTRef)
import Yggdrasil.Distribution (Distribution, DistributionT (DistributionT, runDistT),
coin, liftDistribution)
import Yggdrasil.HList (HList ((:::), Nil))
-- | Describes what a node with internal state of type @[email protected] does when passed an
-- input of type @[email protected] by @Ref [email protected]
type Operation s c a b = a -> StateT c (Action s) b
-- | Given a list of tuples of input and output types, construct a
-- corresponding list of 'Operation' types.
type family Operations s c (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Operations s c '[] = '[]
Operations s c ('( a, b) ': xs) = Operation s c a b ': Operations s c xs
-- | Given a list of tuples of input and output types, construct a
-- corresponding list of 'Interface' types.
type family Interfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Interfaces s '[] = '[]
Interfaces s ('( a, b) ': xs) = (a -> Action s b) ': Interfaces s xs
-- | A functionality is a stateful node, with an initial state, and an
-- interface typed by a list of input/output type tuples, and defined through a
-- 'HList' of 'Operation's.
data Functionality s c ops =
Functionality c
(HList (Operations s c ops))
data SendRef s a b =
forall c. SendRef (STRef s c)
(Operation s c a b)
-- | Yggdrasil's version of 'IO'. Is self-contained, and can be opened with
-- 'run'.
data Action s b where
-- | Fail. This should be used over actual errors!
Abort :: Action s b
-- | Retrieves the security parameter of the running system.
SecParam :: Action s Int
-- | Samples from a distribution.
Sample :: Distribution b -> Action s b
Send :: SendRef s a b -> a -> Action s b
-- | Creates a new node from a functionality specification.
Create
:: InterfaceMap s c ops
=> Functionality s c (ops :: [(*, *)])
-> Action s (HList (Interfaces s ops))
Compose :: Action s c -> (c -> Action s b) -> Action s b
instance Functor (Action s) where
fmap f x = pure f <*> x
instance Applicative (Action s) where
pure = Sample . pure
(<*>) = ap
instance Monad (Action s) where
a >>= b = Compose a b
instance MonadFail (Action s) where
fail _ = Abort
-- | Simulates a world running an external action.
run :: (forall s. Action s b) -> DistributionT Maybe b
run a =
DistributionT $ \rng -> runST $ runMaybeT $ runDistT (run' a) rng
run' :: Action s b -> DistributionT (MaybeT (ST s)) b
run' Abort = DistributionT $ \_ -> MaybeT $ return Nothing
-- TODO: Make a parameter
run' SecParam = return 128
run' (Sample d) = liftDistribution d
run' (Send (SendRef (ptr :: STRef s c) op) msg) = do
c <- lift . lift $ readSTRef ptr
(b, c') <- run' (runStateT (op msg) c)
lift . lift $ writeSTRef ptr c'
return b
run' (Create (Functionality c ops)) = do
ptr <- lift . lift $ newSTRef c
return $ ifmap ptr ops
run' (Compose a f) = run' a >>= run' . f
-- | States we can create interfaces from operations. Implemented for all @[email protected]
class InterfaceMap s c (ts :: [(*, *)]) where
ifmap :: STRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)
instance InterfaceMap s c '[] where
ifmap _ Nil = Nil
instance InterfaceMap s c as => InterfaceMap s c ('( a, b) ': as) where
ifmap ref (x ::: xs) = Send (SendRef ref x) ::: ifmap ref xs
-- | States that we can forcibly sample from a type, such that with negligible
-- probabily there is a collision between samples.
class ForceSample t where
forceSample :: Action s t
instance ForceSample [Bool] where
forceSample = SecParam >>= (\sp -> sequence [Sample coin | _ <- [0 .. sp]])

110
:old/src/Yggdrasil/Functionalities.hs

@ -0,0 +1,110 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
-- | A collection of common functionalities, ready for use.
module Yggdrasil.Functionalities
( ROState
, SigState
, commonRandomString
, randomOracle
, signature
) where
import Control.Monad.State.Lazy (get, modify, put)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.Adversarial (WithAdversary' (WithAdversary'))
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
ForceSample (forceSample),
Functionality (Functionality),
Interfaces, Operation, Operations)
import Yggdrasil.HList (HList ((:::), Nil))
import Yggdrasil.Nat (Zn)
crsOp :: Distribution b -> Operation s (Maybe b) () b
crsOp d () =
get >>= \case
Just x -> return x
Nothing -> do
x <- lift $ Sample d
put $ Just x
return x
-- | A CRS functionality over a given distribution.
commonRandomString :: Distribution b -> Functionality s (Maybe b) '[ '( (), b)]
commonRandomString d = Functionality Nothing (crsOp d ::: Nil)
-- | The state of a 'randomOracle'. Consists of previously recorded
-- query/response pairs.
type ROState a b = [(a, b)]
roLookup :: Eq a => a -> ROState a b -> Maybe b
roLookup _ [] = Nothing
roLookup x' ((x, y):_)
| x == x' = Just y
roLookup x (_:xs) = roLookup x xs
roOp :: Eq a => Distribution b -> Operation s (ROState a b) a b
roOp d x =
(roLookup x <$> get) >>= \case
Just y -> return y
Nothing -> do
y <- lift $ Sample d
modify ((x, y) :)
return y
-- | A random oracle functionality, over a given distribution.
randomOracle ::
Eq a => Distribution b -> Functionality s (ROState a b) '[ '( a, b)]
randomOracle d = Functionality [] (roOp d ::: Nil)
-- | The state of a 'signature' functionality. Consists of previously recorded
-- signatures, and their corresponding messages and signers.
type SigState s n msg sig = [(Zn n, (msg, sig))]
verifyOp ::
(Eq msg, Eq sig) => Operation s (SigState s n msg sig) (Zn n, (msg, sig)) Bool
verifyOp s = (s `elem`) <$> get
fixAdv ::
(Eq msg, Eq sig, ForceSample sig)
=> HList (Interfaces s '[ '( (Zn n, msg), Maybe sig)])
-> HList (Operations s (SigState s n msg sig) '[ '( (Zn n, msg), sig)])
fixAdv (sign ::: Nil) = sign' ::: Nil
where
sign' (p, msg) = do
sig <-
lift (sign (p, msg)) >>= \case
Just s -> do
st <- get
if (p, (msg, s)) `elem` st
then forceSample' msg p
else return s
Nothing -> forceSample' msg p
modify ((p, (msg, sig)) :)
return sig
forceSample' msg p = do
sig <- lift forceSample
st <- get
-- This may recursive infinitely iff the signature space is too small!
-- This is a feature, not a bug.
if (p, (msg, sig)) `elem` st
then forceSample' msg p
else return sig
-- | A robust signature functionality.
signature ::
(Eq msg, Eq sig, ForceSample sig)
=> WithAdversary' s (SigState s n msg sig)
'[ '( (Zn n, msg), sig)]
'[ '( (Zn n, msg), sig)
, '( (Zn n, (msg, sig)), Bool)
]
signature =
WithAdversary'
fixAdv
(\(sign ::: Nil) -> Functionality [] (sign ::: verifyOp ::: Nil))

73
:old/src/Yggdrasil/HList.hs

@ -0,0 +1,73 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- | Provides heterogeneous lists through 'HList', as well as some type and
-- value level operations on them.
module Yggdrasil.HList
( HList(..)
, type (+|+)
, HAppend((+++))
, HSplit(hsplit)
, HSequence(hsequence)
, Applied
) where
infixr 5 :::
-- | A heterogeneous list.
data HList :: [*] -> * where
Nil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
-- | Type-level appending of lists.
type family (as :: [k]) +|+ (bs :: [k]) :: [k] where
'[] +|+ bs = bs
(a ': as) +|+ bs = a ': (as +|+ bs)
-- | Value-level appending of 'HList's.
class HAppend as bs where
(+++) :: HList as -> HList bs -> HList (as +|+ bs)
instance HAppend '[] bs where
_ +++ bs = bs
instance HAppend as bs => HAppend (a ': as) bs where
(a ::: as) +++ bs = a ::: (as +++ bs)
-- | Split a 'HList' at the value level given the type-level components.
class HSplit hs as bs where
hsplit :: HList hs -> (HList as, HList bs)
instance HSplit bs '[] bs where
hsplit bs = (Nil, bs)
instance HSplit hs as bs => HSplit (a ': hs) (a ': as) bs where
hsplit (h ::: hs) =
let (as, bs) = hsplit @hs @as @bs hs
in (h ::: as, bs)
type family Applied m (as :: [k]) = (ys :: [k]) | ys -> as where
Applied m '[] = '[]
Applied m (a ': as) = m a ': Applied m as
class HSequence m as where
hsequence :: HList (Applied m as) -> m (HList as)
instance Monad m => HSequence m '[] where
hsequence Nil = return Nil
instance (Monad m, HSequence m as) => HSequence m (a ': as) where
hsequence (a ::: as) = do
a' <- a
as' <- hsequence @m @as as
return (a' ::: as')

105
:old/src/Yggdrasil/MetaProtocol.hs

@ -0,0 +1,105 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
module Yggdrasil.MetaProtocol
( MetaProtocol
, RelayN
, npartyIdeal
, npartyReal
) where
import Control.Monad.State.Lazy (get, put)
import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces,
Operations)
import Yggdrasil.HList (HList ((:::), Nil),
HSequence (hsequence))
import Yggdrasil.Nat (ForEach, ForEach (foreach),
IdApplied (idApplied), NCopies, Zn)
type MetaProtocol s c c' ops ops'
= Functionality s c ops -> Functionality s c' ops'
class RelayN s n (ops :: [(*, *)]) where
relayNOperations ::
(HList (Interfaces s (WithZn n ops)))
-> Zn n
-> (HList (Operations s () ops))
relayN ::
(HList (Interfaces s (WithZn n ops))) -> Zn n -> Functionality s () ops
relayN is n = Functionality () (relayNOperations @s @n @ops is n)
instance RelayN s n '[] where
relayNOperations _ _ = Nil
instance RelayN s n xs => RelayN s n ('( a, b) ': xs) where
relayNOperations (f ::: xs) n = lift . f . (n, ) ::: relayNOperations @s @n @xs xs n
type family WithZn n (ops :: [(*, *)]) = (ys :: [(*, *)]) | ys -> ops where
WithZn n '[] = '[]
WithZn n ('( a, b) ': xs) = '( (Zn n, a), b) ': WithZn n xs
npartyIdeal ::
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, RelayN s n ops
, InterfaceMap s c (WithZn n ops)
, InterfaceMap s () ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
(WithZn n ops)
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyIdeal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ =
get >>= \case
Just i -> return i
Nothing -> do
f0 <- lift $ Create f
is <-
(lift .
hsequence . idApplied @(Action s) @n @(HList (Interfaces s ops)))
(foreach (\i -> Create (relayN @s @n @ops f0 i)))
put (Just is)
return is
npartyReal ::
forall s c n ops.
( ForEach n (Action s (HList (Interfaces s ops)))
, IdApplied (Action s) n (HList (Interfaces s ops))
, InterfaceMap s c ops
, HSequence (Action s) (NCopies n (HList (Interfaces s ops)))
)
=> MetaProtocol s c
(Maybe (HList (NCopies n (HList (Interfaces s ops)))))
ops
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyReal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ =
get >>= \case
Just i -> return i
Nothing -> do
is <-
(lift .
hsequence . idApplied @(Action s) @n @(HList (Interfaces s ops)))
(foreach (\_ -> Create f))
put (Just is)
return is

83
:old/src/Yggdrasil/Nat.hs

@ -0,0 +1,83 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Yggdrasil.Nat
( Nat
, Zero
, Succ
, NCopies
, Zn
, ForEach(foreach)
, IdApplied(idApplied)
, mkZn
, unZn
) where
import Data.Maybe (fromJust)
import Yggdrasil.HList (Applied, HList ((:::), Nil))
data Zero
data Succ n
class Nat n where
asInt :: Integral i => i
instance Nat Zero where
asInt = 0
instance Nat n => Nat (Succ n) where
asInt = asInt @n + 1
data Zn n =
Zn Integer
deriving (Eq, Show, Ord)
mkZn ::
forall n. Nat n
=> Integer
-> Maybe (Zn n)
mkZn x
| x < 0 = Nothing
| x > asInt @n = Nothing
| otherwise = Just (Zn x)
unZn :: Zn n -> Integer
unZn (Zn n) = n
promote :: Zn n -> Zn (Succ n)
promote (Zn n) = Zn n
type family NCopies n (a :: k) = (as :: [k]) | as -> n
--NCopies n (m a) = Applied m (NCopies n a)
where
NCopies Zero a = '[]
NCopies (Succ n) a = a ': NCopies n a
class ForEach n a where
foreach :: (Zn n -> a) -> HList (NCopies n a)
instance ForEach Zero a where
foreach _ = Nil
instance (Nat n, ForEach n a) => ForEach (Succ n) a where
foreach f =
f (fromJust (mkZn ((asInt @n) - 1))) ::: foreach @n @a (f . promote)
class IdApplied m n as where
idApplied :: HList (NCopies n (m as)) -> HList (Applied m (NCopies n as))
instance IdApplied m Zero as where
idApplied _ = Nil
instance IdApplied m n as => IdApplied m (Succ n) as where
idApplied (a ::: as) = a ::: idApplied @m @n @as as

65
:old/stack.yaml

@ -0,0 +1,65 @@
# This file was automatically generated by 'stack init'
#
# Some commonly used options have been documented as comments in this file.
# For advanced use and comprehensive documentation of the format, please see:
# https://docs.haskellstack.org/en/stable/yaml_configuration/
# Resolver to choose a 'specific' stackage snapshot or a compiler version.
# A snapshot resolver dictates the compiler version and the set of packages
# to be used for project dependencies. For example:
#
# resolver: lts-3.5
# resolver: nightly-2015-09-21
# resolver: ghc-7.10.2
# resolver: ghcjs-0.1.0_ghc-7.10.2
#
# The location of a snapshot can be provided as a file or url. Stack assumes
# a snapshot provided as a file might change, whereas a url resource does not.
#
# resolver: ./custom-snapshot.yaml
# resolver: https://example.com/snapshots/2018-01-01.yaml
resolver: lts-12.9
# User packages to be built.
# Various formats can be used as shown in the example below.
#
# packages:
# - some-directory
# - https://example.com/foo/bar/baz-0.0.2.tar.gz
# - location:
# git: https://github.com/commercialhaskell/stack.git
# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a
# subdirs:
# - auto-update
# - wai
packages:
- .
# Dependency packages to be pulled from upstream that are not in the resolver
# using the same syntax as the packages field.
# (e.g., acme-missiles-0.3)
# extra-deps: []
# Override default flag values for local packages and extra-deps
# flags: {}
# Extra package databases containing global packages
# extra-package-dbs: []
# Control whether we use the GHC we find on the path
# system-ghc: true
#
# Require a specific version of stack, using version ranges
# require-stack-version: -any # Default
# require-stack-version: ">=1.7"
#
# Override the architecture used by stack, especially useful on Windows
# arch: i386
# arch: x86_64
#
# Extra directories used by stack for building
# extra-include-dirs: [/path/to/dir]
# extra-lib-dirs: [/path/to/dir]
#
# Allow a newer minor version of GHC than the snapshot specifies
# compiler-check: newer-minor

35
:old/tests/ExecTests.hs

@ -0,0 +1,35 @@
{-# LANGUAGE ScopedTypeVariables #-}
module ExecTests
( spec
) where
import Crypto.Random (getSystemDRG)
import Data.Maybe (fromJust)
import Test.Hspec (Spec, describe, it, shouldBe)
import Test.Hspec.QuickCheck (prop)
import Yggdrasil.Distribution (sample', uniform)
import Yggdrasil.ExecutionModel (Action (Sample), run)
inSampleRange :: Int -> Bool
inSampleRange x = x > 4700 && x < 5300
sampleTest :: Action s Int
sampleTest = sampleTest' 10000
where
sampleTest' :: Int -> Action s Int
sampleTest' 0 = return 0
sampleTest' n = do
x <- sampleTest' (n - 1)
b <- Sample (uniform [0, 1])
return $ x + b
spec :: IO Spec
spec = do
rnd <- getSystemDRG
return $
describe "action" $ do
prop "obeys return" $ \(x :: String) ->
sample' rnd (run (return x)) == Just x
it "samples evenly" $
inSampleRange (fromJust $ sample' rnd (run sampleTest)) `shouldBe` True

49
:old/tests/FunctTests.hs

@ -0,0 +1,49 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module FunctTests
( spec
) where
import Crypto.Random (getSystemDRG)
import Test.Hspec (Spec, describe, it, shouldBe)
import Yggdrasil.Distribution (sample', uniform)
import Yggdrasil.ExecutionModel (Action (Create), run)
import Yggdrasil.Functionalities (commonRandomString, randomOracle)
import Yggdrasil.HList (HList ((:::), Nil))
crsSameTest :: Action s Bool
crsSameTest = do
(crsHandle ::: Nil) <-
Create $ commonRandomString (uniform [0 .. 10000 :: Int])
fst' <- crsHandle ()
snd' <- crsHandle ()
return (fst' == snd')
roSameTest :: Action s Bool
roSameTest = do
((roHandle :: Int -> Action s Int) ::: Nil) <-
Create $ randomOracle (uniform [0 .. 1000 :: Int])
fst' <- roHandle 1
snd' <- roHandle 1
return (fst' == snd')
roAllEqual :: Action s Bool
roAllEqual = do
((roHandle :: Int -> Action s Int) ::: Nil) <-
Create $ randomOracle (uniform [0 .. 1000 :: Int])
xs <- sequence [roHandle i | i <- [1 .. 1000]]
return $ all (== head xs) (tail xs)
spec :: IO Spec
spec = do
rnd <- getSystemDRG
return $ do
describe "common random string" $
it "returns the same value" $
sample' rnd (run crsSameTest) `shouldBe` Just True
describe "random oracle" $ do
it "returns the same for the same query" $
sample' rnd (run roSameTest) `shouldBe` Just True
it "is random with different queries" $
sample' rnd (run roAllEqual) `shouldBe` Just False

11
:old/tests/Spec.hs

@ -0,0 +1,11 @@
import Test.Hspec (hspec)
import qualified ExecTests
import qualified FunctTests
main :: IO ()
main = do
execTests <- ExecTests.spec
functTests <- FunctTests.spec
hspec execTests
hspec functTests

53
:old/yggdrasil.cabal

@ -0,0 +1,53 @@
name: yggdrasil
version: 0.1.0.0
synopsis: Executable specifications of composable cryptographic protocols.
description: Yggdrasil is a framework for writing executable
specification of composable cryptographic protocols. It is
modelled after Ran Canetti's Universal Composability
framework, although it departs from it in multiple places
to simplify the interface, and provide strong typing.
homepage: https://git.drwx.org/phd/yggdrasil
license: AGPL-3
license-file: LICENSE
author: Thomas Kerber
maintainer: [email protected]
category: Cryptography
build-type: Simple
extra-source-files: ChangeLog.md
cabal-version: >=1.10
source-repository head
type: git
location: https://git.drwx.org/phd/yggdrasil
library
exposed-modules: Yggdrasil.Adversarial
Yggdrasil.Distribution
Yggdrasil.ExecutionModel
Yggdrasil.Functionalities
Yggdrasil.HList
Yggdrasil.MetaProtocol
Yggdrasil.Nat
build-depends: base >= 4.11 && < 4.12
, cryptonite >= 0.25 && < 0.26
, memory >= 0.14 && < 0.15
, mtl >= 2.2 && < 2.3
, transformers >= 0.5 && < 0.6
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints
test-suite spec
type: exitcode-stdio-1.0
other-extensions: ScopedTypeVariables
default-language: Haskell2010
hs-source-dirs: tests
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints
main-is: Spec.hs
other-modules: ExecTests
FunctTests
build-depends: cryptonite
, base
, hspec
, QuickCheck
, yggdrasil

13
:old/yggdrasil.nix

@ -0,0 +1,13 @@
{ mkDerivation, base, cryptonite, hspec, memory, QuickCheck, stdenv
, transformers
}:
mkDerivation {
pname = "yggdrasil";
version = "0.1.0.0";
src = ./.;
libraryHaskellDepends = [ base cryptonite memory transformers ];
testHaskellDepends = [ base cryptonite hspec QuickCheck ];
homepage = "https://git.drwx.org/phd/yggdrasil";
description = "Executable specifications of composable security protocols";
license = stdenv.lib.licenses.agpl3;
}

8
ChangeLog.md

@ -0,0 +1,8 @@
# Revision history for yggdrasil
## 0.1.0.0 -- 2018-09-10
* Provide an UC-like, strictly typed execution model.
* Provide randomness distributions.
* Provide a typed model for arbitrary adversaries.
* Implement random oracles, crs, and signatures.

93
Data/Dag.idr

@ -0,0 +1,93 @@
module Data.Dag
%default total
%access public export
data Edge : Type -> Nat -> Type where
MkEdge : {n : Nat} -> (a, b : Nat) -> {auto pa : LT a b} ->
{auto pb : LT b n} -> c -> Edge c n
data Dag : Type -> Type -> Type where
MkDag : (ns : List a) -> List (Edge b (length ns)) -> Dag a b
nodes : Dag a b -> Nat
nodes (MkDag ns es) = length ns
edges : (d : Dag a b) -> List (Edge b (nodes d))
edges (MkDag _ es) = es
data DagEdge : (d : Dag a b) -> Edge b (Dag.nodes d) -> Type where
EZ : DagEdge (MkDag ns (e::es)) e
ES : DagEdge (MkDag ns es) e' -> DagEdge (MkDag ns (e::es)) e'
startsAt : Edge a n -> Nat
startsAt (MkEdge a b c) = a
endsAt : Edge a n -> Nat
endsAt (MkEdge a b c) = b
data Path : (d : Dag a b) -> Nat -> Nat -> Type where
Nil : {auto prf : LT n (nodes d)} -> Path d n n
(::) : (e : Edge b (nodes d)) -> {auto isEdge : DagEdge d e} ->
Path d n m -> {auto adjacent : Dag.endsAt e = n} ->
Path d (Dag.startsAt e) m
minusLTE : LTE (minus a b) a
minusLTE {a=Z} = LTEZero
minusLTE {a} {b=Z} = rewrite minusZeroRight a in lteRefl
minusLTE {a=S a} {b=S b} = lteSuccRight minusLTE
minusGTIsLT : GT a b -> {auto sml1 : LTE a n} -> {auto sml2 : LTE b n} ->
LT (n - a) (n - b)
minusGTIsLT {n=Z} {a=Z} {b=Z} gt impossible
minusGTIsLT {n=S n} {a=S a} {b=Z} _ = LTESucc (minusLTE {a=n} {b=a})
minusGTIsLT {n=S n} {a=S a} {b=S b} (LTESucc gt) {sml1=LTESucc sml1} {sml2=LTESucc sml2} =
minusGTIsLT gt
reversePreservesLength : (l : List a) -> length l = length (reverse l)
reversePreservesLength = reverseOntoPreservesLength []
where
reverseOntoPreservesLength : (acc : List a) -> (l : List a) ->
length acc + length l = length (reverseOnto acc l)
reverseOntoPreservesLength acc [] = plusZeroRightNeutral (length acc)
reverseOntoPreservesLength acc (x::xs) =
rewrite sym (plusSuccRightSucc (length acc) (length xs)) in
reverseOntoPreservesLength (x::acc) xs
||| Inverts paths in a dag. Each node at index n is mapped to index l - 1 - n.
invert : Dag a b -> Dag a b
invert (MkDag ns es) = MkDag (reverse ns)
(rewrite sym (reversePreservesLength ns) in (map invertE es))
where
invertE : Edge c n -> Edge c n
invertE (MkEdge {n=S n} a b {pa} {pb} c) =
let sml1 : LTE b n = fromLteSucc pb
sml2 : LTE a n = lteSuccLeft (lteTransitive pa sml1)
pa' : LT (minus n b) (minus n a) = minusGTIsLT pa
pb' : LT (minus n a) (S n) = LTESucc minusLTE
in MkEdge (minus n b) (minus n a) c
retain : Dag a b -> List Nat -> Dag a b
retain d = retain' d . sort
where
retain' : Dag a b -> List Nat -> Dag a b
retain' = ?retain
data DagView : Dag a b -> Dag a b -> Type where
MkView : (d : Dag a b) ->
(nlist : List Nat) ->
DagView d (retain d nlist)
pred : (d : Dag a b) -> (n : Nat) -> {auto prf : LT n (nodes d)} ->
(DPair (Dag a b) (\d' => DagView d d'))
pred d n = let l = filter (\m => isPred m n (edges d)) (count (nodes d))
in MkDPair (retain d l) (MkView d l)
where
count : Nat -> List Nat
count Z = []
count (S n) = n :: count n
isPred : {n : Nat} -> Nat -> Nat -> List (Edge c n) -> Bool
isPred n m [] = False
isPred n m (MkEdge a b _::es) = if n == a && m == b then True else isPred n m es

22
README.md

@ -0,0 +1,22 @@
# Yggdrasil
![Yggdrasil - The Mundane Tree](/phd/yggdrasil/raw/branch/master/yggdrasil.jpg)
Yggdrasil is a UC-based system for modelling security protocols.
## Not Asked Questions
Q: Why Idris?
A: Idris is both a dependently-typed programming language, and a theorem
prover, which comes with the territory of powerful type systems. The highly
generic type system allows yggdrasil to reason and prove statements about
highly generic protocols.
Q: Why AGPL?
A: AGPL is actually less strong than I'd like here, but stronger would be
unreasonable. I usually prefer permissive licenses, however it is crucial for
security protocols - and their implementation - to be available for public
scrutiny. If the use of AGPL results in one more protocol being made public, I
consider that a gain.

118
Yggdrasil/Distribution.idr

@ -0,0 +1,118 @@
module Yggdrasil.Distribution
import Control.Monad.Identity
import Data.Fin
import Data.QQ.SternBrocot
import Data.ZZ
import Yggdrasil.Extensible
%access public export
%default total
interface Sampler s where
sample : {n : Nat} -> s -> (Fin (S n), s)
data D : Type -> Type where
||| A value is a distribution.
PureD : a -> D a
||| Sample from Fin, where n >= 2
SampleD : {n : Nat} -> D (Fin (S (S n)))
||| Allow sampling depending on the value of a previous sample.
BindD : D a -> (a -> D b) -> D b
Functor D where
map f x = BindD x (PureD . f)
Applicative D where
pure = PureD
f <*> x = BindD f (\f' => BindD x (\x' => PureD (f' x')))
Monad D where
(>>=) = BindD
allFin : (n : Nat) -> List (Fin n)
allFin Z = []
allFin (S n) = FZ :: map FS (allFin n)
nzMultNzIsNz : {n : Nat} -> {m : Nat} -> LTE 1 n -> LTE 1 m -> LTE 1 (n * m)
nzMultNzIsNz {n=Z} _ _ impossible
nzMultNzIsNz {m=Z} _ _ impossible
nzMultNzIsNz {n=S n} {m=S m} _ _ = LTESucc LTEZero
nomDenomAdd : QPlus -> QPlus -> (ZZ, ZZ, Subset Nat (\x => GT x 0))
nomDenomAdd q1 q2 = let
(n1, d1) = extractQPlus q1;
(n2, d2) = extractQPlus q2;
a' = getWitness n1 * getWitness d2;
b' = getWitness n2 * getWitness d1 in
(Pos a', Pos b', Element (getWitness d1 * getWitness d2) (nzMultNzIsNz (getProof d1) (getProof d2)))
qplusMult : QPlus -> QPlus -> QPlus
qplusMult q1 q2 = let
(n1, d1) = extractQPlus q1;
(n2, d2) = extractQPlus q2;
n = getWitness n1 * getWitness n2;
d = getWitness d1 * getWitness d2 in
injectQPlus n d
(nzMultNzIsNz (getProof n1) (getProof n2))
(nzMultNzIsNz (getProof d1) (getProof d2))
mutual
Num QQ where
Zero + b = b
b + Zero = b
(Neg a) + (Neg b) = let (a, b, c) = nomDenomAdd a b in
(#) (negate (b + a)) (getWitness c) {dGtZ=getProof c}
(Neg a) + (Pos b) = let (a, b, c) = nomDenomAdd a b in
(#) (b - a) (getWitness c) {dGtZ=getProof c}
(Pos a) + (Pos b) = let (a, b, c) = nomDenomAdd a b in
(#) (a + b) (getWitness c) {dGtZ=getProof c}
(Pos a) + (Neg b) = let (a, b, c) = nomDenomAdd a b in
(#) (a - b) (getWitness c) {dGtZ=getProof c}
Zero * _ = Zero
_ * Zero = Zero
(Neg a) * (Neg b) = Pos (qplusMult a b)
(Neg a) * (Pos b) = Neg (qplusMult a b)
(Pos a) * (Neg b) = Neg (qplusMult a b)
(Pos a) * (Pos b) = Pos (qplusMult a b)
fromInteger i = fromInteger i # 1
Neg QQ where
negate Zero = Zero
negate (Pos q) = (Neg q)
negate (Neg q) = (Pos q)
a - b = a + (negate b)
data Event : (a -> Bool) -> D a -> QQ -> Type where
||| If `f x` is true, it's pure distribution has probability 1.
PureT : f a = True -> Event f (PureD a) (1 # 1)
||| If `f x` is false, it's pure distribution has probability 0.
PureF : f a = False -> Event f (PureD a) (0 # 1)
||| If we know the number of samples where `f x` is true,
NFin : length (filter f (allFin (S (S n)))) = m ->
Event f (SampleD {n=n}) (Pos m # S (S n))
CondBind : (f x = True -> Event g (bnd x) p1) ->
(f x = False -> Event g (bnd x) p2) ->
Event f d p3 ->
Event g (BindD d bnd) (p3 * p1 + (1 - p3) * p2)
data DualEvent : {d1 : D a} -> {d2 : D a} ->
(f : (a -> Bool)) ->
(p : QQ) ->
Event f d1 p ->
Event f d2 p ->
Type where
MkDual : (f : a -> Bool) ->
(p : QQ) ->
(e1 : Event f d1 p) ->
(e2 : Event f d2 p) ->
DualEvent f p e1 e2
infixr 5 $=
data ($=) : D a -> D a -> Type where
EEq : Eq a => ((x : a) -> DualEvent {d1=d1} {d2=d2} f p e1 e2) -> d1 $= d2
negligible : Nat -> QQ
negligible n = Pos (replicate n L)

257
Yggdrasil/Examples/SecureChannel.agda

@ -1,257 +0,0 @@
module Yggdrasil.Examples.SecureChannel where
open import Data.Bool using (Bool; true; false; if_then_else_; _∧_)
open import Data.List using (List; []; _∷_; any)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (_*_; zero; suc)
open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level; Lift; lift)
open import Relation.Binary.PropositionalEquality using (refl)
open import Yggdrasil.World
open import Yggdrasil.List
open import Yggdrasil.Security
open import Yggdrasil.Probability using (pure)
open Action↑
open Action↯
open WorldStates
πᵢ-SecureChannel : {ℓ : Level} → (M L : Set ℓ) → (M → L) → World ℓ
πᵢ-SecureChannel M L l = record
{ Γ = record
{ node = mknode (Maybe M) [] (mknquery L ⊤ ∷ [])
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → read) ∷
ncall M ⊤ (λ m → write (just m) >> query here (l m) >> return tt) ∷
[]
}
; Σ = stnode nothing []
}
πᵢ-AuthChannel : {ℓ : Level} → Set ℓ → World ℓ
πᵢ-AuthChannel M = record
{ Γ = record
{ node = mknode (Maybe M) [] (mknquery M ⊤ ∷ [])
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → read) ∷
ncall M ⊤ (λ m → write (just m) >> query here m >> return tt) ∷
[]
}
; Σ = stnode nothing []
}
πᵢ-PKE : {ℓ : Level} → (M C PK L : Set ℓ) → (M → L) → (PK → PK → Bool) →
(C → C → Bool) → World ℓ
πᵢ-PKE M C PK L l pk?= c?= = record
{ Γ = record
{ node = mknode (Maybe (PK × List (M × C))) []
(mknquery L C ∷ mknquery ⊤ PK ∷ [])
; adv = []
; hon =
ncall C (Maybe M) (λ c → read >>= λ
{ nothing → return nothing
; (just ⟨ _ , log ⟩) → return (in-log c log)
}) ∷
ncall (PK × M) (Maybe C) (λ{ ⟨ pk′ , m ⟩ → read >>= λ
{ nothing → return nothing
; (just ⟨ pk , log ⟩) → if pk?= pk pk′ then
query here (l m) >>=
(λ c → write (just ⟨ pk , ⟨ m , c ⟩ ∷ log ⟩) >>
return (just c)) else
return nothing
}}) ∷
ncall ⊤ PK (λ _ → query (there here) tt >>=
(λ pk → write (just ⟨ pk , [] ⟩) >> return pk)) ∷
[]
}
; Σ = stnode nothing []
}
where
in-log : C → List (M × C) → Maybe M
in-log c [] = nothing
in-log c (⟨ m , c′ ⟩ ∷ log) = if c?= c c′ then just m else in-log c log
πᵣ-SecureChannel : {ℓ : Level} → (M C PK L : Set ℓ) → (M → L) →
(PK → PK → Bool) → (C → C → Bool) → World ℓ
πᵣ-SecureChannel M C PK L l pk?= c?= = record
{ Γ = record
{ node = mknode (Maybe PK) (
World.Γ (πᵢ-PKE M C PK L l pk?= c?=) ∷
World.Γ (πᵢ-AuthChannel C) ∷
[])
[]
; adv = []
; hon =
ncall ⊤ (Maybe M) (λ _ → call↓ here (there here) tt >>= λ
{ nothing → return nothing
; (just c) → call↓ here here c
}) ∷
ncall M ⊤ (λ m → let
doSend = λ pk m → call↓ (there here) here ⟨ pk , m ⟩ >>= (λ
{ nothing → abort -- The public key we set was refused!
; (just c) → call↓ (there here) (there here) c
})
in read >>= λ
{ nothing → call↓ (there (there here)) here tt >>= (λ pk →
write (just pk) >> doSend pk m)
; (just pk) → doSend pk m
}) ∷
[]
}
; Σ = stnode nothing (
World.Σ (πᵢ-PKE M C PK L l pk?= c?=) ∷
World.Σ (πᵢ-AuthChannel C) ∷
[])
}
BitString : ∀ {ℓ} → Set ℓ
BitString {ℓ} = Lift ℓ (List Bool)
bitstring?= : ∀ {ℓ} → BitString {ℓ} → BitString {ℓ} → Bool
bitstring?= (lift []) (lift []) = true
bitstring?= (lift (_ ∷ _)) (lift []) = false
bitstring?= (lift []) (lift (_ ∷ _)) = false
bitstring?= {ℓ} (lift (true ∷ xs)) (lift (true ∷ ys)) = bitstring?= {ℓ} (lift xs) (lift ys)
bitstring?= {ℓ} (lift (false ∷ xs)) (lift (false ∷ ys)) = bitstring?= {ℓ} (lift xs) (lift ys)
bitstring?= (lift (true ∷ xs)) (lift (false ∷ ys)) = false
bitstring?= (lift (false ∷ xs)) (lift (true ∷ ys)) = false
_>>↯_ : ∀ {ℓ Σ Γᵢ Γᵣ A B hon-≡} → Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} A →
Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} B →
Action↯ {ℓ} Σ Γᵢ Γᵣ {hon-≡} B
α >>↯ β = α >>= (λ _ → β)
S-SecureChannel : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) →
Simulator (πᵢ-SecureChannel M L l) (πᵣ-SecureChannel M C PK L l pk?= c?=)
S-SecureChannel {ℓ} M C PK L l pk?= c?= = record
{ hon-≡ = refl
; state = Lift ℓ Bool
; initial = lift false
; call↯-map = λ
{ () here
; () (there here here)
; _ (there here (there () _))
; () (there (there here) here)
; _ (there (there here) (there () _))
; _ (there (there (there ())) _)
}
; query-map = λ
{ (path here here) l → read >>= let
perform-leak = query here (there here here) l >>= (λ c →
query here (there (there here) here) c)
in λ
-- 1. on the first leakage seen, query a π-PKE public key (ignore it).
-- 2. on *all* leakages seen, query a π-PKE ciphertext with the leakage
-- 3. finally, query a π-AuthChannel message, with the previous ciphertext.
{ (lift false) → query (there here) (there here here) tt >>↯ perform-leak
; (lift true) → perform-leak
}
; (path here (there ()))
; (path (there () _) _)
}
}
secure : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) → (m?= : M → M → Bool) →
πᵢ-SecureChannel M L l ≃ πᵣ-SecureChannel M C PK L l pk?= c?=
secure {ℓ} M C PK L l pk?= c?= m?= = record
{ gas-map = _* 2
; simulator = S-SecureChannel M C PK L l pk?= c?=
; invariant = λ
{ ⟨ ⟨ stnode (just m) [] , lift true ⟩ ,
stnode (just pk) (
stnode (just ⟨ pk′ , stlog ⟩) [] ∷
stnode (just c) [] ∷
[]
) ⟩ → pk?= pk pk′ ∧ any (λ{ ⟨ m′ , c′ ⟩ → m?= m m′ ∧ c?= c c′ }) stlog
; ⟨ ⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[]
) ⟩ → true
; _ → false
}
; base-case = refl
; proof = λ
{ g σ O (call↓ here tt) ⟨
⟨ stnode (just m) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ here tt) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; zero σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; (suc g) σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ (there here) m) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O _ ⟨ ⟨ stnode nothing [] , lift true ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode nothing _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (stnode nothing [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (
stnode _ [] ∷
stnode nothing [] ∷
[])
⟩ ()
; g σ O _ ⟨ ⟨ stnode (just _) [] , lift false ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode (just _) _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (stnode (just _) [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (
stnode _ [] ∷
stnode (just _) [] ∷
[])
⟩ ()
; g σ O (call↓ (there (there ())) x) Σ inv
; g σ O (call↯ () here x) Σ inv
; g σ O (call↯ () (there here here) x) Σ inv
; g σ O (call↯ () (there (there here) here) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) here) x) Σ inv
; g σ O (call↯ ∈Γ (there here (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there here) (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) (there x₂ Γ⊑)) x) Σ inv
}
}

22
Yggdrasil/ExecutionModel.idr

@ -0,0 +1,22 @@
module Yggdrasil.ExecutionModel
--import Control.ST
import Yggdrasil.Distribution
data Action : Type -> Type -> Type where
Abort : Action s a
SecParam : Action s Nat
Sample : D a -> Action s a
-- Create : ??? (ST doesn't seem to do quite what we want...)
Compose : Action s a -> (a -> Action s b) -> Action s b
mutual
Functor (Action s) where
map f x = Compose x (pure . f)
Applicative (Action s) where
pure = Sample . pure
f <*> x = Compose f (\f' => map f' x)
Monad (Action s) where
(>>=) = Compose

37
Yggdrasil/Extensible.idr

@ -0,0 +1,37 @@
import Prelude.Cast
infixr 5 ^=
export
data (^=) : a -> b -> Type where
Refl : x ^= x
Extend : {a : Type} -> {b : Type} -> (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x ^= g x) -> f ^= g
eEqTransitive : a ^= b -> b ^= c -> a ^= c
eEqTransitive Refl eq = eq
eEqTransitive eq Refl = eq
eEqTransitive (Extend a _ prfab) (Extend _ d prfbc) = Extend a d (\x => eEqTransitive (prfab x) (prfbc x))
eEqSymmetric : a ^= b -> b ^= a
eEqSymmetric Refl = Refl
eEqSymmetric (Extend a b prfab) = Extend b a (\x => eEqSymmetric (prfab x))
Cast (a = b) (a ^= b) where
cast Refl = Refl
-- Tests
fiveEqFive : 5 ^= 5
fiveEqFive = Refl
Double1 : Nat -> Nat
Double1 x = x + x
Double2 : Nat -> Nat
Double2 x = 2 * x
doubleEqItems : (x : Nat) -> Double1 x ^= Double2 x
doubleEqItems n = rewrite plusZeroRightNeutral n in Refl
doubleEq : Double1 ^= Double2
doubleEq = Extend Double1 Double2 doubleEqItems

33
Yggdrasil/List.agda

@ -1,33 +0,0 @@
module Yggdrasil.List where
open import Data.List using (List; _∷_; []; map)
open import Data.Product using (_×_; Σ; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
data _∈_ {ℓ : Level} {A : Set ℓ} : A → List A → Set ℓ where
here : {x : A} {xs : List A} → x ∈ (x ∷ xs)
there : {x y : A} {xs : List A} → y ∈ xs → y ∈ (x ∷ xs)
with-proof : ∀ {ℓ} {A : Set ℓ} → (l : List A) → List (Σ A (_∈ l))
with-proof [] = []
with-proof (x ∷ xs) = ⟨ x , here ⟩ ∷ map (λ{⟨ x , ∈xs ⟩ → ⟨ x , there ∈xs ⟩})
(with-proof xs)
head-≡ : ∀ {ℓ} {A : Set ℓ} {l₁ l₂ : List A} {x y : A} → x ∷ l₁ ≡ y ∷ l₂ → x ≡ y
head-≡ refl = refl
tail-≡ : ∀ {ℓ} {A : Set ℓ} {l₁ l₂ : List A} {x y : A} → x ∷ l₁ ≡ y ∷ l₂ →
l₁ ≡ l₂
tail-≡ refl = refl
map≡-implies-∈≡ : ∀ {ℓ} {A B C : Set ℓ} {f₁ : A → C} {f₂ : B → C} {l₁ : List A}
{l₂ : List B} {x : A} → map f₁ l₁ ≡ map f₂ l₂ →
x ∈ l₁ → ∃[ y ] ((y ∈ l₂) × (f₁ x ≡ f₂ y))
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = []} () here
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = []} () (there ∈xs)
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = y ∷ ys} map≡ here =
⟨ y , ⟨ here , head-≡ map≡ ⟩ ⟩
map≡-implies-∈≡ {l₁ = x ∷ xs} {l₂ = y ∷ ys} map≡ (there ∈xs) = let
⟨ y , ⟨ ∈ys , x≡y ⟩ ⟩ = map≡-implies-∈≡ (tail-≡ map≡) ∈xs
in ⟨ y , ⟨ there ∈ys , x≡y ⟩ ⟩

116
Yggdrasil/Probability.agda

@ -1,116 +0,0 @@
module Yggdrasil.Probability where
open import Agda.Builtin.FromNat using (Number)
import Data.Nat.Literals as ℕLit
import Data.Rational.Literals as ℚLit
import Data.Integer.Literals as ℤLit
open import Data.List using (List; _∷_; []; map; filter; length; foldr)
open import Data.Fin using (Fin; zero; suc)
open import Data.Integer using (ℤ; +_; _-_) renaming (_*_ to _ℤ*_)
open import Data.Nat using (ℕ; zero; suc; s≤s) renaming (_*_ to _ℕ*_; _≤?_ to _ℕ≤?_; _≤_ to _ℕ≤_)
open import Data.Nat.Literals
open import Data.Nat.Properties using (≤-trans; ≤-refl)
open import Data.List.Properties using (length-filter; length-map)
open import Data.Product using (_×_; ∃; ∃-syntax; proj₁) renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ) renaming (_≤?_ to _ℚ≤?_; _≤_ to _ℚ≤_)
open import Function using (_∘_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (True; fromWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
open import Level using (Level; Lift; lower; _⊔_) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.List using (_∈_; with-proof)
import Yggdrasil.Rational as ℚ
instance
ℕnumber : Number ℕ
ℕnumber = ℕLit.number
ℤn