The discrete-logarithm assumption

A PrimeOrderGroupFamily is a family of cyclic groups of prime order, indexed by public descriptions such as (p, q, g) for the subgroup of order q of (ZMod p)ˣ generated by g. Groups are written additively, as ZMod q-modules, so the book's g ^ α is α • g. Algorithms see a group through its description and the words encoding its elements. The family supplies exactly the operations that algorithms using it need, as plain polynomial-time functions of the description and the encoded operands: the order, the encoded generator, addition, and multiplication by a natural number.

The discrete-logarithm experiment ([BS23], Attack Game 10.4) draws a description from a setup law, a uniform α : ZMod q and gives the adversary the description and the encoding of α • g; the adversary wins when the binary number it outputs is α modulo q. DiscreteLog asserts that every uniform strict PPT adversary wins with negligible probability.

As for DecisionLWE, this is a hypothesis, not a theorem. The setup law is arbitrary and is not claimed to be efficiently sampleable: generating primes with certainty is not a strict PPT task, since a fair-coin machine with a fixed clock fails with positive probability. Descriptions are public, and an adversary's running time may depend on their length.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily: cyclic groups of prime order with efficient operations.
• Cslib.Crypto.PrimeOrderGroupFamily.discreteLogGame: the discrete-logarithm experiment.
• Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog: the discrete-logarithm assumption.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_injective: a discrete logarithm modulo q is unique.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 10.5.

structure Cslib.Crypto.PrimeOrderGroupFamily : Type 1

A family of cyclic groups of prime order, indexed by public descriptions, with polynomial-time operations on encoded elements.

• Desc : Type

  Public descriptions of the groups.

• encDesc : self.Desc ↪ List Bool

  The encoding of descriptions given to algorithms.

• order : self.Desc → ℕ

  The order of each group.

• prime_order (d : self.Desc) : Nat.Prime (self.order d)

  Every order is prime.

• Carrier : self.Desc → Type

  The groups, written additively.

• addCommGroup (d : self.Desc) : AddCommGroup (self.Carrier d)

  Each group is commutative.

• module (d : self.Desc) : Module (ZMod (self.order d)) (self.Carrier d)

  Each group is a ZMod q-module, where q is its order.

• generator (d : self.Desc) : self.Carrier d

  The generator of each group.

• card_carrier (d : self.Desc) : Nat.card (self.Carrier d) = self.order d

  Each group has q elements.

• generator_ne_zero (d : self.Desc) : self.generator d ≠ 0

  The generator is not the identity, so it generates the group of prime order.

• encode (d : self.Desc) : self.Carrier d → List Bool

  Group elements as words.

• encode_injective (d : self.Desc) : Function.Injective (self.encode d)

  Distinct elements have distinct encodings.

• add : self.Desc × List Bool × List Bool → List Bool

  Addition of encoded elements.

• add_encode (d : self.Desc) (x y : self.Carrier d) : self.add (d, self.encode d x, self.encode d y) = self.encode d (x + y)

  add adds encoded elements.

• smul : self.Desc × ℕ × List Bool → List Bool

  Multiplication of an encoded element by a natural number.

• smul_encode (d : self.Desc) (a : ℕ) (x : self.Carrier d) : self.smul (d, a, self.encode d x) = self.encode d (↑a • x)

  smul multiplies encoded elements by natural numbers.

• computableInPolyTime_order : Turing.MultiTapeTM.ComputableInPolyTime self.order self.encDesc Turing.MultiTapeTM.encNat

  The order is computable in polynomial time from the description.

• computableInPolyTime_generator : Turing.MultiTapeTM.ComputableInPolyTime (fun (d : self.Desc) => self.encode d (self.generator d)) self.encDesc Turing.MultiTapeTM.encBits

  The encoded generator is computable in polynomial time from the description.

• computableInPolyTime_add : Turing.MultiTapeTM.ComputableInPolyTime self.add (Turing.MultiTapeTM.encPair self.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

  Addition is computable in polynomial time.

• computableInPolyTime_smul : Turing.MultiTapeTM.ComputableInPolyTime self.smul (Turing.MultiTapeTM.encPair self.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

  Multiplication by a binary natural number is computable in polynomial time.

instance Cslib.Crypto.PrimeOrderGroupFamily.instFactPrimeOrder (F : PrimeOrderGroupFamily) (d : F.Desc) : Fact (Nat.Prime (F.order d))

instance Cslib.Crypto.PrimeOrderGroupFamily.instNeZeroNatOrder (F : PrimeOrderGroupFamily) (d : F.Desc) : NeZero (F.order d)

theorem Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_injective (F : PrimeOrderGroupFamily) (d : F.Desc) : Function.Injective fun (α : ZMod (F.order d)) => α • F.generator d

A discrete logarithm modulo q is unique: α ↦ α • g is injective.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.discreteLogGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)) (n : ℕ) : Game

The discrete-logarithm experiment ([BS23], Attack Game 10.4): draw a description and a uniform α, give the adversary the description and the encoding of α • g, and accept when the binary number it outputs is α modulo q.

def Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) : Prop

The discrete-logarithm assumption for a family and a setup law: every uniform strict PPT adversary, given the unary security parameter, the description and the encoded instance, finds the discrete logarithm with negligible probability. This is a hypothesis, not a theorem.