Browse Source

Fro and Fcrs work again!

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
ef38a07fe6
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
5 changed files with 137 additions and 142 deletions
  1. +29
    -31
      src/Yggdrasil/ExecutionModel.hs
  2. +81
    -83
      src/Yggdrasil/Functionalities.hs
  3. +7
    -11
      tests/ExecTests.hs
  4. +18
    -16
      tests/FunctTests.hs
  5. +2
    -1
      yggdrasil.cabal

+ 29
- 31
src/Yggdrasil/ExecutionModel.hs View File

@@ -13,18 +13,18 @@

module Yggdrasil.ExecutionModel
( Operation
, SendRef
, RealRef
, Ref(External)
, Action(..)
, Action(Abort, Sample, Create)
, Operations
, Interfaces
, InterfaceMap
, Functionality(..)
, weaken
, InterfaceMap
, run
) where

import Control.Monad (ap)
import Control.Monad.Fail (MonadFail (fail))
import Control.Monad.ST (ST, runST)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
@@ -36,19 +36,13 @@ import Yggdrasil.HList (HList (Cons, Nil))

type Operation s c a b = c -> Ref s -> a -> Action s (c, b)

type family Operations s c (xs :: [*]) :: [*]

type instance Operations s c '[] = '[]

type instance Operations s c ((a, b) ': xs) =
Operation s c a b ': Operations s c xs
type family Operations s c (xs :: [(*, *)]) :: [*] where
Operations s c '[] = '[]
Operations s c ('( a, b) ': xs) = Operation s c a b ': Operations s c xs

type family Interfaces s (xs :: [*]) = (ys :: [*]) | ys -> xs

type instance Interfaces s '[] = '[]

type instance Interfaces s ((a, b) ': xs) =
SendRef s a b ': Interfaces s xs
type family Interfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
Interfaces s '[] = '[]
Interfaces s ('( a, b) ': xs) = (a -> Action s b) ': Interfaces s xs

data Functionality s c ops =
Functionality c
@@ -57,22 +51,24 @@ data Functionality s c ops =
type ID s = STRef s ()

data SendRef s a b =
forall c. SendRef (STRef s c)
(ID s)
forall c. SendRef (RealRef s c)
(Operation s c a b)

data RealRef s a =
RealRef (STRef s a)
(ID s)

data Ref s
= forall a. Ref (STRef s a)
(ID s)
= forall a. Ref (RealRef s a)
| External

instance Eq (Ref s) where
External == External = True
Ref _ a == Ref _ b = a == b
Ref (RealRef _ a) == Ref (RealRef _ b) = a == b
_ == _ = False

weaken :: SendRef s a b -> Ref s
weaken (SendRef ref id' _) = Ref ref id'
weaken (SendRef ref _) = Ref ref

data Action s b where
Abort :: Action s b
@@ -80,7 +76,7 @@ data Action s b where
Send :: SendRef s a b -> a -> Action s b
Create
:: InterfaceMap s c ops
=> Functionality s c ops
=> Functionality s c (ops :: [(*, *)])
-> Action s (HList (Interfaces s ops))
Compose :: Action s c -> (c -> Action s b) -> Action s b

@@ -94,6 +90,9 @@ instance Applicative (Action s) where
instance Monad (Action s) where
a >>= b = Compose a b

instance MonadFail (Action s) where
fail _ = Abort

run :: (forall s. Action s b) -> DistributionT Maybe b
run a =
DistributionT $ \rng -> runST $ runMaybeT $ runDistT (run' External a) rng
@@ -101,7 +100,7 @@ run a =
run' :: Ref s -> Action s b -> DistributionT (MaybeT (ST s)) b
run' _ Abort = DistributionT $ \_ -> MaybeT $ return Nothing
run' _ (Sample d) = liftDistribution d
run' from (Send to@(SendRef (ptr :: STRef s c) _ op) msg) = do
run' from (Send to@(SendRef (RealRef (ptr :: STRef s c) _) op) msg) = do
c <- lift . lift $ readSTRef ptr
(c', b) <- run' (weaken to) (op c from msg)
lift . lift $ writeSTRef ptr c'
@@ -109,16 +108,15 @@ run' from (Send to@(SendRef (ptr :: STRef s c) _ op) msg) = do
run' _ (Create (Functionality c ops)) = do
ptr <- lift . lift $ newSTRef c
id' <- lift . lift $ newSTRef ()
return $ ifmap ptr id' ops
return $ ifmap (RealRef ptr id') ops
run' from (Compose a f) = run' from a >>= run' from . f

-- | Dictates we can create interfaces from operations.
class InterfaceMap s c (ts :: [*]) where
ifmap ::
STRef s c -> ID s -> HList (Operations s c ts) -> HList (Interfaces s ts)
class InterfaceMap s c (ts :: [(*, *)]) where
ifmap :: RealRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)

instance InterfaceMap s c '[] where
ifmap _ _ Nil = Nil
ifmap _ Nil = Nil

instance InterfaceMap s c as => InterfaceMap s c ((a, b) ': as) where
ifmap ref id' (Cons x xs) = Cons (SendRef ref id' x) (ifmap ref id' xs)
instance InterfaceMap s c as => InterfaceMap s c ('( a, b) ': as) where
ifmap ref (Cons x xs) = Cons (\a -> Send (SendRef ref x) a) (ifmap ref xs)

+ 81
- 83
src/Yggdrasil/Functionalities.hs View File

@@ -1,28 +1,30 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.Functionalities
( ROState
, SigState
, SignatureInterface(..)
--, SigState
--, SignatureInterface(..)
, commonRandomString
, randomOracle
, signature
, robustSignature
--, signature
--, robustSignature
) where

import Data.Dynamic (Typeable)
import Yggdrasil.Adversarial (WithAdversary)
import Yggdrasil.Distribution (Distribution, coin)
import Yggdrasil.ExecutionModel (Action,
--import Yggdrasil.Adversarial (WithAdversary)
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
Functionality (Functionality),
Operation, Ref, abort, doSample,
interface, interface')
Operation)
import Yggdrasil.HList (HList (Cons, Nil))

crsOp :: Distribution b -> Operation (Maybe b) () b
crsOp _ (Just x, _, ()) = return (Just x, x)
crsOp d (Nothing, _, ()) = (\x -> (Just x, x)) <$> doSample d
crsOp :: Distribution b -> Operation s (Maybe b) () b
crsOp _ (Just x) _ () = return (Just x, x)
crsOp d Nothing _ () = (\x -> (Just x, x)) <$> Sample d

commonRandomString ::
Typeable b => Distribution b -> Functionality (Maybe b) (Action b)
commonRandomString d = Functionality Nothing (interface' (crsOp d))
Distribution b -> Functionality s (Maybe b) ('( (), b) ': '[])
commonRandomString d = Functionality Nothing (Cons (crsOp d) Nil)

type ROState a b = [(a, b)]

@@ -32,77 +34,73 @@ roLookup ((x, y):_) x'
| x == x' = Just y
roLookup (_:xs) x = roLookup xs x

roOp :: Eq a => Distribution b -> Operation (ROState a b) a b
roOp d (xs, _, x') =
case roLookup xs x' of
roOp :: Eq a => Distribution b -> Operation s (ROState a b) a b
roOp d xs _ x =
case roLookup xs x of
Just y -> return (xs, y)
Nothing -> do
y <- doSample d
return ((x', y) : xs, y)
y <- Sample d
return ((x, y) : xs, y)

randomOracle ::
(Eq a, Typeable a, Typeable b)
=> Distribution b
-> Functionality (ROState a b) (a -> Action b)
randomOracle d = Functionality [] (interface $ roOp d)

Eq a => Distribution b -> Functionality s (ROState a b) ('( a, b) ': '[])
randomOracle d = Functionality [] (Cons (roOp d) Nil)
-- TODO: Don't abort with bad adversaries? Would probably need a specialised s
-- though.
type SigState m s = [(m, s, Ref)]

data SignatureInterface m s = SignatureInterface
{ sign :: m -> Action s
, verify :: (m, s, Ref) -> Action Bool
}

signOp :: Eq s => ((m, Ref) -> Action s) -> Operation (SigState m s) m s
signOp adv (st, from, m) = do
sig <- adv (m, from)
if sig `elem` map (\(_, s, _) -> s) st
then abort
else return ((m, sig, from) : st, sig)

verifyOp :: (Eq m, Eq s) => Operation (SigState m s) (m, s, Ref) Bool
verifyOp (st, _, s) = return (st, s `elem` st)

signature ::
(Eq m, Eq s, Typeable m, Typeable s)
=> WithAdversary ((m, Ref) -> Action s) (Functionality (SigState m s) (SignatureInterface m s))
signature adv =
Functionality
[]
(do adv' <- adv
adv'' <- maybe abort return adv'
--adv'' <- fromMaybe abort (return <$> adv')
sign' <- interface $ signOp adv''
verify' <- interface verifyOp
return $ SignatureInterface sign' verify')

robustSignOp ::
Maybe ((m, Ref) -> Action [Bool])
-> Int
-> Operation (SigState m [Bool]) m [Bool]
robustSignOp (Just adv) secparam (st, from, m) = do
sig <- adv (m, from)
sig' <-
if sig `elem` map (\(_, s, _) -> s) st
then forceSample secparam
else return sig
return ((m, sig', from) : st, sig')
robustSignOp Nothing secparam (st, from, m) =
(\sig -> ((m, sig, from) : st, sig)) <$> forceSample secparam

forceSample :: Int -> Action [Bool]
forceSample secparam = sequence [doSample coin | _ <- [0 .. secparam]]

robustSignature ::
(Eq m, Typeable m)
=> Int
-> WithAdversary ((m, Ref) -> Action [Bool]) (Functionality (SigState m [Bool]) (SignatureInterface m [Bool]))
robustSignature secparam adv =
Functionality
[]
(do adv' <- adv
sign' <- interface $ robustSignOp adv' secparam
verify' <- interface verifyOp
return $ SignatureInterface sign' verify')
--type SigState m s = [(m, s, Ref)]
--
--data SignatureInterface m s = SignatureInterface
-- { sign :: m -> Action s
-- , verify :: (m, s, Ref) -> Action Bool
-- }
--
--signOp :: Eq s => ((m, Ref) -> Action s) -> Operation (SigState m s) m s
--signOp adv (st, from, m) = do
-- sig <- adv (m, from)
-- if sig `elem` map (\(_, s, _) -> s) st
-- then abort
-- else return ((m, sig, from) : st, sig)
--
--verifyOp :: (Eq m, Eq s) => Operation (SigState m s) (m, s, Ref) Bool
--verifyOp (st, _, s) = return (st, s `elem` st)
--signature ::
-- (Eq m, Eq s, Typeable m, Typeable s)
-- => WithAdversary ((m, Ref) -> Action s) (Functionality (SigState m s) (SignatureInterface m s))
--signature adv =
-- Functionality
-- []
-- (do adv' <- adv
-- adv'' <- maybe abort return adv'
-- --adv'' <- fromMaybe abort (return <$> adv')
-- sign' <- interface $ signOp adv''
-- verify' <- interface verifyOp
-- return $ SignatureInterface sign' verify')
--
--robustSignOp ::
-- Maybe ((m, Ref) -> Action [Bool])
-- -> Int
-- -> Operation (SigState m [Bool]) m [Bool]
--robustSignOp (Just adv) secparam (st, from, m) = do
-- sig <- adv (m, from)
-- sig' <-
-- if sig `elem` map (\(_, s, _) -> s) st
-- then forceSample secparam
-- else return sig
-- return ((m, sig', from) : st, sig')
--robustSignOp Nothing secparam (st, from, m) =
-- (\sig -> ((m, sig, from) : st, sig)) <$> forceSample secparam
--
--forceSample :: Int -> Action [Bool]
--forceSample secparam = sequence [doSample coin | _ <- [0 .. secparam]]
--
--robustSignature ::
-- (Eq m, Typeable m)
-- => Int
-- -> WithAdversary ((m, Ref) -> Action [Bool]) (Functionality (SigState m [Bool]) (SignatureInterface m [Bool]))
--robustSignature secparam adv =
-- Functionality
-- []
-- (do adv' <- adv
-- sign' <- interface $ robustSignOp adv' secparam
-- verify' <- interface verifyOp
-- return $ SignatureInterface sign' verify')

+ 7
- 11
tests/ExecTests.hs View File

@@ -8,33 +8,29 @@ 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, Ref (External), doSample,
run, self)
import Yggdrasil.Distribution (runDistT, uniform)
import Yggdrasil.ExecutionModel (Action (Sample), run)

inSampleRange :: Int -> Bool
inSampleRange x = x > 4700 && x < 5300

sampleTest :: Action Int
sampleTest :: Action s Int
sampleTest = sampleTest' 10000
where
sampleTest' :: Int -> Action Int
sampleTest' :: Int -> Action s Int
sampleTest' 0 = return 0
sampleTest' n = do
x <- sampleTest' (n - 1)
b <- doSample (uniform [0, 1])
b <- Sample (uniform [0, 1])
return $ x + b

spec :: IO Spec
spec = do
rnd <- getSystemDRG
let secparam = 128
return $
describe "action" $ do
prop "obeys return" $ \(x :: String) ->
sample' rnd (run secparam (return x)) == Just x
it "is exteral" $
sample' rnd (run secparam self) == Just External `shouldBe` True
(fst <$> runDistT (run (return x)) rnd) == Just x
it "samples evenly" $
inSampleRange (fromJust $ sample' rnd (run secparam sampleTest)) `shouldBe`
inSampleRange (fst $ fromJust $ runDistT (run sampleTest) rnd) `shouldBe`
True

+ 18
- 16
tests/FunctTests.hs View File

@@ -1,3 +1,4 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

module FunctTests
@@ -6,42 +7,43 @@ module FunctTests

import Crypto.Random (getSystemDRG)
import Test.Hspec (Spec, describe, it, shouldBe)
import Yggdrasil.Distribution (sample', uniform)
import Yggdrasil.ExecutionModel (Action, create, run)
import Yggdrasil.Distribution (runDistT, uniform)
import Yggdrasil.ExecutionModel (Action (Create), run)
import Yggdrasil.Functionalities (commonRandomString, randomOracle)
import Yggdrasil.HList (HList (Cons, Nil))

crsSameTest :: Action Bool
crsSameTest :: Action s Bool
crsSameTest = do
crsHandle <- create $ commonRandomString (uniform [0 .. 10000 :: Int])
fst' <- crsHandle
snd' <- crsHandle
(Cons crsHandle Nil) <-
Create $ commonRandomString (uniform [0 .. 10000 :: Int])
fst' <- crsHandle ()
snd' <- crsHandle ()
return (fst' == snd')

roSameTest :: Action Bool
roSameTest :: Action s Bool
roSameTest = do
roHandle :: (Int -> Action Int) <-
create $ randomOracle (uniform [0 .. 1000 :: Int])
(Cons (roHandle :: Int -> Action s Int) Nil) <-
Create $ randomOracle (uniform [0 .. 1000 :: Int])
fst' <- roHandle 1
snd' <- roHandle 1
return (fst' == snd')

roAllEqual :: Action Bool
roAllEqual :: Action s Bool
roAllEqual = do
roHandle :: (Int -> Action Int) <-
create $ randomOracle (uniform [0 .. 1000 :: Int])
(Cons (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
let secparam = 128
return $ do
describe "common random string" $
it "returns the same value" $
sample' rnd (run secparam crsSameTest) `shouldBe` Just True
(fst <$> runDistT (run crsSameTest) rnd) `shouldBe` Just True
describe "random oracle" $ do
it "returns the same for the same query" $
sample' rnd (run secparam roSameTest) `shouldBe` Just True
(fst <$> runDistT (run roSameTest) rnd) `shouldBe` Just True
it "is random with different queries" $
sample' rnd (run secparam roAllEqual) `shouldBe` Just False
(fst <$> runDistT (run roAllEqual) rnd) `shouldBe` Just False

+ 2
- 1
yggdrasil.cabal View File

@@ -16,7 +16,8 @@ library
exposed-modules:
Yggdrasil.Distribution
Yggdrasil.ExecutionModel
--Yggdrasil.Functionalities Yggdrasil.Adversarial
Yggdrasil.Functionalities
-- Yggdrasil.Adversarial
Yggdrasil.HList
other-extensions: GADTs
Rank2Types

Loading…
Cancel
Save