Documentation

VCVio.CryptoFoundations.KEMDEM

KEM + DEM Composition #

This file defines the textbook KEM+DEM public-key encryption construction and the proof-ladders A1 reduction skeleton against the repo's existing KEM and one-time IND-CPA interfaces.

source
def KEMScheme.composeWithDEM {m : Type → Type v} {K PK SK CKEM M CDEM : Type} [Monad m] (kem : KEMScheme m K PK SK CKEM) (dem : DEMScheme m K M CDEM) :
AsymmEncAlg m M PK SK (CKEM × CDEM)

Textbook KEM+DEM composition. The composed scheme inherits the KEM execution method.

Instances For
    source
    theorem KEMScheme.perfectlyCorrect_composeWithDEM {m : Type → Type v} {K PK SK CKEM M CDEM : Type} [DecidableEq K] [DecidableEq M] [Monad m] [HasEvalSPMF m] [LawfulMonad m] (kem : KEMScheme m K PK SK CKEM) (dem : DEMScheme m K M CDEM) (hkem : Pr[= true | kem.CorrectExp] = 1) (hdem : ∀ (k : K) (msg : M), Pr[= true | dem.CorrectExp k msg] = 1) (msg : M) :
    Pr[= true | (kem.composeWithDEM dem).CorrectExp msg] = 1

    If a KEM and externally keyed DEM are both perfectly correct in the concrete probabilistic semantics of m, then their composition is also perfectly correct.

    source
    def KEMScheme.composeWithDEM_toKEMLeftReduction {K PK SK CKEM M CDEM ι : Type} {spec : OracleSpec ι} (kem : KEMScheme (OracleComp spec) K PK SK CKEM) (dem : DEMScheme (OracleComp spec) K M CDEM) (adversary : (kem.composeWithDEM dem).IND_CPA_Adv) :
    kem.IND_CPA_Adversary

    Left KEM reduction from a one-time IND-CPA adversary against the composed KEM+DEM PKE.

    Instances For
      source
      def KEMScheme.composeWithDEM_toKEMRightReduction {K PK SK CKEM M CDEM ι : Type} {spec : OracleSpec ι} (kem : KEMScheme (OracleComp spec) K PK SK CKEM) (dem : DEMScheme (OracleComp spec) K M CDEM) (adversary : (kem.composeWithDEM dem).IND_CPA_Adv) :
      kem.IND_CPA_Adversary

      Right KEM reduction from a one-time IND-CPA adversary against the composed KEM+DEM PKE.

      Instances For
        source
        def KEMScheme.composeWithDEM_toDEMReduction {K PK SK CKEM M CDEM ι : Type} {spec : OracleSpec ι} (kem : KEMScheme (OracleComp spec) K PK SK CKEM) (dem : DEMScheme (OracleComp spec) K M CDEM) (adversary : (kem.composeWithDEM dem).IND_CPA_Adv) :
        dem.IND_CPA_Adversary

        DEM reduction from a one-time IND-CPA adversary against the composed KEM+DEM PKE. It samples the public key and KEM ciphertext during the message-selection phase so that the simulatee sees the same encaps-then-encrypt effect order as the composed scheme.

        Instances For
          source
          theorem KEMScheme.ind_cpa_one_time_bias_advantage_compose_with_dem_le {K PK SK CKEM M CDEM ι : Type} {spec : OracleSpec ι} [SampleableType K] (kem : KEMScheme (OracleComp spec) K PK SK CKEM) (dem : DEMScheme (OracleComp spec) K M CDEM) (runtime : ProbCompRuntime (OracleComp spec)) (adversary : (kem.composeWithDEM dem).IND_CPA_Adv) :
          (kem.composeWithDEM dem).IND_CPA_OneTime_biasAdvantage runtime adversary ≤ IND_CPA_Advantage runtime (kem.composeWithDEM_toKEMLeftReduction dem adversary) + IND_CPA_Advantage runtime (kem.composeWithDEM_toKEMRightReduction dem adversary) + DEMScheme.IND_CPA_Advantage runtime (kem.composeWithDEM_toDEMReduction dem adversary)

          Proof-ladders A1 reduction statement: the one-time IND-CPA advantage of textbook KEM+DEM is bounded by two KEM IND-CPA advantages plus one DEM IND-CPA advantage, using the canonical left/right and DEM reductions defined above.