Key Encapsulation Mechanisms

This file defines a type to represent protocols for key encapsulation mechanisms. We also define basic correctness and security properties for these protocols.

structure KEMScheme (m : Type → Type u) [Monad m] (K PK SK C : Type) : Type u

A key encapsulation mechanism with shared-key space K, public/secret key spaces PK and SK, and ciphertext space C.

• keygen : m (PK × SK)
• encaps : PK → m (C × K)
• decaps : SK → C → m (Option K)

def KEMScheme.CorrectExp {m : Type → Type v} [Monad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) [DecidableEq K] : m Bool

Correctness experiment: decapsulation of an honestly generated encapsulation should recover the shared key.

def KEMScheme.PerfectlyCorrect {m : Type → Type v} [Monad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) [DecidableEq K] (runtime : ProbCompRuntime m) : Prop

Perfect correctness of a KEM.

structure KEMScheme.IND_CPA_Adversary {K PK SK C ι : Type} {spec : OracleSpec ι} (_kem : KEMScheme (OracleComp spec) K PK SK C) : Type (max 1 u_1)

Two-phase IND-CPA adversary for a KEM. The adversary only gets access to the base oracle set spec, with no decapsulation oracle.

• State : Type
• preChallenge : PK → OracleComp spec self.State
• postChallenge : self.State → C → K → OracleComp spec Bool

def KEMScheme.IND_CPA_Exp {K PK SK C ι : Type} {spec : OracleSpec ι} [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CPA_Adversary) (b : Bool) : SPMF Bool

Fixed-branch IND-CPA experiment for a KEM, matching the source proof-ladders formulation Exp.run(b).

def KEMScheme.IND_CPA_Game {K PK SK C ι : Type} {spec : OracleSpec ι} [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CPA_Adversary) : SPMF Bool

Single-game IND-CPA experiment obtained by sampling the challenge bit uniformly and checking whether the adversary guessed it correctly.

noncomputable def KEMScheme.IND_CPA_Advantage {K PK SK C ι : Type} {spec : OracleSpec ι} [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CPA_Adversary) : ℝ

IND-CPA distinguishing advantage for a KEM, defined canonically as the bias of the single game.

theorem KEMScheme.IND_CPA_Advantage_eq_game_bias {K PK SK C ι : Type} {spec : OracleSpec ι} [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CPA_Adversary) : IND_CPA_Advantage runtime adversary = (IND_CPA_Game runtime adversary).boolBiasAdvantage

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

def KEMScheme.IND_CCA_oracleSpec {K PK SK C ι : Type} {spec : OracleSpec ι} (_kem : KEMScheme (OracleComp spec) K PK SK C) : OracleSpec (ι ⊕ C)

IND-CCA adversaries get access to the base oracle set spec plus a decapsulation oracle.

structure KEMScheme.IND_CCA_Adversary {K PK SK C ι : Type} {spec : OracleSpec ι} (kem : KEMScheme (OracleComp spec) K PK SK C) : Type 1

Two-phase IND-CCA adversary for a KEM.

• State : Type
• preChallenge : PK → OracleComp kem.IND_CCA_oracleSpec self.State
• postChallenge : self.State → C → K → OracleComp kem.IND_CCA_oracleSpec Bool

def KEMScheme.IND_CCA_preChallengeImpl {K PK SK C ι : Type} {spec : OracleSpec ι} (kem : KEMScheme (OracleComp spec) K PK SK C) (sk : SK) : QueryImpl kem.IND_CCA_oracleSpec (OracleComp spec)

Pre-challenge decapsulation oracle.

def KEMScheme.IND_CCA_postChallengeImpl {K PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] (kem : KEMScheme (OracleComp spec) K PK SK C) (sk : SK) (cStar : C) : QueryImpl kem.IND_CCA_oracleSpec (OracleComp spec)

Post-challenge decapsulation oracle: the challenge ciphertext itself maps to none.

def KEMScheme.IND_CCA_Game {K PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CCA_Adversary) : SPMF Bool

IND-CCA real-or-random experiment for a KEM.

noncomputable def KEMScheme.IND_CCA_Advantage {K PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CCA_Adversary) : ℝ

IND-CCA distinguishing advantage for a KEM.

def KEMScheme.IND_CPA_Adversary.toIND_CCA {K PK SK C ι : Type} {spec : OracleSpec ι} {kem : KEMScheme (OracleComp spec) K PK SK C} (adversary : kem.IND_CPA_Adversary) : kem.IND_CCA_Adversary

Any IND-CPA adversary can be viewed as an IND-CCA adversary that simply ignores the decapsulation oracle while preserving its ordinary pre-challenge interaction with the base oracle set spec.

theorem KEMScheme.IND_CPA_Game_eq_IND_CCA_Game_toIND_CCA {K PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] [SampleableType K] {kem : KEMScheme (OracleComp spec) K PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : kem.IND_CPA_Adversary) : IND_CPA_Game runtime adversary = IND_CCA_Game runtime adversary.toIND_CCA

The one-stage IND-CPA game is exactly the IND-CCA game instantiated with the trivial CPA-to-CCA embedding (toIND_CCA) that never uses the decryption oracle.