Asymmetric Encryption Schemes: IND-CCA

IND-CCA interfaces and games for asymmetric encryption schemes.

def AsymmEncAlg.decryptionOracle {m : Type → Type v} [Monad m] {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) (sk : SK) : QueryImpl (OracleSpec.ofFn fun (x : C) => M) (OptionT m)

Oracle that uses a secret key to respond to decryption requests. Invalid ciphertexts become oracle failure in OptionT.

def AsymmEncAlg.IND_CCA_oracleSpec {M PK SK C ι : Type} {spec : OracleSpec ι} (_encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) : OracleSpec (ι ⊕ C)

IND-CCA adversaries get access to the base oracle set spec plus a decryption oracle. Challenge generation is handled explicitly between the two phases of the game.

structure AsymmEncAlg.IND_CCA_Adversary {M PK SK C ι : Type} {spec : OracleSpec ι} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) : Type 1

Two-phase IND-CCA adversary: chooseMessages runs before the challenge and outputs (m₀, m₁, st); distinguish st c⋆ runs after seeing the challenge ciphertext.

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

def AsymmEncAlg.IND_CCA_preChallengeImpl {M PK SK C ι : Type} {spec : OracleSpec ι} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) (sk : SK) : QueryImpl encAlg.IND_CCA_oracleSpec (OracleComp spec)

Pre-challenge decryption oracle for the IND-CCA game.

def AsymmEncAlg.IND_CCA_postChallengeImpl {M PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) (sk : SK) (cStar : C) : QueryImpl encAlg.IND_CCA_oracleSpec (OracleComp spec)

Post-challenge decryption oracle for the IND-CCA game. The challenge ciphertext itself is answered with none, while all other ciphertexts are decrypted normally.

def AsymmEncAlg.IND_CCA_Game {M PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : encAlg.IND_CCA_Adversary) : SPMF Bool

IND-CCA security game in the standard two-phase form. The adversary chooses challenge messages with access to the decryption oracle, then receives the challenge ciphertext and continues interacting with a decryption oracle that returns none on the challenge ciphertext.

noncomputable def AsymmEncAlg.IND_CCA_Advantage {M PK SK C ι : Type} {spec : OracleSpec ι} [DecidableEq C] {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : encAlg.IND_CCA_Adversary) : ℝ

Real-valued IND-CCA advantage, expressed as the Boolean bias of the IND-CCA game.