Data Encapsulation Mechanisms

This file defines data encapsulation mechanisms (DEMs), their correctness notion, and the one-time IND-CPA game used by the KEM+DEM composition theorem.

structure DEMScheme (m : Type → Type u) [Monad m] (K M C : Type) : Type u

A data encapsulation mechanism with key space K, message space M, and ciphertext space C. The key is supplied externally, matching the proof-ladders DEM model.

• encrypt : K → M → m C
• decrypt : K → C → m M

def DEMScheme.CorrectExp {m : Type → Type v} [Monad m] {K M C : Type} (dem : DEMScheme m K M C) [DecidableEq M] (k : K) (msg : M) : m Bool

Correctness experiment for a DEM under an externally supplied key.

def DEMScheme.PerfectlyCorrect {m : Type → Type v} [Monad m] {K M C : Type} (dem : DEMScheme m K M C) [DecidableEq M] (runtime : ProbCompRuntime m) : Prop

Perfect correctness for a DEM: every externally supplied key decrypts honest ciphertexts correctly with probability 1.

structure DEMScheme.IND_CPA_Adversary {K M C ι : Type} {spec : OracleSpec ι} (_dem : DEMScheme (OracleComp spec) K M C) : Type (max 1 u_1)

Two-phase one-time IND-CPA adversary for a DEM. The key is hidden, so the message-selection phase receives no public input.

• State : Type
• chooseMessages : OracleComp spec (M × M × self.State)
• distinguish : self.State → C → OracleComp spec Bool

def DEMScheme.IND_CPA_Exp {K M C ι : Type} {spec : OracleSpec ι} [SampleableType K] {dem : DEMScheme (OracleComp spec) K M C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : dem.IND_CPA_Adversary) (b : Bool) : SPMF Bool

Fixed-branch one-time IND-CPA experiment for a DEM, matching the source proof-ladders DEM_1CPA_Exp.run(b) presentation.

def DEMScheme.IND_CPA_Game {K M C ι : Type} {spec : OracleSpec ι} [SampleableType K] {dem : DEMScheme (OracleComp spec) K M C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : dem.IND_CPA_Adversary) : SPMF Bool

Game-form one-time IND-CPA experiment for a DEM.

noncomputable def DEMScheme.IND_CPA_Advantage {K M C ι : Type} {spec : OracleSpec ι} [SampleableType K] {dem : DEMScheme (OracleComp spec) K M C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : dem.IND_CPA_Adversary) : ℝ

One-time IND-CPA advantage for a DEM, defined canonically as the bias of the single game.

theorem DEMScheme.IND_CPA_Advantage_eq_game_bias {K M C ι : Type} {spec : OracleSpec ι} [SampleableType K] {dem : DEMScheme (OracleComp spec) K M C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : dem.IND_CPA_Adversary) : IND_CPA_Advantage runtime adversary = (IND_CPA_Game runtime adversary).boolBiasAdvantage

The canonical one-time IND-CPA advantage is definitionally the bias of the single game.