Formalizing Diffie-Hellman key exchange and Discrete Logarithms in Agda

Martin Hellman recently recounted that when he set out to solve cryptography’s biggest logistical nightmare, he was told it was impossible; when he solved it, he was told it was treason. He also spoke about his experiences advancing the field of public-key cryptography and the backlash he faced as an ardent digital privacy advocate. In this post, we dive deep into one of his key contributions, the Diffie-Hellman key exchange.

Diffie-Hellman is a key-exchange algorithm that allows two parties to establish a shared secret over an insecure channel. A symmetric encryption key can then be derived from that shared secret. The protocol relies on it being computationally infeasible to derive the shared secret from the public values when the parameters are chosen properly.

Much has been written and said about the algorithm. One popular explanation comes from Computerphile, which uses colour theory to illustrate it (this and this). Below is a brief reminder of how the algorithm works.

Alice and Bob — our trusty scene partners in cryptography skits — first agree on two public numbers: a large prime $p$ and a number $g$. They choose $g$ so that its powers produce many different values modulo $p$ instead of repeating after only a few steps. If they repeated too quickly, there would be too few possible public values, making the private exponents easier to recover. The number $g$ does not itself need to be prime. In practice, implementations use a standardized, publicly reviewed pair $(p, g)$ rather than generating these values themselves. Alice and Bob then choose large random private exponents $a$ and $b$, respectively. Alice publishes $A = g^a \bmod p$, and Bob publishes $B = g^b \bmod p$. Formalizing modular exponentiation in Agda, we have the following:

-- Function to calculate the modulus of an exponentiation
mod-exp : (p : ℕ) → .{{_ : NonZero p}} → ℕ → ℕ → ℕ
mod-exp p base exponent = (base ^ exponent) % p

public-value : (p : ℕ) → .{{_ : NonZero p}} → ℕ → ℕ → ℕ
public-value p g private-exponent = mod-exp p g private-exponent

Alice and Bob exchange the public values $A$ and $B$. Alice now knows only her private exponent $a$ and Bob’s public value $B$, while Bob knows only his private exponent $b$ and Alice’s public value $A$. Alice computes $B^a \bmod p$, while Bob computes $A^b \bmod p$:

alice-shared-secret : (p : ℕ) → {{_ : NonZero p}} → (a bob-public : ℕ) → ℕ
alice-shared-secret p a bob-public = mod-exp p bob-public a

bob-shared-secret : (p : ℕ) → {{_ : NonZero p}} → (b alice-public : ℕ) → ℕ
bob-shared-secret p b alice-public = mod-exp p alice-public b

For a small example, let $p = 5$ and $g = 2$. Alice chooses $a = 2$ and publishes $A = 2^2 \bmod 5 = 4$. Bob chooses $b = 3$ and publishes $B = 2^3 \bmod 5 = 3$. They then calculate:

• Alice: $B^a \bmod p = 3^2 \bmod 5 = 4$
• Bob: $A^b \bmod p = 4^3 \bmod 5 = 4$

Both arrive at the shared secret $4$. Agda can verify these calculations by normalization:

alice-shared-secret-example : alice-shared-secret 5 2 3 ≡ 4
alice-shared-secret-example = refl

bob-shared-secret-example : bob-shared-secret 5 3 4 ≡ 4
bob-shared-secret-example = refl

Note: The complete Agda code can be found here.

Agda notation: {{...}} marks an instance argument that Agda can fill in automatically, while the dot in .{{...}} marks it as irrelevant to the computed result.

Both parties arrive at the same value, crucially due to the commutativity of multiplication: $B^a \bmod p = g^{ba} \bmod p$ and $A^b \bmod p = g^{ab} \bmod p$. Given only the public values, recovering the private exponents $a$ and $b$ requires solving the discrete-logarithm problem, which is computationally infeasible for properly chosen parameters. Recovering either exponent would let an attacker compute the shared secret.

An attacker can see the public values $A = g^a \bmod p$ and $B = g^b \bmod p$. Multiplying and reducing them gives $AB \bmod p = g^{a+b} \bmod p$, whereas the shared secret is $g^{ab} \bmod p$. The security of the protocol relies on it being computationally infeasible to obtain $g^{ab} \bmod p$ from the two public values when the parameters are chosen properly.

This protects against someone who only observes the exchange, but not against an active attacker who replaces the public values and establishes separate secrets with Alice and Bob. Practical protocols therefore authenticate the exchange, for example with digital signatures.

The full proof of the equality of the shared secrets computed by Alice and Bob is below:

We start with a lemma stating that $(x \bmod p)^n \bmod p = x^n \bmod p$. It is proven below with equational reasoning in Agda.

Key steps: %-distribˡ-* reduces both factors of the product modulo $p$. Then m%n%n≡m%n removes the repeated reduction of $x$, and the induction hypothesis handles the remaining power.

mod-exp-reduce-base : (p x n : ℕ) → .{{_ : NonZero p}} → mod-exp p (x % p) n ≡ mod-exp p x n
mod-exp-reduce-base p x ℕ.zero = refl
mod-exp-reduce-base p x (ℕ.suc n) = begin
    mod-exp p (x % p) (ℕ.suc n)
        ≡⟨ refl ⟩
    ((x % p) * ((x % p) ^ n)) % p
        ≡⟨ %-distribˡ-* (x % p) ((x % p) ^ n) p ⟩
    (((x % p) % p) * (((x % p) ^ n) % p)) % p
        ≡⟨ cong (λ k → (k * (((x % p) ^ n) % p)) % p) (m%n%n≡m%n x p) ⟩
    ((x % p) * (((x % p) ^ n) % p)) % p
        ≡⟨ cong (λ k → ((x % p) * k) % p) (mod-exp-reduce-base p x n) ⟩
    ((x % p) * ((x ^ n) % p)) % p
        ≡⟨ sym (%-distribˡ-* x (x ^ n) p) ⟩
    (x * (x ^ n)) % p
        ≡⟨ refl ⟩
    mod-exp p x (ℕ.suc n)
    ∎

And the final proof that the shared secret that Alice and Bob arrive at is the same:

Key steps: Unfolding public-value and alice-shared-secret produces Alice’s calculation. Then mod-exp-reduce-base removes the inner modulo operation, ^-*-assoc combines the nested powers, and *-comm changes the exponent from $ba$ to $ab$. Reversing these steps produces Bob’s calculation.

diffie-hellman-key-exchange : (p : ℕ) → {{_ : NonZero p}} → (g a b : ℕ) →
    alice-shared-secret p a (public-value p g b) ≡
    bob-shared-secret p b (public-value p g a)
diffie-hellman-key-exchange p g a b = begin
    alice-shared-secret p a (public-value p g b)
        ≡⟨ refl ⟩
    mod-exp p (mod-exp p g b) a
        ≡⟨ mod-exp-reduce-base p (g ^ b) a ⟩
    mod-exp p (g ^ b) a
        ≡⟨ cong (λ k → k % p) (^-*-assoc g b a) ⟩
    (g ^ (b * a)) % p
        ≡⟨ cong (λ k → (g ^ k) % p) (*-comm b a) ⟩
    (g ^ (a * b)) % p
        ≡⟨ cong (λ k → k % p) (sym (^-*-assoc g a b)) ⟩
    mod-exp p (g ^ a) b
        ≡⟨ sym (mod-exp-reduce-base p (g ^ a) b) ⟩
    mod-exp p (mod-exp p g a) b
        ≡⟨ refl ⟩
    bob-shared-secret p b (public-value p g a)
    ∎ 

The proof above establishes correctness: Alice and Bob arrive at the same shared secret. We now turn to the security question of why their public values do not reveal their private exponents.

The Discrete Logarithm Problem

This is the difficult problem mentioned earlier: given $g^a \bmod p$, recover $a$. A proposed answer can be checked efficiently, but no efficient classical algorithm is known for finding one when the parameters are chosen properly. A sufficiently powerful quantum computer could solve it efficiently using Shor’s algorithm.

This difficulty is what supports the security of the key exchange. The Agda proof below does not formalize computational difficulty; instead, it proves the uniqueness part of the problem: for a primitive root $g$ of a prime $p$, no two exponents between $0$ and $p - 2$ produce the same value. Equivalently, the discrete logarithm is unique modulo $p - 1$. More generally, the problem is stated as follows:

If $\alpha$ is an arbitrary integer relatively prime to $n$ and $g$ is a primitive root of $n$, then among the numbers $0, 1, 2, \ldots, \phi(n) - 1$, where $\phi(n)$ is the totient function, there is exactly one number $\mu$ such that $\alpha \equiv g^\mu \pmod n$.

Explaining the definition in detail:

• Relatively prime implies that the common factor between two numbers is only 1.
• Primitive root: A primitive root of a prime $p$ is an integer $g$ whose multiplicative order modulo $p$ is $p - 1$.
  • Multiplicative order of $b \bmod n$: The smallest positive exponent $e$ for which $b^e \equiv 1 \pmod n$.
• Totient function: The number of positive integers $\leq n$ that are relatively prime to $n$.

Formalizing the above in Agda, we get:

Multiplicative order:

record MultiplicativeOrder (a p k : ℕ) : Set where
    constructor multiplicative-order
    field
        {{p≢0}} : NonZero p
        {{k≢0}} : NonZero k
        power1 : mod-exp p a k ≡ 1
        minimal : ∀ {k′} → {{_ : NonZero k′}} → k′ < k → mod-exp p a k′ ≢ 1

Totient function:

totientRecursive : (n rec : ℕ) → .{{_ : NonZero n}} → ℕ
totientRecursive n ℕ.zero = 0
totientRecursive n (ℕ.suc rec) with gcd (ℕ.suc rec) n
... | 1 = suc (totientRecursive n rec)
... | _ = totientRecursive n rec

totient : (n : ℕ) → .{{_ : NonZero n}} → ℕ
totient (ℕ.suc ℕ.zero) = 1
totient (ℕ.suc n) = totientRecursive (ℕ.suc n) (n)

Primitive root:

record PrimitiveRoot (p g : ℕ) : Set where
    constructor primitiveRoot
    field
        {{p≢0}} : NonZero p
        p-prime : Prime p
        order-max : MultiplicativeOrder g p (totient p)

And some examples:

• The multiplicative order of $2 \bmod 5$ is $4$ since the smallest number for which $2^x \bmod 5 = 1$ is $4$.
  • $2^1 \bmod 5 = 2$
  • $2^2 \bmod 5 = 4$
  • $2^3 \bmod 5 = 3$
  • $2^4 \bmod 5 = 1$
• The totient of $5$ is $4$ since $5$ is a prime number.
• Finally, $2$ is a primitive root of $5$ since $2 \bmod 5$ has the multiplicative order $5 - 1$.

multiplicative-order-2-mod-5 : MultiplicativeOrder 2 5 4
multiplicative-order-2-mod-5 = multiplicative-order refl λ
    { {1} _ ()
    ; {2} _ ()
    ; {3} _ ()
    ; {suc (suc (suc (suc _)))} (s≤s (s≤s (s≤s (s≤s ()))))
    }

totient5 : totient 5 ≡ 4
totient5 = refl

prime-5 : Prime 5
prime-5 = from-yes (prime? 5)

primitive-root-2-mod-5 : PrimitiveRoot 5 2
primitive-root-2-mod-5 rewrite totient5 = primitiveRoot prime-5 multiplicative-order-2-mod-5

Now that we have all the definitions in place, we will prove the uniqueness part of the discrete logarithm definition:

exactly one number $\mu$ such that $\alpha \equiv g^\mu \pmod n$

The Agda theorem expresses uniqueness modulo $\phi(p)$. For two distinct exponents $\mu$ and $\mu’$, such that $\mu < \mu’$, if they produce the same value, then they have the same remainder after division by $\phi(p)$:

discrete-log-unique :
    (g p : ℕ) → 
    (root : PrimitiveRoot p g) →
    ∀ {μ μ′} →
    μ < μ′ →
    mod-exp p g μ ≡ mod-exp p g μ′ →
    μ % totient p ≡ μ′ % totient p

Since $\phi(p) = p - 1$ for prime $p$, no two distinct exponents between $0$ and $p - 2$ can produce the same power.

The proof proceeds in four steps:

1. Powers repeat after every multiple of the multiplicative order $k$.
2. If $a^x \bmod p = 1$, then $k$ divides $x$.
3. If two powers are equal, raising $a$ to the difference of their exponents gives $1$ modulo $p$.
4. Therefore, $k$ divides that difference, so the exponents have the same remainder when divided by $k$.

We establish each step with the following helper lemmas.

Proving uniqueness modulo the multiplicative order

We start with this lemma: Given natural numbers $a, p, k$ where $k$ is the multiplicative order of $a \bmod p$, we have for all values of $r$ and $q$: $a^{r+qk} \equiv a^r \pmod p$.

Key steps: ^-distribˡ-+-* splits $a^{r+qk}$ into $a^r a^{qk}$. After *-comm changes $qk$ to $kq$, ^-*-assoc rewrites the second factor as $(a^k)^q$. The power1 field then replaces $a^k \bmod p$ with $1$.

mod-exp-periodic : (a p k : ℕ) → {{_ : MultiplicativeOrder a p k}} →
  ∀ r q → mod-exp p a (r + q * k) ≡ mod-exp p a r
mod-exp-periodic a p k {{order}} r q = begin 
    mod-exp p a (r + q * k)
        ≡⟨ refl ⟩
    a ^ (r + q * k) % p
        ≡⟨ cong (λ x → x % p) (^-distribˡ-+-* a r (q * k)) ⟩
    a ^ r * a ^ (q * k) % p
        ≡⟨ cong (λ x → a ^ r * a ^ x % p) (*-comm q k) ⟩
    a ^ r * a ^ (k * q) % p
        ≡⟨ cong (λ x → (a ^ r * x) % p) (sym (^-*-assoc a k q)) ⟩
    (a ^ r * (a ^ k) ^ q) % p
        ≡⟨ %-distribˡ-* (a ^ r) ((a ^ k) ^ q) p ⟩
    ((a ^ r % p) * (((a ^ k) ^ q) % p)) % p
        ≡⟨ cong (λ x → ((a ^ r % p) * x) % p) (sym (mod-exp-reduce-base p (a ^ k) q)) ⟩
    ((a ^ r % p) * ((((a ^ k) % p) ^ q) % p)) % p
        ≡⟨ cong (λ x → ((a ^ r % p) * ((x ^ q) % p)) % p) (MultiplicativeOrder.power1 order) ⟩
    ((a ^ r % p) * (1 ^ q % p)) % p
        ≡⟨ cong (λ x → ((a ^ r % p) * x) % p) (cong (λ x → x % p) (^-zeroˡ q)) ⟩
    ((a ^ r % p) * (1 % p)) % p
        ≡⟨ sym (%-distribˡ-* (a ^ r) 1 p) ⟩
    (a ^ r * 1) % p
        ≡⟨ cong (λ x → x % p) (*-identityʳ (a ^ r)) ⟩
    (a ^ r) % p
        ≡⟨ refl ⟩
    mod-exp p a r
    ∎

Given the same multiplicative order $k$ of $a \bmod p$, if $a^{k’} \bmod p = 1$ then $k$ divides $k’$.

Key steps: mod-exp-periodic and the division algorithm show that $a^{k’ \bmod k} \bmod p = 1$. If this remainder were non-zero, m%n<n and the minimal field would contradict the minimality of $k$; hence the remainder is zero.

mod-exp≡1⇒order|x : (a p k : ℕ) → {{_ : MultiplicativeOrder a p k}} →
    (∀ {k′} → {{_ : NonZero k′}} →
    mod-exp p a k′ ≡ 1 → k ∣ k′)
mod-exp≡1⇒order|x a p k {{order}} {k′} mod-exp_pak′
    with k′ % k in k′%k
... | ℕ.zero = m%n≡0⇒n∣m k′ k k′%k
... | suc r = contradiction
                (subst (λ x → mod-exp p a x ≡ 1) k′%k remainder-power1)
                (MultiplicativeOrder.minimal order
                    (subst (_< k) k′%k (m%n<n k′ k)))
  where
    remainder-power1 : mod-exp p a (k′ % k) ≡ 1
    remainder-power1 = begin
        mod-exp p a (k′ % k)
            ≡⟨ sym (mod-exp-periodic a p k (k′ % k) (k′ / k)) ⟩
        mod-exp p a (k′ % k + (k′ / k) * k)
            ≡⟨ cong (mod-exp p a) (sym (m≡m%n+[m/n]*n k′ k)) ⟩
        mod-exp p a k′
            ≡⟨ mod-exp_pak′ ⟩
        1
        ∎

The corollary of the above: Given the multiplicative order $k$ of $a \bmod p$, if $k$ divides some $k’$, then $a^{k’} \bmod p = 1$.

Key steps: The divisibility witness rewrites $k’$ as $qk$. Then mod-exp-periodic removes this multiple of the order, and power1 supplies the final value $1$.

order|k′⇒mod-exp≡1 : (a p k k′ : ℕ) → {{_ : MultiplicativeOrder a p k}} →
    k ∣ k′ → mod-exp p a k′ ≡ 1
order|k′⇒mod-exp≡1 a p k k′ {{order}} (divides q k′≡q*k) = begin
    mod-exp p a k′
        ≡⟨ cong (mod-exp p a) k′≡q*k ⟩
    mod-exp p a (q * k)
        ≡⟨ mod-exp-periodic a p k 0 q ⟩
    mod-exp p a 0
        ≡⟨ sym (mod-exp-periodic a p k 0 1) ⟩
    mod-exp p a (0 + 1 * k)
        ≡⟨ cong (mod-exp p a) (+-identityʳ k) ⟩
    mod-exp p a k
        ≡⟨ MultiplicativeOrder.power1 order ⟩
    1
    ∎

A simple one: $a^{x+y} \bmod p$ equals $((a^x \bmod p) \cdot (a^y \bmod p)) \bmod p$.

Key steps: ^-distribˡ-+-* changes $a^{x+y}$ into $a^x a^y$, and %-distribˡ-* reduces the two factors separately modulo $p$.

mod-exp-add : (a p x y : ℕ) → {{_ : NonZero p}} →
    mod-exp p a (x + y) ≡ (mod-exp p a x * mod-exp p a y) % p
mod-exp-add a p x y = begin
    mod-exp p a (x + y)
        ≡⟨ cong (_% p) (^-distribˡ-+-* a x y) ⟩
    (a ^ x * a ^ y) % p
        ≡⟨ %-distribˡ-* (a ^ x) (a ^ y) p ⟩
    (mod-exp p a x * mod-exp p a y) % p
    ∎

Another simple one: if a non-zero number $d$ divides the difference between $n$ and $m$ (assume $m < n$), then $m \bmod d = n \bmod d$.

Key steps: m+[n∸m]≡n rewrites $n$ as $m+(n-m)$, and %-distribˡ-+ separates the remainders. Then n∣m⇒m%n≡0 turns the divisible difference into remainder $0$.

d|n∸m⇒m%d≡n%d :
    (m n d : ℕ) → {{_ : NonZero d}} →
    m < n →
    d ∣ (n ∸ m) →
    m % d ≡ n % d
d|n∸m⇒m%d≡n%d m n d m<n d∣n∸m = sym (begin
    n % d
        ≡⟨ cong (_% d) (sym (m+[n∸m]≡n (<⇒≤ m<n))) ⟩
    (m + (n ∸ m)) % d
        ≡⟨ %-distribˡ-+ m (n ∸ m) d ⟩
    ((m % d) + ((n ∸ m) % d)) % d
        ≡⟨ cong (λ x → ((m % d) + x) % d) (n∣m⇒m%n≡0 (n ∸ m) d d∣n∸m) ⟩
    ((m % d) + 0) % d
        ≡⟨ cong (_% d) (+-identityʳ (m % d)) ⟩
    (m % d) % d
        ≡⟨ m%n%n≡m%n m d ⟩
    m % d
    ∎)

The final helper lemma captures modular cancellation. Informally, from $a^\mu \bmod p = a^{\mu’} \bmod p$, we want to cancel $a^\mu$ and conclude that $a^{\mu’-\mu} \bmod p = 1$. Rather than introduce modular inverses, the proof uses periodicity to add $\mu k$ to the exponent, substitutes the equality of the two reduced powers, and recombines them into $a^{\mu k}$. Since $k$ divides $\mu k$, we have $a^{\mu k} \bmod p = 1$. This was the lemma I had the most fun proving:

modular-cancellation :
    (a p k μ μ′ : ℕ) → {{_ : MultiplicativeOrder a p k}} →
    μ < μ′ →
    mod-exp p a μ ≡ mod-exp p a μ′ →
    mod-exp p a (μ′ ∸ μ) ≡ 1
modular-cancellation a p k μ μ′ {{order}} μ<μ′ eq-mod-exp = begin 
    mod-exp p a (μ′ ∸ μ)
        ≡⟨ sym (mod-exp-periodic a p k (μ′ ∸ μ) μ) ⟩
    mod-exp p a ((μ′ ∸ μ) + μ * k)
        ≡⟨ cong (mod-exp p a) (sym (+-∸-comm (μ * k) (<⇒≤ μ<μ′))) ⟩
    mod-exp p a (μ′ + μ * k ∸ μ)
        ≡⟨ cong (mod-exp p a) (+-∸-assoc μ′ (m≤m*n μ k)) ⟩
    mod-exp p a (μ′ + (μ * k ∸ μ))
        ≡⟨ mod-exp-add a p μ′ (μ * k ∸ μ) ⟩
    ((mod-exp p a μ′) * (mod-exp p a (μ * k ∸ μ))) % p
        ≡⟨ cong (λ x → (x * mod-exp p a (μ * k ∸ μ)) % p) (sym eq-mod-exp) ⟩
    ((mod-exp p a μ) * (mod-exp p a (μ * k ∸ μ))) % p
        ≡⟨ sym (mod-exp-add a p μ (μ * k ∸ μ)) ⟩
    (mod-exp p a (μ + (μ * k ∸ μ)))
        ≡⟨ cong (mod-exp p a) (m+[n∸m]≡n (m≤m*n μ k)) ⟩
    (mod-exp p a (μ * k))
        ≡⟨ order|k′⇒mod-exp≡1 a p k (μ * k) {{order}} (n∣m*n μ) ⟩
    1
    ∎

Final proof of uniqueness modulo the totient

Now that we have all the required lemmas, the final proof that equal powers give equal exponent remainders modulo $\phi(p)$ is succinct:

Key steps: modular-cancellation shows that $g^{\mu’-\mu} \bmod p = 1$. Using the multiplicative order $\phi(p)$ supplied by the primitive root, mod-exp≡1⇒order|x proves that $\phi(p)$ divides the exponent difference. Finally, d|n∸m⇒m%d≡n%d gives equality of the two remainders.

discrete-log-unique :
    (g p : ℕ) → 
    (root : PrimitiveRoot p g) →
    ∀ {μ μ′} →
    μ < μ′ →
    mod-exp p g μ ≡ mod-exp p g μ′ →
    μ % totient p ≡ μ′ % totient p
discrete-log-unique g p root {μ} {μ′} μ<μ' eq-mod-exp = d|n∸m⇒m%d≡n%d μ μ′ (totient p) μ<μ'
    (mod-exp≡1⇒order|x g p (totient p) {{root .PrimitiveRoot.order-max}} {μ′ ∸ μ} {{ >-nonZero (m<n⇒0<n∸m μ<μ')}}
        (modular-cancellation g p (totient p) μ  μ′ {{root .PrimitiveRoot.order-max}} μ<μ' eq-mod-exp))

Together, these proofs establish that Alice and Bob compute the same shared secret and that if two distinct exponents produce equal powers modulo $p$, the exponents have the same remainder when divided by $\phi(p)$.

Even if $g$ is a primitive root of $p$, the Pohlig-Hellman algorithm makes the discrete logarithm easier when $p - 1$ factors into small primes. A common defence is to choose a safe prime $p = 2q + 1$, where $q$ is also a large prime. Then the only prime factors of $p - 1$ are $2$ and $q$, so Pohlig-Hellman cannot reduce the problem to many small ones. Most modern software instead uses an elliptic-curve version of Diffie-Hellman. The next post will continue from here!