Browse Source

Re-generalise signatures.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
fd51430e7f
Signed by: tk <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
3 changed files with 42 additions and 29 deletions
  1. +1
    -1
      src/Yggdrasil/Distribution.hs
  2. +8
    -1
      src/Yggdrasil/ExecutionModel.hs
  3. +33
    -27
      src/Yggdrasil/Functionalities.hs

+ 1
- 1
src/Yggdrasil/Distribution.hs View File

@@ -13,7 +13,7 @@ module Yggdrasil.Distribution
, liftDistribution
) where

import Control.Monad ((>=>), ap)
import Control.Monad (ap, (>=>))
import Control.Monad.State.Lazy (State, runState, state)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Crypto.Random (SystemDRG, randomBytesGenerate)


+ 8
- 1
src/Yggdrasil/ExecutionModel.hs View File

@@ -19,6 +19,7 @@ module Yggdrasil.ExecutionModel
, Interfaces
, Functionality(..)
, InterfaceMap
, ForceSample(forceSample)
, run
) where

@@ -31,7 +32,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.STRef (STRef, newSTRef, readSTRef,
writeSTRef)
import Yggdrasil.Distribution (Distribution, DistributionT (DistributionT, runDistT),
liftDistribution)
coin, liftDistribution)
import Yggdrasil.HList (HList ((:::), Nil))

type Operation s c a b = Ref s -> a -> StateT c (Action s) b
@@ -123,3 +124,9 @@ instance InterfaceMap s c '[] where

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

class ForceSample t where
forceSample :: Action s t

instance ForceSample [Bool] where
forceSample = SecParam >>= (\sp -> sequence [Sample coin | _ <- [0 .. sp]])

+ 33
- 27
src/Yggdrasil/Functionalities.hs View File

@@ -16,8 +16,9 @@ import Control.Monad.State.Lazy (get, modify, put)
import Control.Monad.Trans.Class (lift)

import Yggdrasil.Adversarial (WithAdversary' (WithAdversary'))
import Yggdrasil.Distribution (Distribution, coin)
import Yggdrasil.ExecutionModel (Action (Sample, SecParam),
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
ForceSample (forceSample),
Functionality (Functionality),
Interfaces, Operation, Operations,
Ref)
@@ -56,39 +57,44 @@ randomOracle ::
Eq a => Distribution b -> Functionality s (ROState a b) '[ '( a, b)]
randomOracle d = Functionality [] (roOp d ::: Nil)

type SigState s msg = [(msg, [Bool], Ref s)]
type SigState s msg sig = [(msg, sig, Ref s)]

verifyOp :: (Eq msg) => Operation s (SigState s msg) (msg, [Bool], Ref s) Bool
verifyOp ::
(Eq msg, Eq sig) => Operation s (SigState s msg sig) (msg, sig, Ref s) Bool
verifyOp _ s = (s `elem`) <$> get

forceSample :: Action s [Bool]
forceSample = SecParam >>= (\sp -> sequence [Sample coin | _ <- [0 .. sp]])

fixAdv ::
Eq msg
=> HList (Interfaces s '[ '( (msg, Ref s), Maybe [Bool])])
-> HList (Operations s (SigState s msg) '[ '( (msg, Ref s), [Bool])])
(Eq msg, Eq sig, ForceSample sig)
=> HList (Interfaces s '[ '( (msg, Ref s), Maybe sig)])
-> HList (Operations s (SigState s msg sig) '[ '( (msg, Ref s), sig)])
fixAdv (sign ::: Nil) = sign' ::: Nil
where
sign' _ (msg, ref) =
lift (sign (msg, ref)) >>=
(\case
Just s ->
get >>=
(\st ->
if (msg, s, ref) `elem` st
then lift forceSample
else return s)
Nothing -> lift forceSample) >>=
(\s -> modify ((msg, s, ref) :) >> return s)
sign' _ (msg, ref) = do
sig <-
lift (sign (msg, ref)) >>= \case
Just s -> do
st <- get
if (msg, s, ref) `elem` st
then forceSample' msg ref
else return s
Nothing -> forceSample' msg ref
modify ((msg, sig, ref) :)
return sig
forceSample' msg ref = 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 (msg, sig, ref) `elem` st
then forceSample' msg ref
else return sig

signature ::
Eq msg
=> WithAdversary' s (SigState s msg)
'[ '( (msg, Ref s), [Bool])]
'[
'( (msg, Ref s), [Bool]),
'( (msg, [Bool], Ref s), Bool)
(Eq msg, Eq sig, ForceSample sig)
=> WithAdversary' s (SigState s msg sig)
'[ '( (msg, Ref s), sig)]
'[ '( (msg, Ref s), sig)
, '( (msg, sig, Ref s), Bool)
]
signature =
WithAdversary'


Loading…
Cancel
Save