Safe Haskell	Safe
Language	GHC2021

LambdaUC.Games.SymEncryption

Synopsis

data SymEncryptionScheme key mes ciph s = SymEncryptionScheme {
- symEKey :: forall m. MonadRand m => m key
- symEEnc :: forall m. MonadRand m => key -> mes -> s -> m (Maybe (s, ciph))
- symEDec :: key -> ciph -> Maybe mes
}
type SpSymEncryptionScheme key mes ciph s = Integer -> SymEncryptionScheme key mes ciph s
data EncDecReq mes ciph
- = EncReq mes
- | DecReq ciph
data EncDecResp mes ciph
- = EncResp ciph
- | DecResp mes
- | RespError
type EncDecIface mes ciph = EncDecReq mes ciph :> EncDecResp mes ciph
type AdvAlgo mes ciph = OracleCaller '[EncDecIface mes ciph] Bool
advantageIndCca2 :: forall key mes ciph s. (UniformDist mes, Default s) => Integer -> SpSymEncryptionScheme key mes ciph s -> (Integer -> AdvAlgo mes ciph) -> Rational
advantageIndCca3 :: forall key mes ciph s. (UniformDist mes, Default s) => Integer -> SpSymEncryptionScheme key mes ciph s -> (Integer -> AdvAlgo mes ciph) -> Rational
oracleEncDec :: SymEncryptionScheme key mes ciph s -> key -> s -> Oracle (EncDecIface mes ciph) ()
oracleEncRandNoDec :: UniformDist mes => SymEncryptionScheme key mes ciph s -> key -> s -> Oracle (EncDecIface mes ciph) ()
oracleEncRandDec :: UniformDist mes => SymEncryptionScheme key mes ciph s -> key -> s -> Oracle (EncDecIface mes ciph) ()

Documentation

data SymEncryptionScheme key mes ciph s #

Constructors

SymEncryptionScheme
Fields symEKey :: forall m. MonadRand m => m key symEEnc :: forall m. MonadRand m => key -> mes -> s -> m (Maybe (s, ciph)) Probabilistic, stateful computation that may fail, This is equivalent to `key -> mes -> StateT s (MaybeT m) ciph`. symEDec :: key -> ciph -> Maybe mes Deterministic, stateless computation that may fail

data EncDecReq mes ciph #

Constructors

EncReq mes
DecReq ciph

data EncDecResp mes ciph #

Constructors

type EncDecIface mes ciph = EncDecReq mes ciph :> EncDecResp mes ciph #

Arguments

:: forall key mes ciph s. (UniformDist mes, Default s)
=> Integer	Security parameter
-> SpSymEncryptionScheme key mes ciph s	Encryption scheme
-> (Integer -> AdvAlgo mes ciph)	Adversary
-> Rational

Arguments

:: forall key mes ciph s. (UniformDist mes, Default s)
=> Integer	Security parameter
-> SpSymEncryptionScheme key mes ciph s	Encryption scheme
-> (Integer -> AdvAlgo mes ciph)	Adversary
-> Rational

Authenticated Encryption formulated as a form of Indistinguishability under Chosen Ciphertext Attack, see https://eprint.iacr.org/2004/272

TODO: implement without-loss-of-generality logic for the adversary here

oracleEncDec :: SymEncryptionScheme key mes ciph s -> key -> s -> Oracle (EncDecIface mes ciph) () #