Diffie–Hellman key exchange

DefinitionGroup exponentiation with modular exponents#✓fully proved

Let \(G\) be a group, \(q\) a natural number, \(g \in G\) and \(a \in \mathbb{Z}/q\mathbb{Z}\). Then \(g^a\) is defined as \(g^n\), where \(n\) is the natural-number value of \(a\): its representative in \(\{0, \dots, q-1\}\) when \(q > 0\), and \(|a|\) when \(q = 0\) (in which case \(\mathbb{Z}/q\mathbb{Z} = \mathbb{Z}\)).

def gpow (g : G) (a : ZMod q) : G := g ^ a.val

Used by 16

Used byCorrectness of Diffie–Hellman key agreement · Value of the Diffie–Hellman shared key · Random DDH experiment · The reduction is a fair coin on random DDH triples · Real DDH experiment · ElGamal decryption · Correctness of ElGamal · ElGamal eavesdropping game equals the real DDH experiment of the reduction · ElGamal encryption · ElGamal public key · Schnorr verifier's acceptance condition · Completeness of the Schnorr identification scheme · Special soundness · Honest Schnorr transcript · Simulated Schnorr transcript · Perfect honest-verifier zero knowledge

TheoremCorrectness of Diffie–Hellman key agreement#✓fully proved

Let \(G\) be a group, \(q\) a natural number and \(g \in G\). For \(x \in G\) and \(c \in \mathbb{Z}/q\mathbb{Z}\) write \(x^c\) for \(x^n\), where \(n\) is the natural-number value of \(c\): its representative in \(\{0, \dots, q-1\}\) when \(q > 0\), and \(|c|\) when \(q = 0\) (in which case \(\mathbb{Z}/q\mathbb{Z} = \mathbb{Z}\)). Then \((g^b)^a = (g^a)^b\) for all \(a, b \in \mathbb{Z}/q\mathbb{Z}\).

theorem dh_agree (g : G) (a b : ZMod q) : gpow (gpow g b) a = gpow (gpow g a) b

Uses 1 · Used by 2

Statement usesGroup exponentiation with modular exponents

Used byValue of the Diffie–Hellman shared key · Correctness of ElGamal

TheoremValue of the Diffie–Hellman shared key#✓fully proved

Let \(G\) be a group, \(q\) a natural number and \(g \in G\) with \(g^q = 1\). For \(x \in G\) and \(c \in \mathbb{Z}/q\mathbb{Z}\) write \(x^c\) for \(x^n\), where \(n\) is the natural-number value of \(c\): its representative in \(\{0, \dots, q-1\}\) when \(q > 0\), and \(|c|\) when \(q = 0\) (in which case \(\mathbb{Z}/q\mathbb{Z} = \mathbb{Z}\)). Then \((g^b)^a = g^{ab}\) for all \(a, b \in \mathbb{Z}/q\mathbb{Z}\), where \(ab\) is the product in \(\mathbb{Z}/q\mathbb{Z}\).

theorem dh_key_eq {g : G} (hg : g ^ q = 1) (a b : ZMod q) :
    gpow (gpow g b) a = gpow g (a * b)

Uses 2

Statement usesGroup exponentiation with modular exponents

Proof usesCorrectness of Diffie–Hellman key agreement

DefinitionExponentiation from a generator is a bijection#✓fully proved

Let \(G\) be a finite group of order \(q\), with \(q \neq 0\), and let \(g \in G\) generate \(G\), that is, every element of \(G\) is an integer power of \(g\). Then \(a \mapsto g^a\) is a bijection from \(\mathbb{Z}/q\mathbb{Z}\) to \(G\), where \(g^a = g^n\) for the representative \(n \in \{0, \dots, q-1\}\) of \(a\). Its inverse is the discrete logarithm to base \(g\).

noncomputable def gpowEquiv (hgen : ∀ x : G, x ∈ Subgroup.zpowers g)
    (hcard : Fintype.card G = q) : ZMod q ≃ G :=
  Multiplicative.ofAdd.trans
    (zmodMulEquivOfGenerator hgen (Nat.card_eq_fintype_card.trans hcard)).toEquiv

Used by 1

Used byThe reduction is a fair coin on random DDH triples

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.