Browse Source

Complete first pass of documentation.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
876c79c777
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
5 changed files with 75 additions and 14 deletions
  1. +4
    -4
      ChangeLog.md
  2. +22
    -0
      src/Yggdrasil/Adversarial.hs
  3. +27
    -0
      src/Yggdrasil/ExecutionModel.hs
  4. +8
    -0
      src/Yggdrasil/Functionalities.hs
  5. +14
    -10
      yggdrasil.cabal

+ 4
- 4
ChangeLog.md View File

@@ -1,8 +1,8 @@
# Revision history for yggdrasil

## 0.1.0.0 -- YYYY-mm-dd
## 0.1.0.0 -- 2018-09-10

* First version. Released on an unsuspecting world.
* Provide an UC-like execution model.
* Provide an UC-like, strictly typed execution model.
* Provide randomness distributions.
* Provide a (mostly) sane global state. (In particular, it is safe once weakened)
* Provide a typed model for arbitrary adversaries.
* Implement random oracles, crs, and signatures.

+ 22
- 0
src/Yggdrasil/Adversarial.hs View File

@@ -11,6 +11,14 @@
{-# 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
@@ -31,19 +39,29 @@ import Yggdrasil.ExecutionModel (Action (Create),
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 @b@ given a list of interfaces @ts@ 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 @c@ and interface @bs@
-- whjen given a list of interfaces @as@ 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
@@ -55,10 +73,13 @@ instance NoAdversary s '[] where
instance NoAdversary s xs => NoAdversary s ('( a, b) ': xs) where
nullOperations = (\_ _ -> return Nothing) ::: nullOperations @s @xs

-- | Closely corresponding to 'Interfaces', but also receiving a reference to
-- the original sender.
type family DummyInterfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
DummyInterfaces s '[] = '[]
DummyInterfaces s ('( a, b) ': xs) = (Ref s -> a -> Action s b) ': DummyInterfaces s xs

-- | A dummy adversary executes the interfaces the environments hands it.
class DummyAdversary s (bs :: [(*, *)]) where
operations ::
HList (DummyInterfaces s (MaybeMap bs))
@@ -75,6 +96,7 @@ instance DummyAdversary s bs => DummyAdversary s ('( a, b) ': bs) where
((\ref x -> lift $ b ref x) :: 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))

+ 27
- 0
src/Yggdrasil/ExecutionModel.hs View File

@@ -10,6 +10,12 @@
{-# 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
, RealRef
@@ -35,16 +41,25 @@ import Yggdrasil.Distribution (Distribution, DistributionT (Distrib
coin, liftDistribution)
import Yggdrasil.HList (HList ((:::), Nil))

-- | Describes what a node with internal state of type @c@ does when passed an
-- input of type @a@ by @Ref s@.
type Operation s c a b = Ref s -> 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))
@@ -55,10 +70,12 @@ data SendRef s a b =
forall c. SendRef (RealRef s c)
(Operation s c a b)

-- | A reference to an actual node in the system.
data RealRef s a =
RealRef (STRef s a)
(ID s)

-- | A reference to a node, either 'RealRef', or external to the system.
data Ref s
= forall a. Ref (RealRef s a)
| External
@@ -71,11 +88,17 @@ instance Eq (Ref s) where
weaken :: SendRef s a b -> Ref s
weaken (SendRef ref _) = Ref ref

-- | 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 :: [(*, *)])
@@ -95,6 +118,7 @@ instance Monad (Action s) where
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' External a) rng
@@ -115,7 +139,7 @@ run' _ (Create (Functionality c ops)) = do
return $ ifmap (RealRef ptr id') ops
run' from (Compose a f) = run' from a >>= run' from . f

-- | States we can create interfaces from operations. Implemented for all @ts@.
class InterfaceMap s c (ts :: [(*, *)]) where
ifmap :: RealRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)

@@ -125,6 +149,8 @@ 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

-- | 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


+ 8
- 0
src/Yggdrasil/Functionalities.hs View File

@@ -4,6 +4,7 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- | A collection of common functionalities, ready for use.
module Yggdrasil.Functionalities
( ROState
, SigState
@@ -33,9 +34,12 @@ crsOp 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
@@ -53,10 +57,13 @@ roOp d _ x =
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 msg sig = [(msg, sig, Ref s)]

verifyOp ::
@@ -89,6 +96,7 @@ fixAdv (sign ::: Nil) = sign' ::: Nil
then forceSample' msg ref
else return sig

-- | A robust signature functionality.
signature ::
(Eq msg, Eq sig, ForceSample sig)
=> WithAdversary' s (SigState s msg sig)

+ 14
- 10
yggdrasil.cabal View File

@@ -1,28 +1,31 @@
name: yggdrasil
version: 0.1.0.0
synopsis: Executable specifications of composable security protocols.
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: t.kerber@ed.ac.uk
maintainer: tk@drwx.org
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:
exposed-modules: Yggdrasil.Adversarial
Yggdrasil.Distribution
Yggdrasil.ExecutionModel
Yggdrasil.Functionalities
Yggdrasil.Adversarial
Yggdrasil.HList
other-extensions: GADTs
Rank2Types
ScopedTypeVariables
TupleSections
build-depends: base >= 4.11 && < 4.12
, cryptonite >= 0.25 && < 0.26
, memory >= 0.14 && < 0.15
@@ -30,14 +33,14 @@ library
, transformers >= 0.5 && < 0.6
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Werror
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 -Werror
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints
main-is: Spec.hs
other-modules: ExecTests
FunctTests

Loading…
Cancel
Save