From 39b20803d4c09a9ef8eab9b0027be425510f4f49 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Mon, 6 Apr 2026 17:55:33 -0300 Subject: [PATCH 01/11] 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 02/11] 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} +} From 6eab62eb66522b2ee79eb80dd2b850f34300d7e9 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 14:27:44 -0300 Subject: [PATCH 03/11] refactor(KeyExchange): relocate to Crypto/Protocols and trim imports Move KeyExchange/{Basic,DiffieHellman}.lean from Systems/Distributed/Protocols/Cryptographic/ to Crypto/Protocols/, mirroring the SecretSharing layout. Drop the umbrella `Mathlib.Tactic` import: Basic.lean needs no Mathlib imports, and DiffieHellman.lean reduces to a single `Mathlib.Data.ZMod.Basic` import. Update the Cslib.lean aggregator accordingly. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cslib.lean | 4 ++-- .../Protocols}/KeyExchange/Basic.lean | 10 ++++------ .../Protocols}/KeyExchange/DiffieHellman.lean | 14 +++++++------- 3 files changed, 13 insertions(+), 15 deletions(-) rename Cslib/{Systems/Distributed/Protocols/Cryptographic => Crypto/Protocols}/KeyExchange/Basic.lean (90%) rename Cslib/{Systems/Distributed/Protocols/Cryptographic => Crypto/Protocols}/KeyExchange/DiffieHellman.lean (89%) diff --git a/Cslib.lean b/Cslib.lean index 5bb796841..724315199 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,6 +46,8 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs public import Cslib.Crypto.Protocols.SecretSharing.Scheme public import Cslib.Crypto.Protocols.SecretSharing.Shamir public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial +public import Cslib.Crypto.Protocols.KeyExchange.Basic +public import Cslib.Crypto.Protocols.KeyExchange.DiffieHellman public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects @@ -126,8 +128,6 @@ 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/Crypto/Protocols/KeyExchange/Basic.lean similarity index 90% rename from Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean rename to Cslib/Crypto/Protocols/KeyExchange/Basic.lean index 34f2696da..9e43231b1 100644 --- a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean +++ b/Cslib/Crypto/Protocols/KeyExchange/Basic.lean @@ -6,10 +6,6 @@ Authors: Christiano Braga module -public import Mathlib.Tactic - -@[expose] public section - /-! # Key Exchange Protocol @@ -32,7 +28,9 @@ assumptions belong to concrete instances. * [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.1 -/ -namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange +@[expose] public section + +namespace Cslib.Crypto.Protocols.KeyExchange universe u v w @@ -47,4 +45,4 @@ class KeyExchangeProtocol agreement : ∀ (α β : PrivateKey), sharedSecret (pub β) α = sharedSecret (pub α) β -end Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange +end Cslib.Crypto.Protocols.KeyExchange diff --git a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean b/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean similarity index 89% rename from Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean rename to Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean index 22927a9bb..2ecddd27f 100644 --- a/Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean +++ b/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean @@ -6,10 +6,8 @@ Authors: Christiano Braga module -public import Mathlib.Tactic -public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic - -@[expose] public section +public import Mathlib.Data.ZMod.Basic +public import Cslib.Crypto.Protocols.KeyExchange.Basic /-! # Diffie-Hellman protocol @@ -41,11 +39,13 @@ This file formalizes only the *correctness* (agreement) of the exchange. * [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.2 -/ -namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.DH +@[expose] public section + +namespace Cslib.Crypto.Protocols.KeyExchange.DH open KeyExchange -class DiffieHellman {G : Type u} [Group G] [Fintype G] [IsCyclic G] +structure 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 @@ -73,4 +73,4 @@ 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 +end Cslib.Crypto.Protocols.KeyExchange.DH From cbae4f839367983efc354770e03fff9e3c10857f Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 15:30:57 -0300 Subject: [PATCH 04/11] refactor(DiffieHellman): drop KEP, rebase DH on `Module F G` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the `KeyExchangeProtocol` abstraction (Basic.lean) and its aggregator entry. KEP carried no inheritable theory at its level — agreement was its only law and no generic theorems applied above it. None of the protocols this library targets (X3DH, PQXDH, Signal double-ratchet, MLS, KVAC) fit the symmetric one-shot KEP shape, so KEP was paying ergonomic cost for no abstraction benefit. Rewrite Diffie–Hellman on `Module F G`, matching the BAIF PQXDH-model and VCV-io's hardness-assumptions file. The textbook multiplicative view `gᵃ` becomes the additive scalar action `a • g`, and Mathlib's `Module` lemmas (`mul_smul`, `add_smul`, `smul_add`) cover the algebraic core for free. This eliminates the multiplicative-`Group G` + `Fintype` + `IsCyclic` + `orderOf g = q` machinery the old file needed; the order/cardinality/generator conditions move to the instantiation layer (X25519, X448) as a `Function.Bijective (· • g)` condition on the action when needed. State `agreement`, `dh_add_left`, `dh_add_right` as named theorems for downstream citation by X3DH/PQXDH transcript-composition proofs. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cslib.lean | 1 - Cslib/Crypto/Protocols/KeyExchange/Basic.lean | 48 -------- .../Protocols/KeyExchange/DiffieHellman.lean | 106 +++++++++--------- 3 files changed, 56 insertions(+), 99 deletions(-) delete mode 100644 Cslib/Crypto/Protocols/KeyExchange/Basic.lean diff --git a/Cslib.lean b/Cslib.lean index 724315199..fba74ce95 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,7 +46,6 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs public import Cslib.Crypto.Protocols.SecretSharing.Scheme public import Cslib.Crypto.Protocols.SecretSharing.Shamir public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial -public import Cslib.Crypto.Protocols.KeyExchange.Basic public import Cslib.Crypto.Protocols.KeyExchange.DiffieHellman public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free diff --git a/Cslib/Crypto/Protocols/KeyExchange/Basic.lean b/Cslib/Crypto/Protocols/KeyExchange/Basic.lean deleted file mode 100644 index 9e43231b1..000000000 --- a/Cslib/Crypto/Protocols/KeyExchange/Basic.lean +++ /dev/null @@ -1,48 +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 - -/-! -# Key Exchange Protocol - -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: - -* `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 `α, β`. - -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. - -## Reference - -* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.1 --/ - -@[expose] public section - -namespace Cslib.Crypto.Protocols.KeyExchange - -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 α) β - -end Cslib.Crypto.Protocols.KeyExchange diff --git a/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean b/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean index 2ecddd27f..4c1070b17 100644 --- a/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean +++ b/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean @@ -6,71 +6,77 @@ Authors: Christiano Braga module -public import Mathlib.Data.ZMod.Basic -public import Cslib.Crypto.Protocols.KeyExchange.Basic +public import Mathlib.Algebra.Module.Basic /-! -# Diffie-Hellman protocol +# Diffie–Hellman primitive, founded on `Module F G` -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`. +The Diffie–Hellman primitive is the scalar action of a commutative ring `F` on +an additive abelian group `G`. Writing exponents additively, as Mathlib does +for elliptic-curve groups, the textbook `gᵃ` becomes `a • g`, and the textbook +exponent-product `(gᵃ)ᵇ = gᵃᵇ` becomes `b • (a • g) = (b * a) • g`. Every +Mathlib `Module` lemma applies directly to `dh`. -## Scope +This file states only the primitive and the laws downstream protocols (X3DH, +PQXDH, Signal double-ratchet, MLS) cite. Hardness assumptions (DLog, CDH, +DDH) and concrete instantiations (X25519, X448) live in separate files. -This file formalizes only the *correctness* (agreement) of the exchange. +## Notation correspondence + +| Multiplicative textbook | Additive (`Module F G`) | +|----------------------------|--------------------------------| +| `gᵃ` | `a • g` | +| `(gᵃ)ᵇ = gᵃᵇ` | `b • (a • g) = (b * a) • g` | +| `gᵃ · gᵇ = gᵃ⁺ᵇ` | `a • g + b • g = (a + b) • g` | +| `(g · h)ᵃ = gᵃ · hᵃ` | `a • (g + h) = a • g + a • h` | ## 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. +* `dh a B` — the primitive `a • B`. +* `agreement` — `b • (a • B) = a • (b • B)`: the two parties agree on the + shared point regardless of which side performs the final scalar action. +* `dh_add_left`, `dh_add_right` — scalar- and base-additivity of `dh`, + cited by protocols that combine secrets or transcripts additively + (X3DH/PQXDH). -## Reference +## References -* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.2 +* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], + Section 10.4. +* BAIF, *PostQuantumeXtendedDiffieHellman-model* (PQXDHLean/X3DH/DH.lean). +* Verified-zkEVM, *VCV-io* + (VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean). -/ @[expose] public section namespace Cslib.Crypto.Protocols.KeyExchange.DH -open KeyExchange - -structure 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] +variable {F : Type*} [CommRing F] +variable {G : Type*} [AddCommGroup G] [Module F G] + +/-- Diffie–Hellman primitive: the scalar action `a • B`. Declared as `abbrev` +so that every Mathlib `Module` lemma applies definitionally. -/ +abbrev dh (a : F) (B : G) : G := a • B + +/-- **Agreement.** Two parties starting from a common base point `B`, with +private scalars `a` and `b`, compute the same shared point regardless of +which side performs the final scalar action. Both sides equal `(a * b) • B`. -/ +theorem agreement (a b : F) (B : G) : + dh b (dh a B) = dh a (dh b B) := by + change b • (a • B) = a • (b • B) + rw [← mul_smul, ← mul_smul, mul_comm] + +/-- Scalar-additivity. Cited by protocols that combine secrets additively, +e.g. a long-term scalar added to an ephemeral one. -/ +theorem dh_add_left (a b : F) (B : G) : + dh (a + b) B = dh a B + dh b B := + add_smul a b B + +/-- Base-additivity. Cited by protocols whose peer public values decompose +as sums of component public values, as in X3DH/PQXDH transcripts. -/ +theorem dh_add_right (a : F) (B C : G) : + dh a (B + C) = dh a B + dh a C := + smul_add a B C end Cslib.Crypto.Protocols.KeyExchange.DH From 90fca19e5ca295e04299f95a6500ad7863398276 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 15:35:17 -0300 Subject: [PATCH 05/11] refactor(DiffieHellman): move to its own directory, rename file to Basic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Relocate the Diffie–Hellman module from `KeyExchange/DiffieHellman.lean` to `DiffieHellman/Basic.lean`, mirroring the `SecretSharing/` layout (each protocol gets its own directory, with `Basic` as the entry point). Drop the now-empty `KeyExchange/` directory. Rename the in-file namespace `Cslib.Crypto.Protocols.KeyExchange.DH` to `Cslib.Crypto.Protocols.DiffieHellman`, eliminating the now-redundant `.DH` suffix. This prepares the directory for future siblings (`Hardness.lean`, `Instances/X25519.lean`, etc.) without the misleading `KeyExchange` umbrella, which is no longer carrying an abstraction. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cslib.lean | 2 +- .../DiffieHellman.lean => DiffieHellman/Basic.lean} | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) rename Cslib/Crypto/Protocols/{KeyExchange/DiffieHellman.lean => DiffieHellman/Basic.lean} (97%) diff --git a/Cslib.lean b/Cslib.lean index fba74ce95..41e23fe04 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,7 +46,7 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs public import Cslib.Crypto.Protocols.SecretSharing.Scheme public import Cslib.Crypto.Protocols.SecretSharing.Shamir public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial -public import Cslib.Crypto.Protocols.KeyExchange.DiffieHellman +public import Cslib.Crypto.Protocols.DiffieHellman.Basic public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects diff --git a/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean similarity index 97% rename from Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean rename to Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index 4c1070b17..a7909c697 100644 --- a/Cslib/Crypto/Protocols/KeyExchange/DiffieHellman.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -50,7 +50,7 @@ DDH) and concrete instantiations (X25519, X448) live in separate files. @[expose] public section -namespace Cslib.Crypto.Protocols.KeyExchange.DH +namespace Cslib.Crypto.Protocols.DiffieHellman variable {F : Type*} [CommRing F] variable {G : Type*} [AddCommGroup G] [Module F G] @@ -79,4 +79,4 @@ theorem dh_add_right (a : F) (B C : G) : dh a (B + C) = dh a B + dh a C := smul_add a B C -end Cslib.Crypto.Protocols.KeyExchange.DH +end Cslib.Crypto.Protocols.DiffieHellman From 0cda394dd2c7fbe49f9ecde14bb3de1f4b98df4a Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 16:05:22 -0300 Subject: [PATCH 06/11] feat(DiffieHellman): add `shared_eq_mul` canonical form, drop redundant linearity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace `dh_add_left` and `dh_add_right` with `shared_eq_mul`, the canonical-form statement of DH correctness: `dh b (dh a B) = (a * b) • B`. Either party's computation lands on a single closed expression independent of computation order. `agreement` now follows as a corollary of `shared_eq_mul` by `mul_comm` in the scalar ring, making the structural dependency between the two statements explicit. The removed `dh_add_left`/`dh_add_right` were one-to-one aliases for `add_smul`/`smul_add` with no DH-specific content. None of the named target protocols (X3DH, PQXDH) combine DH outputs by addition in `G` — they concatenate-and-KDF — so the lemmas were YAGNI noise. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Crypto/Protocols/DiffieHellman/Basic.lean | 36 ++++++++----------- 1 file changed, 15 insertions(+), 21 deletions(-) diff --git a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index a7909c697..af477242e 100644 --- a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -33,11 +33,10 @@ DDH) and concrete instantiations (X25519, X448) live in separate files. ## Main declarations * `dh a B` — the primitive `a • B`. -* `agreement` — `b • (a • B) = a • (b • B)`: the two parties agree on the - shared point regardless of which side performs the final scalar action. -* `dh_add_left`, `dh_add_right` — scalar- and base-additivity of `dh`, - cited by protocols that combine secrets or transcripts additively - (X3DH/PQXDH). +* `shared_eq_mul` — the shared point in canonical form: + `b • (a • B) = (a * b) • B`. +* `agreement` — the two parties compute the same shared point; corollary + of `shared_eq_mul`. ## References @@ -59,24 +58,19 @@ variable {G : Type*} [AddCommGroup G] [Module F G] so that every Mathlib `Module` lemma applies definitionally. -/ abbrev dh (a : F) (B : G) : G := a • B +/-- **Shared secret in canonical form.** Either party's computation lands +on `(a * b) • B` — a single closed expression independent of which side +performs the final scalar action. -/ +theorem shared_eq_mul (a b : F) (B : G) : + dh b (dh a B) = (a * b) • B := by + change b • (a • B) = (a * b) • B + rw [← mul_smul, mul_comm b a] + /-- **Agreement.** Two parties starting from a common base point `B`, with -private scalars `a` and `b`, compute the same shared point regardless of -which side performs the final scalar action. Both sides equal `(a * b) • B`. -/ +private scalars `a` and `b`, compute the same shared point. Corollary of +`shared_eq_mul` by commutativity of multiplication in `F`. -/ theorem agreement (a b : F) (B : G) : dh b (dh a B) = dh a (dh b B) := by - change b • (a • B) = a • (b • B) - rw [← mul_smul, ← mul_smul, mul_comm] - -/-- Scalar-additivity. Cited by protocols that combine secrets additively, -e.g. a long-term scalar added to an ephemeral one. -/ -theorem dh_add_left (a b : F) (B : G) : - dh (a + b) B = dh a B + dh b B := - add_smul a b B - -/-- Base-additivity. Cited by protocols whose peer public values decompose -as sums of component public values, as in X3DH/PQXDH transcripts. -/ -theorem dh_add_right (a : F) (B C : G) : - dh a (B + C) = dh a B + dh a C := - smul_add a B C + rw [shared_eq_mul, mul_comm a b, ← shared_eq_mul] end Cslib.Crypto.Protocols.DiffieHellman From 5746dcebf5c466f871498b6e9d021fec624d8edf Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 16:09:08 -0300 Subject: [PATCH 07/11] =?UTF-8?q?docs(DiffieHellman):=20drop=20Boneh?= =?UTF-8?q?=E2=80=93Shoup,=20link=20the=20two=20formulation=20references?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Boneh–Shoup §10.4 presents DH in the textbook multiplicative-group style — it isn't a reference for the `Module F G` formulation this file actually uses. The notation table in the docstring already bridges multiplicative-textbook to additive algebraic readings, so the citation was misdirecting more than helping. Replace it by linking the two remaining references (BAIF and VCV-io) directly to their GitHub source files — both of which do use the `Module F G` formulation, and are what this file is genuinely built on. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cslib/Crypto/Protocols/DiffieHellman/Basic.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index af477242e..82d89d65e 100644 --- a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -40,11 +40,8 @@ DDH) and concrete instantiations (X25519, X448) live in separate files. ## References -* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], - Section 10.4. -* BAIF, *PostQuantumeXtendedDiffieHellman-model* (PQXDHLean/X3DH/DH.lean). -* Verified-zkEVM, *VCV-io* - (VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean). +* BAIF, [PostQuantumeXtendedDiffieHellman-model / PQXDHLean/X3DH/DH.lean](https://github.com/Beneficial-AI-Foundation/PostQuantumeXtendedDiffieHellman-model/blob/main/PQXDHLean/X3DH/DH.lean). +* Verified-zkEVM, [VCV-io / VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean](https://github.com/Verified-zkEVM/VCV-io/blob/main/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean). -/ @[expose] public section From 4e65fa3959fa5bf765af3def009f0d901887bd6f Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 16:11:15 -0300 Subject: [PATCH 08/11] docs(DiffieHellman): drop References section Co-Authored-By: Claude Opus 4.7 (1M context) --- Cslib/Crypto/Protocols/DiffieHellman/Basic.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index 82d89d65e..4b91214d1 100644 --- a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -37,11 +37,6 @@ DDH) and concrete instantiations (X25519, X448) live in separate files. `b • (a • B) = (a * b) • B`. * `agreement` — the two parties compute the same shared point; corollary of `shared_eq_mul`. - -## References - -* BAIF, [PostQuantumeXtendedDiffieHellman-model / PQXDHLean/X3DH/DH.lean](https://github.com/Beneficial-AI-Foundation/PostQuantumeXtendedDiffieHellman-model/blob/main/PQXDHLean/X3DH/DH.lean). -* Verified-zkEVM, [VCV-io / VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean](https://github.com/Verified-zkEVM/VCV-io/blob/main/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean). -/ @[expose] public section From fb3c6eddba84adeb1c672fc3128cdfcc0defca11 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 16:12:06 -0300 Subject: [PATCH 09/11] docs(references): drop orphan BonehShoup entry MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Boneh–Shoup citation was removed from DiffieHellman/Basic.lean in 5746dce; no other .lean file cites it. Removing the orphan BibTeX entry from references.bib. Co-Authored-By: Claude Opus 4.7 (1M context) --- references.bib | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/references.bib b/references.bib index 5c84e3133..e6645c5f0 100644 --- a/references.bib +++ b/references.bib @@ -371,13 +371,3 @@ @incollection{WinskelNielsen1995 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} -} From 17b2a56f99782eb37c468c6b63463ba433e254ff Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 17:40:20 -0300 Subject: [PATCH 10/11] feat(DiffieHellman): add `IsHonestGenerator` typeclass; gate `dh` on it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce `IsHonestGenerator F G`, a typeclass capturing the non-degeneracy condition for the scalar action of `F` on `G`: there is a fixed `generator : G` for which `(· • generator) : F → G` is a bijection. This is the minimal cryptographic-meaningfulness predicate on the module — degenerate modules (trivial; rank > 1; torsion-bearing) satisfy `Module F G` algebraically but admit no honest generator, and DH's security collapses on them. Structure: * `IsHonestGenerator F G` (class) — declared first; carries the chosen generator and the bijectivity proof. * `dh` is gated unconditionally: declared inside a sub-section that `include hg`s the typeclass instance. Callers must supply `[IsHonestGenerator F G]` to invoke `dh`. * `shared_eq_mul` and `agreement` pick up `[IsHonestGenerator F G]` automatically — Lean introduces it on demand because their statements call `dh`. No `include`, no linter suppression, no manual repetition. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Crypto/Protocols/DiffieHellman/Basic.lean | 63 ++++++++++++++++--- 1 file changed, 55 insertions(+), 8 deletions(-) diff --git a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index 4b91214d1..7ddf4157a 100644 --- a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -17,9 +17,19 @@ for elliptic-curve groups, the textbook `gᵃ` becomes `a • g`, and the textbo exponent-product `(gᵃ)ᵇ = gᵃᵇ` becomes `b • (a • g) = (b * a) • g`. Every Mathlib `Module` lemma applies directly to `dh`. -This file states only the primitive and the laws downstream protocols (X3DH, -PQXDH, Signal double-ratchet, MLS) cite. Hardness assumptions (DLog, CDH, -DDH) and concrete instantiations (X25519, X448) live in separate files. +DH is restricted here to **non-degenerate** modules. The class +`IsHonestGenerator F G` (declared below) asserts that some element of `G` +makes the scalar-to-point map a bijection, and every other declaration in +this file is gated on it via `include hg`. Degenerate modules (trivial, +rank > 1, torsion-bearing) satisfy `Module F G` but admit no honest +generator; DH's algebraic equations still hold on them, but its security +claims collapse, so they are excluded at the type level. + +Downstream protocols (X3DH, PQXDH, Signal double-ratchet, MLS) consume +the primitive and its correctness laws. Hardness assumptions (DLog, CDH, +DDH) and concrete instantiations (X25519, X448) live in separate files; +the latter install `IsHonestGenerator F G` instances by exhibiting their +standard base point as `generator`. ## Notation correspondence @@ -32,24 +42,60 @@ DDH) and concrete instantiations (X25519, X448) live in separate files. ## Main declarations +* `IsHonestGenerator F G` — typeclass: `G` has a fixed honest generator — + an element `generator : G` for which `(· • generator) : F → G` is a + bijection. The minimal non-degeneracy condition; every other declaration + in this file is gated on it. * `dh a B` — the primitive `a • B`. * `shared_eq_mul` — the shared point in canonical form: `b • (a • B) = (a * b) • B`. * `agreement` — the two parties compute the same shared point; corollary of `shared_eq_mul`. + +## References + +* Verified-zkEVM, [VCV-io / VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean](https://github.com/Verified-zkEVM/VCV-io/blob/main/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean) — + VCV-io uses the same `Module F G` foundation as this file. -/ @[expose] public section namespace Cslib.Crypto.Protocols.DiffieHellman -variable {F : Type*} [CommRing F] -variable {G : Type*} [AddCommGroup G] [Module F G] - -/-- Diffie–Hellman primitive: the scalar action `a • B`. Declared as `abbrev` -so that every Mathlib `Module` lemma applies definitionally. -/ +/-- `G`, viewed as an `F`-module, has a fixed **honest generator** — an +element `generator : G` for which the scalar-to-point map +`(fun a : F => a • generator)`, *"given a scalar `a`, return the point +`a • generator`"*, is a bijection. + +The bijection packs two conditions: + +* **surjective** — every point in `G` is reachable as `a • generator` for some + scalar `a`; no spot is hidden from scalar sampling. +* **injective** — distinct scalars produce distinct points; equivalently, the + generator has no torsion collisions that would collapse exponent counts. + +This is the minimal non-degeneracy condition under which DH is +cryptographically meaningful. Degenerate modules (trivial; rank > 1; +torsion-bearing) satisfy `Module F G` but fail to admit any honest +generator, and DH's security claims collapse on them. Concrete +instantiations (X25519, X448) install an instance by exhibiting their +standard base point as `generator`. -/ +class IsHonestGenerator (F G : Type*) [CommRing F] [AddCommGroup G] [Module F G] where + /-- The chosen honest generator. -/ + generator : G + /-- The scalar-to-point map at `generator` is a bijection. -/ + bijective : Function.Bijective (fun a : F => a • generator) + +variable {F G : Type*} [CommRing F] [AddCommGroup G] [Module F G] [hg : IsHonestGenerator F G] + +include hg in -- Necessary because a • B does not need hg, so the elaborator does not bind it. + -- A degenerate module is cryptographically insecure. +/-- Diffie–Hellman primitive: the scalar action `a • B`. Gated unconditionally +on `[IsHonestGenerator F G]` (via `include hg` in this section) — this file +does not formalize DH on degenerate modules. -/ abbrev dh (a : F) (B : G) : G := a • B +omit hg in -- Because dh already carries hg. /-- **Shared secret in canonical form.** Either party's computation lands on `(a * b) • B` — a single closed expression independent of which side performs the final scalar action. -/ @@ -58,6 +104,7 @@ theorem shared_eq_mul (a b : F) (B : G) : change b • (a • B) = (a * b) • B rw [← mul_smul, mul_comm b a] +omit hg in -- Because dh already carries hg. /-- **Agreement.** Two parties starting from a common base point `B`, with private scalars `a` and `b`, compute the same shared point. Corollary of `shared_eq_mul` by commutativity of multiplication in `F`. -/ From 6889c732eb0064fe84fbcd52ee513e77292eaae1 Mon Sep 17 00:00:00 2001 From: Christiano Braga Date: Fri, 22 May 2026 18:52:32 -0300 Subject: [PATCH 11/11] feat(DiffieHellman): enforce primality gate; cite VCVio26 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `dh` is now gated on two orthogonal cryptographic prerequisites: * `[IsHonestGenerator F G]` — the scalar-to-point map is a bijection (non-degeneracy of the chosen generator). * `[Fact (Nat.Prime (Fintype.card F))]` — `F` is finite with prime cardinality, so (via the bijection) `G` is a prime-order cyclic group. Without prime order, Pohlig–Hellman reduces DLog to small prime-power subgroups; the gate excludes that case at the type level. Previously `IsHonestGenerator` bundled both conditions; this commit separates them, because primality is a property of `|G|` and is orthogonal to whether the chosen generator is honest. They are declared as independent typeclass hypotheses and both are forced into `dh`'s signature via `include hg hp`. Add a `VCVio26` BibTeX entry (Tuma, Dao, Waters, Hicks, Hopper, *VCVio: Verified Cryptography in Lean via Oracle Effects and Handlers*, Cryptology ePrint 2026/899) and cite it from the module docstring as the layer-2 reference using the same `Module F G` foundation. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Crypto/Protocols/DiffieHellman/Basic.lean | 107 +++++++++++------- references.bib | 7 ++ 2 files changed, 71 insertions(+), 43 deletions(-) diff --git a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean index 7ddf4157a..0f67d9f43 100644 --- a/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean +++ b/Cslib/Crypto/Protocols/DiffieHellman/Basic.lean @@ -7,6 +7,8 @@ Authors: Christiano Braga module public import Mathlib.Algebra.Module.Basic +public import Mathlib.Data.Fintype.Card +public import Mathlib.Data.Nat.Prime.Basic /-! # Diffie–Hellman primitive, founded on `Module F G` @@ -17,19 +19,31 @@ for elliptic-curve groups, the textbook `gᵃ` becomes `a • g`, and the textbo exponent-product `(gᵃ)ᵇ = gᵃᵇ` becomes `b • (a • g) = (b * a) • g`. Every Mathlib `Module` lemma applies directly to `dh`. -DH is restricted here to **non-degenerate** modules. The class -`IsHonestGenerator F G` (declared below) asserts that some element of `G` -makes the scalar-to-point map a bijection, and every other declaration in -this file is gated on it via `include hg`. Degenerate modules (trivial, -rank > 1, torsion-bearing) satisfy `Module F G` but admit no honest -generator; DH's algebraic equations still hold on them, but its security -claims collapse, so they are excluded at the type level. +`dh` is gated on two **orthogonal** cryptographic prerequisites: -Downstream protocols (X3DH, PQXDH, Signal double-ratchet, MLS) consume -the primitive and its correctness laws. Hardness assumptions (DLog, CDH, -DDH) and concrete instantiations (X25519, X448) live in separate files; -the latter install `IsHonestGenerator F G` instances by exhibiting their -standard base point as `generator`. +1. `IsHonestGenerator F G` — there is a fixed `generator : G` for which the + scalar-to-point map is a bijection. Rules out *degenerate* modules + (trivial, rank > 1, torsion-bearing), on which DLog is ill-defined. +2. `Fact (Nat.Prime (Fintype.card F))` — the scalar ring's cardinality is + prime, so (via the bijection) `G` is a prime-order cyclic group. Rules + out *composite-order* modules, on which Pohlig–Hellman reduces DLog in + `G` to DLog in its prime-power subgroups — catastrophic for security. + +The two conditions are independent: a bijection can hold on a +composite-order group (`ZMod 6 → ZMod 6` via the identity), and a +prime-order group can fail bijection (a degenerate non-faithful action). +Both gates are needed; both are forced onto `dh` via `include hg hp`. + +On any module that fails either gate, DH's algebraic equations still hold, +but its cryptographic claims collapse, so they are excluded at the type +level. + +Downstream protocols (X3DH, PQXDH, Signal double-ratchet, MLS) consume the +primitive and its correctness laws. Hardness assumptions (DLog, CDH, DDH) +and concrete instantiations (X25519, X448) live in separate files; the +latter install `IsHonestGenerator F G` and `Fact (Nat.Prime …)` instances +by exhibiting their standard base point and citing the established +primality of their subgroup order. ## Notation correspondence @@ -42,11 +56,12 @@ standard base point as `generator`. ## Main declarations -* `IsHonestGenerator F G` — typeclass: `G` has a fixed honest generator — - an element `generator : G` for which `(· • generator) : F → G` is a - bijection. The minimal non-degeneracy condition; every other declaration - in this file is gated on it. -* `dh a B` — the primitive `a • B`. +* `IsHonestGenerator F G` — typeclass: a fixed element `generator : G` for + which `(· • generator) : F → G` is a bijection (non-degeneracy of the + action). +* `dh a B` — the primitive `a • B`. Gated on + `[IsHonestGenerator F G]` *and* `[Fact (Nat.Prime (Fintype.card F))]` + (the latter is the prime-order condition, supplied independently). * `shared_eq_mul` — the shared point in canonical form: `b • (a • B) = (a * b) • B`. * `agreement` — the two parties compute the same shared point; corollary @@ -54,48 +69,55 @@ standard base point as `generator`. ## References -* Verified-zkEVM, [VCV-io / VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean](https://github.com/Verified-zkEVM/VCV-io/blob/main/VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean) — - VCV-io uses the same `Module F G` foundation as this file. +* [VCVio26] Tuma, Dao, Waters, Hicks, Hopper, *VCVio: Verified Cryptography in + Lean via Oracle Effects and Handlers*, Cryptology ePrint 2026/899 + ([eprint.iacr.org/2026/899](https://eprint.iacr.org/2026/899)) — companion + paper to the [VCV-io library](https://github.com/Verified-zkEVM/VCV-io), + whose [DiffieHellman.lean] + (https://github.com/Verified-zkEVM/VCV-io/blob/main/ + VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean) + uses the same `Module F G` foundation as this file and lifts it to the + hardness layer (DLog/CDH/DDH experiments and reductions). -/ @[expose] public section namespace Cslib.Crypto.Protocols.DiffieHellman -/-- `G`, viewed as an `F`-module, has a fixed **honest generator** — an -element `generator : G` for which the scalar-to-point map -`(fun a : F => a • generator)`, *"given a scalar `a`, return the point -`a • generator`"*, is a bijection. +/-- `g` is an **honest generator** for the scalar action of `F` on `G` when +the map `(fun a : F => a • g) : F → G` is a bijection: surjective (every +point of `G` is reachable as `a • g`) and injective (distinct scalars +produce distinct points; no torsion collisions). This is the +*non-degeneracy* condition on the chosen generator, and is orthogonal to +any condition on the order of `G`. -The bijection packs two conditions: - -* **surjective** — every point in `G` is reachable as `a • generator` for some - scalar `a`; no spot is hidden from scalar sampling. -* **injective** — distinct scalars produce distinct points; equivalently, the - generator has no torsion collisions that would collapse exponent counts. - -This is the minimal non-degeneracy condition under which DH is -cryptographically meaningful. Degenerate modules (trivial; rank > 1; -torsion-bearing) satisfy `Module F G` but fail to admit any honest -generator, and DH's security claims collapse on them. Concrete -instantiations (X25519, X448) install an instance by exhibiting their -standard base point as `generator`. -/ +Without the bijection, DLog is ill-defined or multi-valued, and the +discrete-log game is meaningless even before we consider hardness. -/ class IsHonestGenerator (F G : Type*) [CommRing F] [AddCommGroup G] [Module F G] where /-- The chosen honest generator. -/ generator : G /-- The scalar-to-point map at `generator` is a bijection. -/ bijective : Function.Bijective (fun a : F => a • generator) -variable {F G : Type*} [CommRing F] [AddCommGroup G] [Module F G] [hg : IsHonestGenerator F G] +variable {F G : Type*} [CommRing F] [AddCommGroup G] [Module F G] + +section +variable [Fintype F] [hg : IsHonestGenerator F G] [hp : Fact (Nat.Prime (Fintype.card F))] +include hg hp +-- `dh` is gated on **two orthogonal cryptographic prerequisites**: +-- 1. `IsHonestGenerator F G` — the action is faithful (bijection). +-- 2. `Fact (Nat.Prime (Fintype.card F))` — the scalar ring's cardinality +-- is prime, so (under the bijection) `G` is a prime-order cyclic +-- group, avoiding Pohlig–Hellman. +-- `dh`'s body doesn't reference either typeclass, so we force their +-- inclusion via `include hg hp`. -include hg in -- Necessary because a • B does not need hg, so the elaborator does not bind it. - -- A degenerate module is cryptographically insecure. /-- Diffie–Hellman primitive: the scalar action `a • B`. Gated unconditionally -on `[IsHonestGenerator F G]` (via `include hg` in this section) — this file -does not formalize DH on degenerate modules. -/ +on `[IsHonestGenerator F G]` and `[Fact (Nat.Prime (Fintype.card F))]` — +this file does not formalize DH on degenerate or composite-order modules. -/ abbrev dh (a : F) (B : G) : G := a • B +end -omit hg in -- Because dh already carries hg. /-- **Shared secret in canonical form.** Either party's computation lands on `(a * b) • B` — a single closed expression independent of which side performs the final scalar action. -/ @@ -104,7 +126,6 @@ theorem shared_eq_mul (a b : F) (B : G) : change b • (a • B) = (a * b) • B rw [← mul_smul, mul_comm b a] -omit hg in -- Because dh already carries hg. /-- **Agreement.** Two parties starting from a common base point `B`, with private scalars `a` and `b`, compute the same shared point. Corollary of `shared_eq_mul` by commutativity of multiplication in `F`. -/ diff --git a/references.bib b/references.bib index e6645c5f0..1f65cd4f5 100644 --- a/references.bib +++ b/references.bib @@ -371,3 +371,10 @@ @incollection{WinskelNielsen1995 eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, } +@misc{ VCVio26, + author = {Tuma, Devon and Dao, Quang and Waters, James and Hicks, Alexander and Hopper, Nicholas}, + title = {{VCVio}: Verified Cryptography in {Lean} via Oracle Effects and Handlers}, + howpublished = {Cryptology {ePrint} Archive, Paper 2026/899}, + year = {2026}, + url = {https://eprint.iacr.org/2026/899}, +}