ElGamal IND-CPA as Concrete UC Emulation from DDH

The ElGamal IND-CPA game pair, indexed by the message pair (m₀, m₁), as a concrete UC emulation whose bound is the DDH advantage of explicit reductions. For every adversary A and environment Z, the gap is at most

DDH_Advantage (Reduction m₀ (envReduction A Z)) + DDH_Advantage (Reduction m₁ (envReduction A Z))

where (m₀, m₁) = Z.input, envReduction A Z runs A and then Z's distinguisher, and Reduction embeds a DDH triple as public key and ciphertext (ElGamalDDH.Reduction).

Main results

• elgamalGameAdvBoundC — the concrete game bound, from elgamal_indcpa_security.
• elgamal_uc_concrete — concrete UC emulation, obtained by instance search.
• elgamal_uc_concrete_apply — the same statement for a fixed adversary and environment, with the reductions written out.

noncomputable def CatCryptCore.Examples.ElGamalUCConcrete.elgamalReal (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : G × G → CatCrypt.Core.SPComp (G × ElGamalDDH.ElGamalScheme.Ciphertext G)

IND-CPA real game indexed by the message pair: encrypt m₀.

Equations

• CatCryptCore.Examples.ElGamalUCConcrete.elgamalReal G m = CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_real G m.1 m.2

noncomputable def CatCryptCore.Examples.ElGamalUCConcrete.elgamalIdeal (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : G × G → CatCrypt.Core.SPComp (G × ElGamalDDH.ElGamalScheme.Ciphertext G)

IND-CPA ideal game indexed by the message pair: encrypt m₁.

Equations

• CatCryptCore.Examples.ElGamalUCConcrete.elgamalIdeal G m = CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_ideal G m.1 m.2

noncomputable def CatCryptCore.Examples.ElGamalUCConcrete.elgamalDDHBound (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : G × G → (G × ElGamalDDH.ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) → ENNReal

DDH bound of a distinguisher D on messages m: the DDH advantages of the two reductions embedding m₀ and m₁.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCryptCore.Examples.ElGamalUCConcrete.elgamalReal_isPure (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m₀ m₁ : G) : (ElGamalDDH.ElGamal_INDCPA_real G m₀ m₁).IsPure

The real IND-CPA game does not read the heap.

instance CatCryptCore.Examples.ElGamalUCConcrete.instPureGameProdCiphertextElgamalReal (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Crypto.UCConcrete.PureGame (elgamalReal G)

instance CatCryptCore.Examples.ElGamalUCConcrete.instPureGameProdCiphertextElgamalIdeal (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Crypto.UCConcrete.PureGame (elgamalIdeal G)

instance CatCryptCore.Examples.ElGamalUCConcrete.elgamalGameAdvBoundC (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Crypto.UCConcrete.GameAdvBoundC (elgamalReal G) (elgamalIdeal G) (elgamalDDHBound G)

Concrete game bound: IND-CPA advantage of D on (m₀, m₁) is at most the DDH advantages of the reductions built from D.

theorem CatCryptCore.Examples.ElGamalUCConcrete.elgamal_uc_concrete (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (V : Type) : CatCrypt.Crypto.UCConcrete.UCEmulatesCSim (CatCrypt.Crypto.UCDSL.UCSpec.ofGame (G × G) (G × ElGamalDDH.ElGamalScheme.Ciphertext G) V) (CatCrypt.Crypto.UCDSL.UCProtocol.ofGame (elgamalReal G)) (CatCrypt.Crypto.UCDSL.UCProtocol.ofGame (elgamalIdeal G)) id (CatCrypt.Crypto.UCConcrete.gameUCBound (elgamalDDHBound G))

ElGamal IND-CPA as concrete UC emulation from DDH (composition plumbing, simulator S = A): the bound of adversary A and environment Z is the DDH advantage of the reductions of envReduction A Z.

theorem CatCryptCore.Examples.ElGamalUCConcrete.elgamal_uc_concrete_apply (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (V : Type) (A : G × ElGamalDDH.ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp V) (Z : CatCrypt.Crypto.UCConcrete.Env (G × G) (Unit ⊕ V)) : CatCrypt.Crypto.UCConcrete.Env.gap (fun (m : G × G) => (CatCrypt.Crypto.UCDSL.UCProtocol.ofGame (elgamalReal G) m).bind (CatCrypt.Crypto.mapSum CatCrypt.Core.SPComp.pure A)) (fun (m : G × G) => (CatCrypt.Crypto.UCDSL.UCProtocol.ofGame (elgamalIdeal G) m).bind (CatCrypt.Crypto.mapSum CatCrypt.Core.SPComp.pure A)) Z ≤ CyclicGroupDDH.DDH_Advantage G (ElGamalDDH.Reduction G Z.input.1 (CatCrypt.Crypto.UCConcrete.envReduction A Z)) + CyclicGroupDDH.DDH_Advantage G (ElGamalDDH.Reduction G Z.input.2 (CatCrypt.Crypto.UCConcrete.envReduction A Z))

elgamal_uc_concrete for a fixed adversary A and environment Z, with the DDH reductions written out.