Cyclic Group Abstraction and the DDH Games

An abstract cyclic-group interface CyclicGroup G with explicit exponents, together with the group-theoretic Decisional Diffie–Hellman games DDH_real / DDH_ideal and the advantage DDH_Advantage.

This is the exponent-level DDH formulation used by discrete-log encryption schemes (e.g. Hashed ElGamal). It is distinct from the PairingGroup / DDHDef formulation in CatCryptCore.Examples.ElGamal and CatCryptCore.Crypto.Assumptions.DDH: here the group is presented abstractly with a bijective exponentiation pow : Exp → G, and the shared-secret operation elemPow is defined through the discrete logarithm.

Cyclic group interface

• G is a finite, nonempty type of group elements.
• Exp is a finite, nonempty type of exponents (Z_q where q = |G|).
• pow : Exp → G is exponentiation of the generator, assumed bijective.
• mul / inv / one give the group operation, inverse, and identity.
• expMul multiplies exponents; pow_comm records exponent commutativity.

DDH games

• DDH_real: sample a, b, output (g^a, g^b, g^(a·b)).
• DDH_ideal: sample a, b, c, output (g^a, g^b, g^c).
• DDH_Advantage: the distinguishing advantage between the two.

References

• [Boneh & Shoup, A Graduate Course in Applied Cryptography, Chapter 11]
• [SSProve: theories/Crypt/examples/PKE/ElGamal.v]

Cyclic Group Abstraction

class CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup (G : Type) : Type 1

A cyclic group structure with explicit exponents.

An abstract interface capturing the algebraic structure of a prime-order cyclic group: a bijective exponentiation pow : Exp → G, a commutative group operation, and exponent multiplication.

• Exp : Type

  The type of exponents (Z_q where q is the group order).

• finG : Fintype G

  G is finite.

• neG : Nonempty G

  G is nonempty.

• finExp : Fintype (Exp G)

  Exponents are finite.

• neExp : Nonempty (Exp G)

  Exponents are nonempty.

• gen : G

  The generator.

• pow : Exp G → G

  Exponentiation: g^a.

• mul : G → G → G

  Group multiplication.

• inv : G → G

  Group inverse.

• expMul : Exp G → Exp G → Exp G

  Exponent multiplication (in Z_q).

• expNeg : Exp G → Exp G

  Exponent negation (in Z_q).

• one : G

  Identity element.

• pow_comm (a b : Exp G) : pow (expMul a b) = pow (expMul b a)

  Exponent commutativity for pow.

• mul_assoc (x y z : G) : mul (mul x y) z = mul x (mul y z)

  Multiplication is associative.

• mul_comm (x y : G) : mul x y = mul y x

  Multiplication is commutative (in a cyclic group).

• mul_inv (x : G) : mul x (inv x) = one

  Right inverse: x * x⁻¹ = 1.

• mul_one (x : G) : mul x one = x

  Right identity: x * 1 = x.

• pow_bij : Function.Bijective pow

  Exponentiation is a bijection from Exp to G.

@[instance_reducible]

instance CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instMul {G : Type} [CG : CyclicGroup G] : Mul G

Notation for group multiplication.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instMul = { mul := CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.mul }

@[instance_reducible]

instance CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instInv {G : Type} [CG : CyclicGroup G] : Inv G

Notation for group inverse.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instInv = { inv := CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.inv }

@[instance_reducible]

instance CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instOne {G : Type} [CG : CyclicGroup G] : One G

Notation for identity.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.instOne = { one := CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.one }

@[reducible, inline]

abbrev CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.gPow {G : Type} [CG : CyclicGroup G] (a : Exp G) : G

g^a via coercion.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.gPow a = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow a

noncomputable def CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.elemPow {G : Type} [CG : CyclicGroup G] (x : G) (a : Exp G) : G

x^a for x : G using the discrete log and then exponentiating. Since pow is bijective, there is a unique exponent e with pow e = x; then x^a = pow (expMul e a).

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.elemPow x a = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul ⋯.choose a)

def CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.powNeg {G : Type} [CG : CyclicGroup G] (a : Exp G) : G

The inverse operation on exponents: g^(-a) = (g^a)⁻¹.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.powNeg a = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.inv (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow a)

theorem CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.elemPow_pow {G : Type} [CG : CyclicGroup G] (e a : Exp G) : elemPow (pow e) a = pow (expMul e a)

elemPow (pow e) a = pow (expMul e a): exponentiating g^e by a gives g^(e·a), from the definition of elemPow and the bijectivity of pow.

Decisional Diffie–Hellman (DDH) Games

The DDH assumption states that it is hard to distinguish (g^a, g^b, g^(ab)) for random a, b from (g^a, g^b, g^c) for random a, b, c.

@[reducible, inline]

abbrev CatCryptCore.Examples.CyclicGroupDDH.DDHTriple (G : Type) : Type

DDH triple type: (g^a, g^b, z) where z is either g^(ab) or g^c.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.DDHTriple G = (G × G × G)

noncomputable def CatCryptCore.Examples.CyclicGroupDDH.DDH_real (G : Type) [CG : CyclicGroup G] : CatCrypt.Core.SPComp (DDHTriple G)

Real DDH game: sample a, b and return (g^a, g^b, g^(ab)).

Equations

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

noncomputable def CatCryptCore.Examples.CyclicGroupDDH.DDH_ideal (G : Type) [CG : CyclicGroup G] : CatCrypt.Core.SPComp (DDHTriple G)

Ideal DDH game: sample a, b, c and return (g^a, g^b, g^c).

Equations

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

noncomputable def CatCryptCore.Examples.CyclicGroupDDH.DDH_Advantage (G : Type) [CG : CyclicGroup G] (A : DDHTriple G → CatCrypt.Core.SPComp Bool) : ENNReal

DDH advantage: the distinguishing advantage between real and ideal DDH games.

Equations

• CatCryptCore.Examples.CyclicGroupDDH.DDH_Advantage G A = CatCrypt.Crypto.AdvantageA (CatCryptCore.Examples.CyclicGroupDDH.DDH_real G) (CatCryptCore.Examples.CyclicGroupDDH.DDH_ideal G) A