From 39b20803d4c09a9ef8eab9b0027be425510f4f49 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Mon, 6 Apr 2026 17:55:33 -0300 Subject: [PATCH 1/2] feat(Protocols): Key exchange protocols and Diffie-Hellman Add KeyExchangeProtocol class with agreement property and Diffie-Hellman as an instance over commutative groups. --- Cslib.lean | 2 + .../Cryptographic/KeyExchange/Basic.lean | 48 +++++++++ .../KeyExchange/Diffie-Hellman.lean | 99 +++++++++++++++++++ 3 files changed, 149 insertions(+) create mode 100644 Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean create mode 100644 Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean diff --git a/Cslib.lean b/Cslib.lean index 7db43680b..54e3e317a 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -122,6 +122,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic +public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic +public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Diffie-Hellman public import Cslib.Logics.HML.Basic public import Cslib.Logics.HML.LogicalEquivalence public import Cslib.Logics.LinearLogic.CLL.Basic diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean new file mode 100644 index 000000000..aea7e8728 --- /dev/null +++ b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Christiano Braga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christiano Braga +-/ + +module + +public import Mathlib.Tactic + +@[expose] public section + +/-! +# Key Exchange Protocol + +A *key exchange protocol* allows two parties (Alice and Bob) to establish a shared secret +over an insecure channel. + +The protocol proceeds as follows: + +1. Alice picks a private key α, computes her public value pub(α), and sends it to Bob. +2. Bob picks a private key β, computes his public value pub(β), and sends it to Alice. +3. Alice computes the shared secret as sharedSecret(pub(β), α). +4. Bob computes the shared secret as sharedSecret(pub(α), β). + +The fundamental correctness property (*agreement*) states that both parties compute the same +shared secret: + + sharedSecret(pub(β), α) = sharedSecret(pub(α), β) + +Reference: + +* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*][BonehShoup], + Section 10.4. +-/ + +universe u v w + +class KeyExchangeProtocol + (PrivateKey : Type u) (PublicValue : Type v) + (SharedSecret : Type w) where + /-- Compute public value from private key. This is sent to the other party. -/ + pub : PrivateKey → PublicValue + /-- Compute shared secret from received public value and own private key. -/ + sharedSecret : PublicValue → PrivateKey → SharedSecret + /-- Agreement: both parties compute the same shared secret. -/ + agreement : ∀ (α β : PrivateKey), + sharedSecret (pub β) α = sharedSecret (pub α) β diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean new file mode 100644 index 000000000..29d70c0c5 --- /dev/null +++ b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Christiano Braga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christiano Braga +-/ + +module + +public import Mathlib.Tactic +public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic + +@[expose] public section + +/-! +# Diffie-Hellman protocol + +Suppose p is a large prime and that q is a large prime dividing p − 1 (think of p as being very +large random prime, say 2048 bits long, and think of q as being about 256 bits long). We will be +doing arithmetic mod p, that is, working in ℤₚ. Recall that ℤₚ* is the set of nonzero elements +of ℤₚ. An essential fact is that since q divides p − 1, ℤₚ* has an element g of order q. +This means that gᑫ = 1 and that all of the powers gᵃ, for a = 0, …, q − 1, are distinct. +Let G := {gᵃ : a = 0, …, q − 1}, so that G is a subset of ℤₚ* of cardinality q. It is not hard +to see that G is closed under multiplication and inversion; that is, for all u, v ∈ G, +we have u·v ∈ G and u⁻¹ ∈ G. Indeed, gᵃ · gᵇ = gᵃ⁺ᵇ = gᶜ with c := (a + b) mod q, and (gᵃ)⁻¹ = gᵈ +with d := (−a) mod q. In the language of algebra, G is called a subgroup of the group ℤₚ*. + +For every u ∈ G and integers a and b, it is easy to see that uᵃ = uᵇ if a ≡ b mod q. +Thus, the value of uᵃ depends only on the residue class of a modulo q. Therefore, +if α = [a]_q ∈ ℤ_q is the residue class of a modulo q, we can define uᵅ := uᵃ and this definition +is unambiguous. From here on we will frequently use elements of ℤ_q as exponents applied to +elements of G. + +So now we have everything we need to describe the Diffie-Hellman key exchange protocol. +We assume that the description of G, including g ∈ G and q, is a system parameter that is +generated once and for all at system setup time and shared by all parties involved. +The protocol runs as follows: + +1. Alice computes α ←ᴿ ℤ_q, u ← gᵅ, and sends u to Bob. +2. Bob computes β ←ᴿ ℤ_q, v ← gᵝ, and sends v to Alice. +3. Upon receiving v from Bob, Alice computes w ← vᵅ. +4. Upon receiving u from Alice, Bob computes w ← uᵝ. + +The secret shared by Alice and Bob is: + + w = vᵅ = gᵅᵝ = uᵝ + +Reference: + +* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*, One-time pad][BonehShoup], + Section 10.4. +-/ + +instance DiffieHellmanKE {G : Type u} [CommGroup G] (g : G) (q : ℕ) : + KeyExchangeProtocol (ZMod q) G G where + pub := fun α => g ^ α.val + sharedSecret := fun u α => u ^ α.val + agreement := by + intro α β + show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val + rw [← pow_mul, ← pow_mul, mul_comm] + +namespace Cslib.Systems.Distributed.Protocols.Cryptographic.DH + +variable {G : Type u} [CommGroup G] {q : ℕ} [Fact q.Prime] +variable (g : G) (hG : ∀ x : G, x ^ q = 1) +include hG + +/- +pow_mod_q — Exponents can be reduced mod q + x ^ (n % q) = x ^ n + +What it says: Exponentiating by n is the same as exponentiating by n mod q. + +Why it's true: By the division algorithm, n = q · (n / q) + (n mod q). So: + x^n = x^(q·(n/q) + n mod q) = x^(q·(n/q)) · x^(n mod q) + = (x^q)^(n/q) · x^(n mod q) = 1^(n/q) · x^(n mod q) = x^(n mod q) + +Why it matters: It lets you treat ℕ-valued exponents as living in ZMod q, +bridging Lean's natural number arithmetic with modular arithmetic. +-/ +omit [Fact q.Prime] in +private lemma pow_mod_q (x : G) (n : ℕ) : x ^ (n % q) = x ^ n := by + conv_rhs => rw [← Nat.div_add_mod n q] + rw [pow_add, pow_mul, hG x, one_pow, one_mul] + +/- +secret_eq — The shared secret (gᵝ)ᵅ equals g^(α·β) +Computing the shared secret from the other party's public value +is the same as exponentiating the generator by the product of both private keys. +This is the key algebraic fact underlying the protocol — it +shows the shared secret can be characterized as g^(α·β), independent of which +party computes it. +-/ +omit [Fact q.Prime] in +theorem secret_eq (α β : ZMod q) : + (g ^ β.val) ^ α.val = g ^ (α * β).val := by + rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q hG] + +end Cslib.Systems.Distributed.Protocols.Cryptographic.DH From ebbca7f502b2278f7208d0382d2e1542bbdf7555 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Wed, 22 Apr 2026 23:03:02 +0200 Subject: [PATCH 2/2] Address PR #473 review feedback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Rename Diffie-Hellman.lean → DiffieHellman.lean (valid module name). - Align namespaces under ...Cryptographic.KeyExchange; DH lives in ...KeyExchange.DH as a sibling sub-namespace. - Tighten the DiffieHellman class with [Fintype G], hq : Fintype.card G = q, and hg : orderOf g = q, so that g is a generator of a cyclic group of order q (previously under-constrained). - Remove dead Fact q.Prime hypothesis. - Rewrite module docstrings to match the actual generality of the code and add an explicit Scope note: correctness only, not DLP/CDH/DDH. - Upgrade pow_mod_q / secret_eq prose to /-- ... -/ doc-strings. - references.bib: switch BonehShoup entry to the online draft with URL. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Cryptographic/KeyExchange/Basic.lean | 32 +++--- .../KeyExchange/Diffie-Hellman.lean | 99 ------------------- .../KeyExchange/DiffieHellman.lean | 76 ++++++++++++++ references.bib | 11 +++ 4 files changed, 104 insertions(+), 114 deletions(-) delete mode 100644 Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean create mode 100644 Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean index aea7e8728..34f2696da 100644 --- a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean +++ b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean @@ -13,27 +13,27 @@ public import Mathlib.Tactic /-! # Key Exchange Protocol -A *key exchange protocol* allows two parties (Alice and Bob) to establish a shared secret -over an insecure channel. +An abstract typeclass capturing the structure of a two-party key-exchange protocol. A +protocol is given by three types — `PrivateKey`, `PublicValue`, `SharedSecret` — together +with: -The protocol proceeds as follows: +* `pub : PrivateKey → PublicValue`, the value a party publishes; +* `sharedSecret : PublicValue → PrivateKey → SharedSecret`, what each party computes from + the peer's public value and its own private key; +* `agreement`, the correctness law + `sharedSecret (pub β) α = sharedSecret (pub α) β` for all `α, β`. -1. Alice picks a private key α, computes her public value pub(α), and sends it to Bob. -2. Bob picks a private key β, computes his public value pub(β), and sends it to Alice. -3. Alice computes the shared secret as sharedSecret(pub(β), α). -4. Bob computes the shared secret as sharedSecret(pub(α), β). +Concrete protocols (e.g. Diffie-Hellman) arise by instantiating the three types and +supplying the three fields. This file captures only the correctness equation; security +assumptions belong to concrete instances. -The fundamental correctness property (*agreement*) states that both parties compute the same -shared secret: +## Reference - sharedSecret(pub(β), α) = sharedSecret(pub(α), β) - -Reference: - -* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*][BonehShoup], - Section 10.4. +* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.1 -/ +namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange + universe u v w class KeyExchangeProtocol @@ -46,3 +46,5 @@ class KeyExchangeProtocol /-- Agreement: both parties compute the same shared secret. -/ agreement : ∀ (α β : PrivateKey), sharedSecret (pub β) α = sharedSecret (pub α) β + +end Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean deleted file mode 100644 index 29d70c0c5..000000000 --- a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean +++ /dev/null @@ -1,99 +0,0 @@ -/- -Copyright (c) 2026 Christiano Braga. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christiano Braga --/ - -module - -public import Mathlib.Tactic -public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic - -@[expose] public section - -/-! -# Diffie-Hellman protocol - -Suppose p is a large prime and that q is a large prime dividing p − 1 (think of p as being very -large random prime, say 2048 bits long, and think of q as being about 256 bits long). We will be -doing arithmetic mod p, that is, working in ℤₚ. Recall that ℤₚ* is the set of nonzero elements -of ℤₚ. An essential fact is that since q divides p − 1, ℤₚ* has an element g of order q. -This means that gᑫ = 1 and that all of the powers gᵃ, for a = 0, …, q − 1, are distinct. -Let G := {gᵃ : a = 0, …, q − 1}, so that G is a subset of ℤₚ* of cardinality q. It is not hard -to see that G is closed under multiplication and inversion; that is, for all u, v ∈ G, -we have u·v ∈ G and u⁻¹ ∈ G. Indeed, gᵃ · gᵇ = gᵃ⁺ᵇ = gᶜ with c := (a + b) mod q, and (gᵃ)⁻¹ = gᵈ -with d := (−a) mod q. In the language of algebra, G is called a subgroup of the group ℤₚ*. - -For every u ∈ G and integers a and b, it is easy to see that uᵃ = uᵇ if a ≡ b mod q. -Thus, the value of uᵃ depends only on the residue class of a modulo q. Therefore, -if α = [a]_q ∈ ℤ_q is the residue class of a modulo q, we can define uᵅ := uᵃ and this definition -is unambiguous. From here on we will frequently use elements of ℤ_q as exponents applied to -elements of G. - -So now we have everything we need to describe the Diffie-Hellman key exchange protocol. -We assume that the description of G, including g ∈ G and q, is a system parameter that is -generated once and for all at system setup time and shared by all parties involved. -The protocol runs as follows: - -1. Alice computes α ←ᴿ ℤ_q, u ← gᵅ, and sends u to Bob. -2. Bob computes β ←ᴿ ℤ_q, v ← gᵝ, and sends v to Alice. -3. Upon receiving v from Bob, Alice computes w ← vᵅ. -4. Upon receiving u from Alice, Bob computes w ← uᵝ. - -The secret shared by Alice and Bob is: - - w = vᵅ = gᵅᵝ = uᵝ - -Reference: - -* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*, One-time pad][BonehShoup], - Section 10.4. --/ - -instance DiffieHellmanKE {G : Type u} [CommGroup G] (g : G) (q : ℕ) : - KeyExchangeProtocol (ZMod q) G G where - pub := fun α => g ^ α.val - sharedSecret := fun u α => u ^ α.val - agreement := by - intro α β - show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val - rw [← pow_mul, ← pow_mul, mul_comm] - -namespace Cslib.Systems.Distributed.Protocols.Cryptographic.DH - -variable {G : Type u} [CommGroup G] {q : ℕ} [Fact q.Prime] -variable (g : G) (hG : ∀ x : G, x ^ q = 1) -include hG - -/- -pow_mod_q — Exponents can be reduced mod q - x ^ (n % q) = x ^ n - -What it says: Exponentiating by n is the same as exponentiating by n mod q. - -Why it's true: By the division algorithm, n = q · (n / q) + (n mod q). So: - x^n = x^(q·(n/q) + n mod q) = x^(q·(n/q)) · x^(n mod q) - = (x^q)^(n/q) · x^(n mod q) = 1^(n/q) · x^(n mod q) = x^(n mod q) - -Why it matters: It lets you treat ℕ-valued exponents as living in ZMod q, -bridging Lean's natural number arithmetic with modular arithmetic. --/ -omit [Fact q.Prime] in -private lemma pow_mod_q (x : G) (n : ℕ) : x ^ (n % q) = x ^ n := by - conv_rhs => rw [← Nat.div_add_mod n q] - rw [pow_add, pow_mul, hG x, one_pow, one_mul] - -/- -secret_eq — The shared secret (gᵝ)ᵅ equals g^(α·β) -Computing the shared secret from the other party's public value -is the same as exponentiating the generator by the product of both private keys. -This is the key algebraic fact underlying the protocol — it -shows the shared secret can be characterized as g^(α·β), independent of which -party computes it. --/ -omit [Fact q.Prime] in -theorem secret_eq (α β : ZMod q) : - (g ^ β.val) ^ α.val = g ^ (α * β).val := by - rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q hG] - -end Cslib.Systems.Distributed.Protocols.Cryptographic.DH diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean new file mode 100644 index 000000000..22927a9bb --- /dev/null +++ b/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Christiano Braga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christiano Braga +-/ + +module + +public import Mathlib.Tactic +public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic + +@[expose] public section + +/-! +# Diffie-Hellman protocol + +Diffie-Hellman key exchange as an instance of `KeyExchangeProtocol` in a finite cyclic +group `G` of cardinality `q` with a generator `g`. Two parties sample private keys +`α, β : ZMod q`, publish `g ^ α.val` and `g ^ β.val`, and each raises the peer's public +value to its own private key. Correctness: both arrive at `g ^ (α · β).val`. + +## Scope + +This file formalizes only the *correctness* (agreement) of the exchange. + +## Main declarations + +* `DiffieHellman g q hq hg` — the protocol, extending `KeyExchangeProtocol (ZMod q) G G`. + Two setup invariants are carried as fields: + - `hq : Fintype.card G = q` pins down `q` as the cardinality of `G`. This is what lets + private keys live in `ZMod q` faithfully: by Lagrange `x ^ Fintype.card G = 1` for every + `x : G`, hence `hq` gives `x ^ q = 1`, so exponents depend only on their residue + modulo `q`. + - `hg : orderOf g = q` says `g` has order `q`. Combined with `hq`, it means + `orderOf g = Fintype.card G`, which in a cyclic group is exactly the statement that `g` + is a generator. +* `secret_eq` — `(g ^ β.val) ^ α.val = g ^ (α * β).val`: the algebraic core of agreement. + +## Reference + +* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.2 +-/ + +namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.DH + +open KeyExchange + +class DiffieHellman {G : Type u} [Group G] [Fintype G] [IsCyclic G] + (g : G) (q : ℕ) (hq : Fintype.card G = q) (hg : orderOf g = q) + extends KeyExchangeProtocol (ZMod q) G G where + pub α := g ^ α.val + sharedSecret u α := u ^ α.val + agreement := by + intro α β + show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val + rw [← pow_mul, ← pow_mul, mul_comm] + +variable {G : Type u} [Group G] [Fintype G] +variable (g : G) (q : ℕ) (hq : Fintype.card G = q) +include hq + +/-- In a finite group of cardinality `q`, exponents may be reduced modulo `q`. Together with +`ZMod.val_mul` this lets `ℕ`-valued exponents be treated as living in `ZMod q`. -/ +private lemma pow_mod_q (x : G) (n : ℕ) : + x ^ (n % q) = x ^ n := by + conv_rhs => rw [← Nat.div_add_mod n q] + have hxq : x ^ q = 1 := hq ▸ pow_card_eq_one + rw [pow_add, pow_mul, hxq, one_pow, one_mul] + +/-- The Diffie-Hellman shared secret `(g ^ β.val) ^ α.val` equals `g ^ (α * β).val`, +independently of which party computes it. This is the algebraic core of `agreement`. -/ +theorem secret_eq (α β : ZMod q) : + (g ^ β.val) ^ α.val = g ^ (α * β).val := by + rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q q hq] + +end Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.DH diff --git a/references.bib b/references.bib index 1f8c0dc51..03521ebc8 100644 --- a/references.bib +++ b/references.bib @@ -287,3 +287,14 @@ @incollection{WinskelNielsen1995 url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, } + +@online{ BonehShoup, + author = {Boneh, Dan and Shoup, Victor}, + title = {A Graduate Course in Applied Cryptography}, + month = {Jan.}, + year = {2023}, + edition = {Version 0.6}, + note = {Free online}, + url = {https://toc.cryptobook.us/}, + urldate = {2026-04-22} +}