Certified PPT Reductions and Probabilistic Operations for Cramer–Shoup

This module constructs the uniform strict-PPT (IsPPTOn) operations and security reductions for the Multiplicative Cramer–Shoup public-key encryption scheme ($\mathcal{E}_{\mathrm{MCS}}$, Boneh and Shoup, Exercise 12.27, printed pp. 521–522, specialized to associated data $\mathcal{D} = \mathrm{Unit}$) over a PrimeOrderGroupFamily, following the Games 0–4 reduction structure of Boneh and Shoup, Section 12.5.3, Theorem 12.9, printed pp. 488–493:

1. Approximate exponent sampling via sampleModNat: sampleExp, sampleCramerShoupPair, sampleCramerShoupTripleExponents, and sampleCramerShoupSK, together with their IsPPTOn certificates and Game.advantage bounds (1 / 2 ^ n per exponent draw) relative to exact uniform sampling on ZMod (F.order d).
2. Phase 1/2 and collision-tracking decryption oracle handlers: cramerShoupPhase1Oracle, cramerShoupPhase2Reply, cramerShoupPhase2Oracle, and cramerShoupCollisionPhase2Oracle.
3. Certified strict-PPT DDH distinguishers (Game 1 → Game 2, eq. (12.22), printed p. 492): cramerShoupMsgToDDHDistinguisher and cramerShoupToDDHDistinguisher, with IsPPTOn certificates isPPTOn_cramerShoupMsgToDDHDistinguisher and isPPTOn_cramerShoupToDDHDistinguisher.
4. Certified strict-PPT CRHF collision finders (Game 3 → Game 4, eqs. (12.24)–(12.25), printed p. 492): cramerShoupMsgToCollisionFinder and cramerShoupToCollisionFinder, with IsPPTOn certificates isPPTOn_cramerShoupMsgToCollisionFinder and isPPTOn_cramerShoupToCollisionFinder.
5. Certified strict-PPT Encryption.cca2GameOn operations: cramerShoupValid, cramerShoupKeyGenProb, cramerShoupEncryptProb, and cramerShoupDecryptOpt, together with their ComputableInPolyTime and IsPPTOn certificates.

Approximate exponent sampling via sampleModNat

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleCramerShoupPair (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp (ℕ × ℕ)

Sample a pair of approximate exponents modulo F.order d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleCramerShoupTripleExponents (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp (ℕ × ℕ × ℕ)

Sample a 3-tuple of approximate exponents (a, b, c) modulo F.order d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleCramerShoupSK (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp ((ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ)

Sample a 6-tuple secret key ((s, t), ((s₁, t₁), (s₂, t₂))) of approximate exponents modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_sampleCramerShoupPair_le (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) (k : ZMod (F.order d) → ZMod (F.order d) → Game) : Game.advantage ((F.sampleCramerShoupPair n d).eval.bind fun (p : ℕ × ℕ) => k ↑p.1 ↑p.2) ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (σ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (τ : ZMod (F.order d)) => k σ τ) ≤ 2 / 2 ^ n

Replacing sampleCramerShoupPair n d by two independent uniform draws on ZMod (F.order d) changes Game.advantage by at most 2 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_sampleCramerShoupTripleExponents_le (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) (k : ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → Game) : Game.advantage ((F.sampleCramerShoupTripleExponents n d).eval.bind fun (p : ℕ × ℕ × ℕ) => k ↑p.1 ↑p.2.1 ↑p.2.2) ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (α : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (β : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (γ : ZMod (F.order d)) => k α β γ) ≤ 3 / 2 ^ n

Replacing sampleCramerShoupTripleExponents n d by three independent uniform draws on ZMod (F.order d) changes Game.advantage by at most 3 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_bind_sampleCramerShoupSK_le (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) (k : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ → Game) (kZMod : ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → ZMod (F.order d) → Game) (hcast : ∀ (s t s₁ t₁ s₂ t₂ : ℕ), k ((s, t), (s₁, t₁), s₂, t₂) = kZMod ↑s ↑t ↑s₁ ↑t₁ ↑s₂ ↑t₂) : Game.advantage ((F.sampleCramerShoupSK n d).eval.bind k) ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (σ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (τ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (σ₁ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (τ₁ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (σ₂ : ZMod (F.order d)) => (Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (τ₂ : ZMod (F.order d)) => kZMod σ τ σ₁ τ₁ σ₂ τ₂) ≤ 6 / 2 ^ n

Replacing sampleCramerShoupSK n d by six independent uniform draws on ZMod (F.order d) changes Game.advantage by at most 6 / 2 ^ n.

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupPhase1Oracle (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (request : Unit × List Bool) : StateT Unit ProbComp (List Bool)

Phase 1 decryption oracle handler for Cramer–Shoup.

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupPhase2Reply (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct req : List Bool) : List Bool

Stateless Phase 2 decryption reply for Cramer–Shoup, rejecting the challenge ciphertext ct with [].

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupPhase2Oracle (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) (request : Unit × List Bool) : StateT Unit ProbComp (List Bool)

Phase 2 decryption oracle handler for Cramer–Shoup, rejecting the challenge ciphertext ct.

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupCollisionPhase2Oracle (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) (request : Unit × List Bool) : StateT (Option (List Bool)) ProbComp (List Bool)

Phase 2 collision-tracking oracle handler for cramerShoupToCollisionFinder: replies with cramerShoupCollisionPhase2Reply and records some (extractCramerShoupTriple request.2) whenever isCramerShoupCollision H d request.2 ct holds.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupMsgToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from a CCA2AdversaryOf Msg with message-to-group-word encoding encodeMsg : F.Desc × Msg → List Bool ([BS23], proof of Theorem 12.9, Game 1 $\to$ Game 2, equation (12.22), printed pp. 490, 492, adapted to $\mathcal{E}_{\mathrm{MCS}}$).

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupToDDHDistinguisher (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf (List Bool)) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from a group-message 1CCA adversary (Msg = List Bool, encodeMsg = Prod.snd).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupMsgToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {encodeMsg : F.Desc × Msg → List Bool} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {adversary : Encryption.CCA2AdversaryOf Msg} (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime encodeMsg (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hA : Encryption.CCA2AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (p : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary bit p.1 p.2

cramerShoupMsgToDDHDistinguisher is uniform strict PPT whenever encodeMsg, H, and isElem are computable in polynomial time and adversary is a strict oracle PPT 1CCA adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupToDDHDistinguisher (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {adversary : Encryption.CCA2AdversaryOf (List Bool)} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hA : Encryption.CCA2AdversaryOf.IsPPT Turing.MultiTapeTM.encBits adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (p : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.cramerShoupToDDHDistinguisher H isElem adversary bit p.1 p.2

cramerShoupToDDHDistinguisher is uniform strict PPT whenever H and isElem are computable in polynomial time and adversary is a strict oracle PPT 1CCA adversary.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupMsgToCollisionFinder (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) : CollisionFinderFor F.Desc

The setup-parameterized collision finder constructed from a CCA2AdversaryOf Msg with message-to-group-word encoding encodeMsg : F.Desc × Msg → List Bool ([BS23], proof of Theorem 12.9, Game 4, equations (12.24)–(12.25), printed p. 492, adapted to $\mathcal{E}_{\mathrm{MCS}}$).

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupToCollisionFinder (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf (List Bool)) (bit : Bool) : CollisionFinderFor F.Desc

The setup-parameterized collision finder constructed from a group-message 1CCA adversary (Msg = List Bool, encodeMsg = Prod.snd).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupMsgToCollisionFinder (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {encodeMsg : F.Desc × Msg → List Bool} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {adversary : Encryption.CCA2AdversaryOf Msg} (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime encodeMsg (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hA : Encryption.CCA2AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary F.encDesc) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × F.Desc) => F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary bit p.1 p.2

cramerShoupMsgToCollisionFinder is uniform strict PPT whenever encodeMsg, H, and isElem are computable in polynomial time and adversary is a strict oracle PPT 1CCA adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupToCollisionFinder (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {adversary : Encryption.CCA2AdversaryOf (List Bool)} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hA : Encryption.CCA2AdversaryOf.IsPPT Turing.MultiTapeTM.encBits adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary F.encDesc) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × F.Desc) => F.cramerShoupToCollisionFinder H isElem adversary bit p.1 p.2

cramerShoupToCollisionFinder is uniform strict PPT whenever H and isElem are computable in polynomial time and adversary is a strict oracle PPT 1CCA adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeCramerShoupPublicKey_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (d : F.Desc) (α : ZMod (F.order d)) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) : F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk = F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2)

encodeCramerShoupPublicKey depends on sk only through its residues modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeCramerShoupChallenge_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (v w : F.Carrier d) (m : List Bool) : F.encodeCramerShoupChallenge H d sk (F.encode d v) (F.encode d w) m = F.encodeCramerShoupChallenge H d (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2) (F.encode d v) (F.encode d w) m

encodeCramerShoupChallenge depends on sk only through its residues modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeCramerShoup_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) : F.decodeCramerShoup H isElem d sk ct = F.decodeCramerShoup H isElem d (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2) ct

decodeCramerShoup depends on sk only through its residues modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupPhase1Oracle_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) : F.cramerShoupPhase1Oracle H isElem d sk = F.cramerShoupPhase1Oracle H isElem d (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2)

cramerShoupPhase1Oracle depends on sk only through its residues modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupPhase2Oracle_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) : F.cramerShoupPhase2Oracle H isElem d sk ct = F.cramerShoupPhase2Oracle H isElem d (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2) ct

cramerShoupPhase2Oracle depends on sk only through its residues modulo F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupCollisionPhase2Oracle_eq_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (d : F.Desc) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) : F.cramerShoupCollisionPhase2Oracle H isElem d sk ct = F.cramerShoupCollisionPhase2Oracle H isElem d (F.skNatOfZMod d ↑sk.1.1 ↑sk.1.2 ↑sk.2.1.1 ↑sk.2.1.2 ↑sk.2.2.1 ↑sk.2.2.2) ct

cramerShoupCollisionPhase2Oracle depends on sk only through its residues modulo F.order d.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeCramerShoupEncrypt_publicKey_eq_challenge (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α β σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m : List Bool) : have pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂; F.encodeCramerShoupEncrypt H d (F.encode d pkVal.1, F.encode d pkVal.2.1, F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2) m β.val = F.encodeCramerShoupChallenge H d (F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂) (F.encode d (β • F.generator d)) (F.encode d ((α * β) • F.generator d)) m

Word-level public-key encryption under cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂ coincides with encodeCramerShoupChallenge on (v, w) = (β • g, (α * β) • g) ([BS23], Section 12.5.3, Game 0 $\to$ Game 1, equation (12.21), printed p. 490).

Encryption.cca2GameOn and Encryption.INDCCA2On instantiation

def Cslib.Crypto.PrimeOrderGroupFamily.decodeCramerShoupSK (w : List Bool) : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ

Unpack a canonically framed 6-tuple secret key ((s, t), ((s₁, t₁), (s₂, t₂))) of natural numbers.

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeCramerShoupSK_encCramerShoupSK (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) : decodeCramerShoupSK (encCramerShoupSK sk) = sk

decodeCramerShoupSK left-inverts encCramerShoupSK.

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupValid (F : PrimeOrderGroupFamily) (isElem : F.Desc × List Bool → Bool) (d : ℕ → F.Desc) (n : ℕ) (_pk m₀ m₁ : List Bool) : Bool

Challenge-pair group-membership admissibility predicate for Encryption.cca2GameOn ([BS23], Section 12.5.3 & Exercise 12.27): both challenge words m₀ and m₁ must belong to the group F.Carrier (d n).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupKeyGenProb (F : PrimeOrderGroupFamily) (d : ℕ → F.Desc) (n : ℕ) : ProbComp (List Bool × List Bool)

Probabilistic polynomial-time Cramer–Shoup key generation for a group family d : ℕ → F.Desc, sampling approximate uniform exponents via sampleModNat.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupEncryptProb (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) (n : ℕ) (pk m : List Bool) : ProbComp (List Bool)

Probabilistic polynomial-time Cramer–Shoup encryption for a group family d : ℕ → F.Desc, sampling the encryption exponent via sampleModNat.

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupDecryptOpt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : ℕ → F.Desc) (n : ℕ) (skBits ct : List Bool) : Option (List Bool)

Deterministic polynomial-time Cramer–Shoup decryption for Encryption.cca2GameOn.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_cramerShoupValid (F : PrimeOrderGroupFamily) {isElem : F.Desc × List Bool → Bool} {d : ℕ → F.Desc} (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool × List Bool) => F.cramerShoupValid isElem d p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool

cramerShoupValid is computable in polynomial time whenever isElem and d are.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupKeyGenProb (F : PrimeOrderGroupFamily) {d : ℕ → F.Desc} (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (F.cramerShoupKeyGenProb d)

cramerShoupKeyGenProb is uniformly strict PPT whenever d is computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_cramerShoupEncryptProb (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × List Bool) => F.cramerShoupEncryptProb H d p.1 p.2.1 p.2.2

cramerShoupEncryptProb is uniformly strict PPT whenever H and d are computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_cramerShoupDecryptOpt (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {d : ℕ → F.Desc} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => F.cramerShoupDecryptOpt H isElem d p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

cramerShoupDecryptOpt is computable in polynomial time whenever H, isElem, and d are.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cca2Phase1Oracle_cramerShoupDecryptOpt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : ℕ → F.Desc) (n : ℕ) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) : Encryption.cca2Phase1Oracle Turing.MultiTapeTM.encBits (F.cramerShoupDecryptOpt H isElem d) n (encCramerShoupSK sk) = F.cramerShoupPhase1Oracle H isElem (d n) sk

cca2Phase1Oracle for cramerShoupDecryptOpt agrees with cramerShoupPhase1Oracle.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cca2Phase2Oracle_cramerShoupDecryptOpt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (d : ℕ → F.Desc) (n : ℕ) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) (ct : List Bool) : Encryption.cca2Phase2Oracle Turing.MultiTapeTM.encBits (F.cramerShoupDecryptOpt H isElem d) n (encCramerShoupSK sk) ct = F.cramerShoupPhase2Oracle H isElem (d n) sk ct

cca2Phase2Oracle for cramerShoupDecryptOpt agrees with cramerShoupPhase2Oracle.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeBits4_dropFrame_encodeCramerShoupPublicKey (F : PrimeOrderGroupFamily) (d : F.Desc) (u : List Bool) (sk : (ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ) : decodeBits4 (Turing.MultiTapeTM.dropFrame (F.encodeCramerShoupPublicKey d u sk)) = (u, F.encodeProjHashAux d sk.1.1 sk.1.2 u, F.encodeProjHashAux d sk.2.1.1 sk.2.1.2 u, F.encodeProjHashAux d sk.2.2.1 sk.2.2.2 u)

Extracting the 4-tuple of public-key group words from encodeCramerShoupPublicKey.

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeCramerShoupEncrypt_skNatOfZMod (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α σ τ σ₁ τ₁ σ₂ τ₂ : ZMod (F.order d)) (m : List Bool) (b : ℕ) : have u := F.encode d (α • F.generator d); have sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂; have pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂; F.encodeCramerShoupEncrypt H d (u, F.encodeProjHashAux d sk.1.1 sk.1.2 u, F.encodeProjHashAux d sk.2.1.1 sk.2.1.2 u, F.encodeProjHashAux d sk.2.2.1 sk.2.2.2 u) m b = F.encodeCramerShoupEncrypt H d (F.encode d pkVal.1, F.encode d pkVal.2.1, F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2) m (↑b).val

encodeCramerShoupEncrypt on the public-key words generated by skNatOfZMod agrees with cramerShoupPublicKey.