Cryptography

Diffie–Hellman: a shared secret

Run both sides of a key exchange and prove they arrive at the same residue.

-- Diffie–Hellman: a shared secret
-- History: 1976 · Diffie and Hellman.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Both participants arrive at g^(ab) even though they exchange only g^a and g^b.
-- Scope: Checks one exchange modulo 23 with known example secrets. It demonstrates agreement, not cryptographic security. Do not use these parameters for protection.
-- Source: https://www-ee.stanford.edu/~hellman/publications/24.pdf

def publicKey (secret : Nat) : Fin 23 := (5 : Fin 23)^secret

def aliceSecret := 6
def bobSecret := 15

def aliceShared := (publicKey bobSecret)^aliceSecret
def bobShared := (publicKey aliceSecret)^bobSecret

theorem agreement : aliceShared = bobShared := by decide

def main : IO Unit := do
  IO.println s!"Alice sends {publicKey aliceSecret}"
  IO.println s!"Bob sends {publicKey bobSecret}"
  IO.println s!"Alice gets {aliceShared}"
  IO.println s!"Bob gets {bobShared}"

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

`Fin n`

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

1976 · Diffie and Hellman

Both participants arrive at g^(ab) even though they exchange only g^a and g^b.

Checks one exchange modulo 23 with known example secrets. It demonstrates agreement, not cryptographic security. Do not use these parameters for protection.

New Directions in Cryptography (1976)

Expected output

Reference only. Run the file to check its actual result.

Alice sends 8
Bob sends 19
Alice gets 2
Bob gets 2

Exercise

Change the two secrets and rerun. With such tiny numbers, can you recover a secret by exhaustive search?