Schnorr groups

A Schnorr group is the subgroup of prime order q of (ZMod p)ˣ, for a prime p, generated by a residue g of multiplicative order q. It is described by the triple (p, q, g) of binary numbers, and its elements are encoded by the binary digits of their residues. Multiplication and exponentiation are computed modulo p, by schoolbook multiplication and square-and-multiply. These groups form a PrimeOrderGroupFamily, so the discrete-logarithm assumption and the security theorems stated for such families apply to them.

A description is valid when p and q are prime, 1 < g < p and g ^ q % p = 1; these facts imply that g has order q and that q divides p - 1. Validity is part of the description type: algorithms receive only valid descriptions, and nothing here claims that valid descriptions can be generated efficiently.

Main definitions

• Cslib.Crypto.SchnorrGroup.Valid: valid descriptions (p, q, g).
• Cslib.Crypto.schnorrGroups: Schnorr groups as a PrimeOrderGroupFamily.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 10.4.
• C.-P. Schnorr, Efficient Signature Generation by Smart Cards

structure Cslib.Crypto.SchnorrGroup.Valid (d : ℕ × ℕ × ℕ) : Prop

A valid description (p, q, g) of a Schnorr group: p and q are prime, and the residue g satisfies 1 < g < p and g ^ q ≡ 1 (mod p).

• prime_modulus : Nat.Prime d.1

  The modulus is prime.

• prime_order : Nat.Prime d.2.1

  The group order is prime.

• one_lt_generator : 1 < d.2.2

  The generator is not 0 or 1.

• generator_lt : d.2.2 < d.1

  The generator is a reduced residue.

• generator_pow : d.2.2 ^ d.2.1 % d.1 = 1

  The generator has order dividing q.

@[reducible, inline]

abbrev Cslib.Crypto.SchnorrGroup.Desc : Type

Valid Schnorr-group descriptions.

def Cslib.Crypto.SchnorrGroup.generatorUnit (d : Desc) : (ZMod (↑d).1)ˣ

The generator as a unit modulo p.

@[reducible, inline]

abbrev Cslib.Crypto.SchnorrGroup.Carrier (d : Desc) : Type

The Schnorr group of a description, written additively.

instance Cslib.Crypto.SchnorrGroup.instFactPrimeFstNatSndProdValValid (d : Desc) : Fact (Nat.Prime (↑d).2.1)

theorem Cslib.Crypto.SchnorrGroup.generatorUnit_pow_order (d : Desc) : generatorUnit d ^ (↑d).2.1 = 1

The generator has order dividing q.

theorem Cslib.Crypto.SchnorrGroup.pow_order (d : Desc) (x : ↥(Subgroup.zpowers (generatorUnit d))) : x ^ (↑d).2.1 = 1

Every element of the Schnorr group has order dividing q.

@[instance_reducible]

instance Cslib.Crypto.SchnorrGroup.instModuleZModFstNatSndProdValValidCarrier (d : Desc) : Module (ZMod (↑d).2.1) (Carrier d)

instance Cslib.Crypto.SchnorrGroup.instNeZeroNatFstProdValValid (d : Desc) : NeZero (↑d).1

theorem Cslib.Crypto.SchnorrGroup.generatorUnit_ne_one (d : Desc) : generatorUnit d ≠ 1

The generator is not the identity.

def Cslib.Crypto.SchnorrGroup.generator (d : Desc) : Carrier d

The generator of the Schnorr group.

theorem Cslib.Crypto.SchnorrGroup.card_carrier (d : Desc) : Nat.card (Carrier d) = (↑d).2.1

The Schnorr group has q elements.

theorem Cslib.Crypto.SchnorrGroup.generator_ne_zero (d : Desc) : generator d ≠ 0

The generator is not the identity of the Schnorr group.

def Cslib.Crypto.SchnorrGroup.encode (d : Desc) (x : Carrier d) : List Bool

Elements are encoded by the binary digits of their residues modulo p.

theorem Cslib.Crypto.SchnorrGroup.encode_injective (d : Desc) : Function.Injective (encode d)

Distinct elements have distinct encodings.

def Cslib.Crypto.SchnorrGroup.add (input : Desc × List Bool × List Bool) : List Bool

Multiplication modulo p of encoded residues.

theorem Cslib.Crypto.SchnorrGroup.add_encode (d : Desc) (x y : Carrier d) : add (d, encode d x, encode d y) = encode d (x + y)

add multiplies encoded group elements.

def Cslib.Crypto.SchnorrGroup.smul (input : Desc × ℕ × List Bool) : List Bool

Exponentiation modulo p of an encoded residue.

theorem Cslib.Crypto.SchnorrGroup.smul_encode (d : Desc) (a : ℕ) (x : Carrier d) : smul (d, a, encode d x) = encode d (↑a • x)

smul raises encoded group elements to natural powers.

theorem Cslib.Crypto.SchnorrGroup.encode_generator (d : Desc) : encode d (generator d) = (↑d).2.2.bits

The encoded generator is the binary digits of g.

def Cslib.Crypto.SchnorrGroup.encDesc : Desc ↪ List Bool

Descriptions are encoded as the binary triple (p, q, g).

theorem Cslib.Crypto.SchnorrGroup.computableInPolyTime_order : Turing.MultiTapeTM.ComputableInPolyTime (fun (d : Desc) => (↑d).2.1) encDesc Turing.MultiTapeTM.encNat

The group order is computable in polynomial time from the description.

theorem Cslib.Crypto.SchnorrGroup.computableInPolyTime_generator : Turing.MultiTapeTM.ComputableInPolyTime (fun (d : Desc) => encode d (generator d)) encDesc Turing.MultiTapeTM.encBits

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

theorem Cslib.Crypto.SchnorrGroup.computableInPolyTime_add : Turing.MultiTapeTM.ComputableInPolyTime add (Turing.MultiTapeTM.encPair encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

Multiplication modulo p is computable in polynomial time.

theorem Cslib.Crypto.SchnorrGroup.computableInPolyTime_smul : Turing.MultiTapeTM.ComputableInPolyTime smul (Turing.MultiTapeTM.encPair encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

Exponentiation modulo p is computable in polynomial time, by square-and-multiply.

def Cslib.Crypto.schnorrGroups : PrimeOrderGroupFamily

Schnorr groups, the subgroups of prime order q of (ZMod p)ˣ, as a family of cyclic groups of prime order with efficient operations.