Asymmetric Encryption Schemes: One-Time IND-CPA

This file contains the standard two-phase one-time IND-CPA game together with the ProbComp specialization used by the generic many-query lift.

structure AsymmEncAlg.IND_CPA_Adv {m : Type → Type v} [Monad m] {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) : Type (max 1 v)

Two-phase adversary for IND-CPA security.

• State : Type
• chooseMessages : PK → m (M × M × self.State)
• distinguish : self.State → C → m Bool

def AsymmEncAlg.IND_CPA_OneTime_Game {M PK SK C ι : Type} {spec : OracleSpec ι} {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} (adv : encAlg.IND_CPA_Adv) (runtime : ProbCompRuntime (OracleComp spec)) : SPMF Bool

One-time IND-CPA experiment for an asymmetric encryption algorithm: sample keys, let the adversary choose challenge messages, encrypt one branch, and return whether the adversary guessed the hidden bit.

noncomputable def AsymmEncAlg.IND_CPA_OneTime_biasAdvantage {M PK SK C ι : Type} {spec : OracleSpec ι} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) (runtime : ProbCompRuntime (OracleComp spec)) (adv : encAlg.IND_CPA_Adv) : ℝ

Absolute one-time IND-CPA bias advantage for the general two-phase game.

@[reducible, inline]

abbrev AsymmEncAlg.IND_CPA_OneTime_Game_ProbComp {M PK SK C : Type} {encAlg : AsymmEncAlg ProbComp M PK SK C} (adv : encAlg.IND_CPA_Adv) : ProbComp Bool

ProbComp specialization of the one-time IND-CPA game.

noncomputable def AsymmEncAlg.IND_CPA_OneTime_signedAdvantageReal {M PK SK C : Type} (encAlg : AsymmEncAlg ProbComp M PK SK C) (adv : encAlg.IND_CPA_Adv) : ℝ

Real-valued signed one-time IND-CPA advantage.