From 68a08972c63353ab0c6198f42ee1c83b9ca2fe43 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 2 Oct 2026 23:27:56 -0400 Subject: [PATCH 1/3] =?UTF-8?q?fix(DiffieHellman):=20use=20each=20role?= =?UTF-8?q?=E2=80=99s=20own=20private=20exponent?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../DiffieHellman/Basic.lean | 4 ++-- CslibTests/DiffieHellman.lean | 23 +++++++++++++++---- 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean index 390a43354..f0d04272c 100644 --- a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean +++ b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean @@ -108,7 +108,7 @@ inductive Params.Val | nat (n : ℕ) | zMod (z : ZMod params.p) /-- Alice's expression for computing the public message. -/ abbrev aliceComputeMesg : Expr Var params.Val FunId := Expr.call .computePublicMessage - [.val <| .nat params.p, .val <| .zMod params.g, .val <| .nat params.b] + [.val <| .nat params.p, .val <| .zMod params.g, .val <| .nat params.a] /-- Alice's expression for computing the shared secret. -/ abbrev aliceComputeSharedSecret : Expr Var params.Val FunId := @@ -121,7 +121,7 @@ abbrev bobComputeMesg : Expr Var params.Val FunId := /-- Bob's expression for computing the shared secret. -/ abbrev bobComputeSharedSecret : Expr Var params.Val FunId := - Expr.call .computeSharedSecret [.val <| .nat params.p, params.x, .val <| .nat params.a] + Expr.call .computeSharedSecret [.val <| .nat params.p, params.x, .val <| .nat params.b] /-- Alice's program. -/ def alice : Process Pid Var params.Val FunId params.SelLabel params.ProcName := diff --git a/CslibTests/DiffieHellman.lean b/CslibTests/DiffieHellman.lean index be0ab8481..9e8039258 100644 --- a/CslibTests/DiffieHellman.lean +++ b/CslibTests/DiffieHellman.lean @@ -12,19 +12,32 @@ open Cslib.Mech Cslib.Algorithms.StatefulProcesses.DiffieHellman variable {Pid Var : Type*} (params : Params Pid Var) --- Each final key computation can evaluate after receiving a field element. +-- Each role must use its own exponent in its public message. +example (σ : LocalStore Var params.Val) : + (funEval params).EvalExpr σ (aliceComputeMesg params) (.zMod (params.g ^ params.a)) := by + apply FunCallEval.EvalExpr.call (.cons .val (.cons .val (.cons .val .nil))) + intro hmod + rfl + +example (σ : LocalStore Var params.Val) : + (funEval params).EvalExpr σ (bobComputeMesg params) (.zMod (params.g ^ params.b)) := by + apply FunCallEval.EvalExpr.call (.cons .val (.cons .val (.cons .val .nil))) + intro hmod + rfl + +-- Each role must also use its own exponent on the received message. example (σ : LocalStore Var params.Val) (message : ZMod params.p) (h : σ params.y = .zMod message) : - ∃ key, (funEval params).EvalExpr σ (aliceComputeSharedSecret params) (.zMod key) := by - refine ⟨message ^ params.a, .call (.cons .val (.cons .var (.cons .val .nil))) ?_⟩ + (funEval params).EvalExpr σ (aliceComputeSharedSecret params) (.zMod (message ^ params.a)) := by + apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) simp only [h, funEval] intro hmod rfl example (σ : LocalStore Var params.Val) (message : ZMod params.p) (h : σ params.x = .zMod message) : - ∃ key, (funEval params).EvalExpr σ (bobComputeSharedSecret params) (.zMod key) := by - refine ⟨message ^ params.a, .call (.cons .val (.cons .var (.cons .val .nil))) ?_⟩ + (funEval params).EvalExpr σ (bobComputeSharedSecret params) (.zMod (message ^ params.b)) := by + apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) simp only [h, funEval] intro hmod rfl From 08385e310bd50cf575b6202f61755a42c193bb8a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 6 Oct 2026 14:24:58 -0400 Subject: [PATCH 2/3] fix(DiffieHellman): reject mismatched moduli (#1042) The evaluator expressed modulus equality as an implication, so a call with the wrong modulus accepted every result. Require modulus equality together with the expected computed value. Adds a regression check rejecting every result for both functions when the modulus differs, while retaining the valid role-evaluation checks. The field elements already have type `ZMod params.p`, so the corrected relation also avoids the old dependent casts. Depends on #1041 (the role-exponent fix); this PR targets that branch. Implemented with Codex. --- .../DiffieHellman/Basic.lean | 7 ++++--- CslibTests/DiffieHellman.lean | 20 +++++++++---------- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean index f0d04272c..2b7187b98 100644 --- a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean +++ b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean @@ -139,12 +139,13 @@ def bob : Process Pid Var params.Val FunId params.SelLabel params.ProcName := /-! ## Semantics -/ -/-- Implementation of local function call evaluation. -/ +/-- Implementation of local function call evaluation. +Calls with a mismatched modulus are rejected. -/ def funEval : FunCallEval FunId params.Val | .computePublicMessage, [.nat p, .zMod g, .nat privateExp], v => - (h : p = params.p) → v = (.zMod <| h ▸ computePublicMessage p (h ▸ g) privateExp) + p = params.p ∧ v = .zMod (computePublicMessage params.p g privateExp) | .computeSharedSecret, [.nat p, .zMod msg, .nat privateExp], v => - (h : p = params.p) → v = (.zMod <| h ▸ computeSharedSecret p (h ▸ msg) privateExp) + p = params.p ∧ v = .zMod (computeSharedSecret params.p msg privateExp) | _, _, _ => False /-- DH network. -/ diff --git a/CslibTests/DiffieHellman.lean b/CslibTests/DiffieHellman.lean index 9e8039258..076a6a5e3 100644 --- a/CslibTests/DiffieHellman.lean +++ b/CslibTests/DiffieHellman.lean @@ -16,30 +16,30 @@ variable {Pid Var : Type*} (params : Params Pid Var) example (σ : LocalStore Var params.Val) : (funEval params).EvalExpr σ (aliceComputeMesg params) (.zMod (params.g ^ params.a)) := by apply FunCallEval.EvalExpr.call (.cons .val (.cons .val (.cons .val .nil))) - intro hmod - rfl + exact ⟨rfl, rfl⟩ example (σ : LocalStore Var params.Val) : (funEval params).EvalExpr σ (bobComputeMesg params) (.zMod (params.g ^ params.b)) := by apply FunCallEval.EvalExpr.call (.cons .val (.cons .val (.cons .val .nil))) - intro hmod - rfl + exact ⟨rfl, rfl⟩ -- Each role must also use its own exponent on the received message. example (σ : LocalStore Var params.Val) (message : ZMod params.p) (h : σ params.y = .zMod message) : (funEval params).EvalExpr σ (aliceComputeSharedSecret params) (.zMod (message ^ params.a)) := by apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) - simp only [h, funEval] - intro hmod - rfl + simp [h, funEval, computeSharedSecret] example (σ : LocalStore Var params.Val) (message : ZMod params.p) (h : σ params.x = .zMod message) : (funEval params).EvalExpr σ (bobComputeSharedSecret params) (.zMod (message ^ params.b)) := by apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) - simp only [h, funEval] - intro hmod - rfl + simp [h, funEval, computeSharedSecret] + +-- A mismatched modulus must reject every result for either function. +example (f : FunId) (p : ℕ) (hp : p ≠ params.p) (message : ZMod params.p) + (privateExp : ℕ) (v : params.Val) : + ¬ funEval params f [.nat p, .zMod message, .nat privateExp] v := by + cases f <;> exact fun h => hp h.1 end CslibTests.DiffieHellman From 7f021b315abaeb369e21a0a1116c824cc4881950 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 6 Oct 2026 14:26:24 -0400 Subject: [PATCH 3/3] fix(DiffieHellman): state correctness over complete executions (#1044) The correctness statement assumed that the initial network reached `0` in one transition, which is impossible. Use `MTr` so the statement covers complete executions. Adds a regression proof constructing a four-step execution from any initial store, with both final keys equal to `g ^ (a * b)`. Depends on #1042 (the modulus-check fix); this PR targets that branch. Implemented with Codex. --- .../DiffieHellman/Basic.lean | 4 +- CslibTests/DiffieHellman.lean | 58 ++++++++++++++++++- 2 files changed, 59 insertions(+), 3 deletions(-) diff --git a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean index 2b7187b98..e2e13b1be 100644 --- a/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean +++ b/Cslib/Algorithms/StatefulProcesses/DiffieHellman/Basic.lean @@ -195,9 +195,9 @@ abbrev Params.cfgLts {SelLabel ProcName : Type*} := Cfg.lts (Pid := Pid) (Var := Var) (SelLabel := SelLabel) (ProcName := ProcName) (fun _ => False) (funEval params) -/- Functional correctness of the Diffie-Hellman protocol. -/ +/- Functional correctness of the Diffie-Hellman protocol over complete executions. -/ proof_wanted net_fun_correct - (hmtr : params.cfgLts.Tr ⟨net params, gs⟩ μs ⟨0, gs'⟩) : + (hmtr : params.cfgLts.MTr ⟨net params, gs⟩ μs ⟨0, gs'⟩) : (gs' params.alice) params.s = (gs' params.bob) params.s end Cslib.Algorithms.StatefulProcesses.DiffieHellman diff --git a/CslibTests/DiffieHellman.lean b/CslibTests/DiffieHellman.lean index 076a6a5e3..9416388d4 100644 --- a/CslibTests/DiffieHellman.lean +++ b/CslibTests/DiffieHellman.lean @@ -8,7 +8,7 @@ import Cslib.Algorithms.StatefulProcesses.DiffieHellman.Basic namespace CslibTests.DiffieHellman -open Cslib.Mech Cslib.Algorithms.StatefulProcesses.DiffieHellman +open Cslib Cslib.Mech Cslib.StatefulProcesses Cslib.Algorithms.StatefulProcesses.DiffieHellman variable {Pid Var : Type*} (params : Params Pid Var) @@ -42,4 +42,60 @@ example (f : FunId) (p : ℕ) (hp : p ≠ params.p) (message : ZMod params.p) ¬ funEval params f [.nat p, .zMod message, .nat privateExp] v := by cases f <;> exact fun h => hp h.1 +-- A complete execution exists from every initial store and produces the expected key. +theorem complete_run [DecidableEq Pid] [DecidableEq Var] + (gs : GlobalStore Pid Var params.Val) : + ∃ gs' μs, μs.length = 4 ∧ params.cfgLts.MTr ⟨net params, gs⟩ μs ⟨0, gs'⟩ ∧ + (gs' params.alice) params.s = .zMod (params.g ^ (params.a * params.b)) ∧ + (gs' params.bob) params.s = .zMod (params.g ^ (params.a * params.b)) := by + let aliceMsg : params.Val := .zMod (params.g ^ params.a) + let bobMsg : params.Val := .zMod (params.g ^ params.b) + let key : params.Val := .zMod (params.g ^ (params.a * params.b)) + let cfg₁ := Cfg.mk ((net params)[params.alice := alice₁ params][params.bob := bob₁ params]) + (gs[(params.bob, params.x) := aliceMsg]) + let cfg₂ := Cfg.mk (cfg₁.net[params.bob := bob₂ params][params.alice := alice₂ params]) + (cfg₁.store[(params.alice, params.y) := bobMsg]) + let cfg₃ := Cfg.mk (Function.update cfg₂.net params.alice 0) + (cfg₂.store[(params.alice, params.s) := key]) + refine ⟨cfg₃.store[(params.bob, params.s) := key], + [.com params.alice params.bob aliceMsg, .com params.bob params.alice bobMsg, + .local params.alice, .local params.bob], rfl, + .stepL (s2 := cfg₁) ?_ (.stepL (s2 := cfg₂) ?_ (.stepL (s2 := cfg₃) ?_ (.single _ ?_))), + ?_, ?_⟩ + · apply Cfg.Tr.com (e := aliceComputeMesg params) (hstore := rfl) + · refine Network.Tr.com ?_ ?_ rfl + · simp only [net, HasSubstitution.subst, Function.update_of_ne params.alice_neq_bob, + Function.update_self] + exact .pre + · simp only [net, HasSubstitution.subst, Function.update_self] + exact .pre + · exact .call (.cons .val (.cons .val (.cons .val .nil))) ⟨rfl, rfl⟩ + · apply Cfg.Tr.com (e := bobComputeMesg params) (hstore := rfl) + · refine Network.Tr.com ?_ ?_ rfl + · simp only [cfg₁, HasSubstitution.subst, Function.update_self] + exact .pre + · simp only [cfg₁, HasSubstitution.subst, Function.update_of_ne params.alice_neq_bob, + Function.update_self] + exact .pre + · exact .call (.cons .val (.cons .val (.cons .val .nil))) ⟨rfl, rfl⟩ + · apply Cfg.Tr.assign (x := params.s) (e := aliceComputeSharedSecret params) (hstore := rfl) + · refine Network.Tr.local rfl ?_ rfl + simp only [cfg₂, HasSubstitution.subst, Function.update_self] + exact .pre + · apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) + simp [cfg₂, HasSubstitution.subst, key, bobMsg, funEval, computeSharedSecret, + ← pow_mul, Nat.mul_comm] + · apply Cfg.Tr.assign (x := params.s) (e := bobComputeSharedSecret params) (hstore := rfl) + · apply Network.Tr.local (prP := 0) rfl + · simp only [cfg₃, cfg₂, HasSubstitution.subst, + Function.update_of_ne (Ne.symm params.alice_neq_bob), Function.update_self] + exact .pre + · ext p + simp +contextual [cfg₃, cfg₂, cfg₁, net, HasSubstitution.subst, Function.update_apply] + · apply FunCallEval.EvalExpr.call (.cons .val (.cons .var (.cons .val .nil))) + simp [cfg₃, cfg₂, cfg₁, HasSubstitution.subst, key, aliceMsg, funEval, computeSharedSecret, + ← pow_mul, Ne.symm params.alice_neq_bob] + · simp [cfg₃, HasSubstitution.subst, params.alice_neq_bob, key] + · simp [HasSubstitution.subst, key] + end CslibTests.DiffieHellman