mirror of
https://github.com/luxfi/pulsar.git
synced 2026-07-26 22:53:49 +00:00
fix(ec): delete stale V04 leaking-path orphan; machine-check all EC theories; scrub v0.4 refs; comment-aware budget
This commit is contained in:
Antje Worring
+25
-35
@@ -3,43 +3,33 @@
|
||||
# count drifts ABOVE these. The honest goal is to DECREASE them (discharge
|
||||
# axioms/admits into proved lemmas), never to raise the ceiling.
|
||||
#
|
||||
# Current surface. The axioms are fully bucketed in AXIOM-INVENTORY.md:
|
||||
# A standard-math-fact (16/17) | B serialization/layout (42) |
|
||||
# C OPEN security assumption (22; see AXIOM-INVENTORY.md / BLOCKERS.md).
|
||||
# Per-bucket breakdown is authoritative in AXIOM-INVENTORY.md:
|
||||
# A standard-math-fact | B serialization/layout | C OPEN security assumption (19).
|
||||
#
|
||||
# THIS PASS — no-leak de-misdirection (NOT a raw count reduction; an
|
||||
# assurance-QUALITY improvement). No EC toolchain on host => no hand EC
|
||||
# proof can be machine-rechecked here, and every in-file-derivable axiom is
|
||||
# already a proved lemma. What changed:
|
||||
# * Added proofs/easycrypt/Pulsar_N1_NoLeak.ec, the HONEST production model:
|
||||
# the masked Lagrange aggregate equals central z WITHOUT forming the
|
||||
# master secret, the hint is recovered from PUBLIC w', and the ONLY open
|
||||
# assumption is a STANDARD Module-LWE/MSIS reduction (no implementation
|
||||
# reconstruct). This ADDS 2 axioms (public_hint_roundtrip [B],
|
||||
# no_leak_reduction [C-standard]) -> AXIOM 87 -> 89.
|
||||
# * The CORRECTNESS CORE of that model is MACHINE-CHECKED in Lean 4+Mathlib
|
||||
# on this host (lake build green, 0 sorry): Crypto.Pulsar.NoLeakAggregate
|
||||
# + Crypto.Pulsar.BoundaryClearance + Crypto.Threshold_Lagrange. The 2 new
|
||||
# EC axioms are procedure-level wrappers of those machine-checked facts
|
||||
# (public_hint_roundtrip) and the disclosed standard reduction
|
||||
# (no_leak_reduction); both are recheck-pending ec-compile (CI gate).
|
||||
# * The reconstruct-then-sign combine_body_axiom cone is RE-LABELLED in
|
||||
# AXIOM-INVENTORY.md / reviewed-axioms.txt as the IDEALISED-CORRECTNESS
|
||||
# model; the production residual is now the standard reduction above.
|
||||
# Net: +2 disclosed standard-assumption axioms, in exchange for replacing the
|
||||
# headline reconstruct-then-sign residual with a Module-LWE/MSIS reduction
|
||||
# whose algebraic core is machine-checked. Honesty over a flat count.
|
||||
# EC TOOLCHAIN IS LIVE ON THIS HOST. EasyCrypt (opam switch `proofs`) +
|
||||
# z3/alt-ergo machine-check all top-level + lemmas/ theories via
|
||||
# `easycrypt compile`; the framework gate runs checks/ec-machine-check.sh
|
||||
# every invocation, and pulsar passes 14/14. (The earlier "no EC toolchain on
|
||||
# host / recheck-pending ec-compile" note was FALSE and is removed.)
|
||||
#
|
||||
# COUNT NOTE: AXIOM=89 is what axiom-budget.sh's regex counts. Only 80 are
|
||||
# real `axiom`/`declare axiom` DECLARATIONS (78 prior + 2 new) -- the regex
|
||||
# also matches 9 comment lines inside (* ... *) blocks that begin with the
|
||||
# word "axiom". The gate only fails on an INCREASE, so this neither hides nor
|
||||
# inflates.
|
||||
# Two things changed the count since the no-leak pass:
|
||||
# * Deleted proofs/easycrypt/V04_Sign_Ctx.ec -- a stale orphan for the v0.4
|
||||
# ctx-bound AlgebraicAggregate leaking path (sibling of the removed v0.3
|
||||
# path). It never compiled (missing FIPS204_Axioms theory, no .eco). This
|
||||
# removes 5 axiom declarations (empty_bytes_len/byte_of_zero/bytes_cat_empty_l
|
||||
# [was B41], mldsa_sign_ctx_axiom [was C15], algebraic_aggregate_ctx_body_axiom
|
||||
# [was C16 -- the reconstruct-then-sign axiom in its starkest form]).
|
||||
# * The no-leak production model (Pulsar_N1_NoLeak.ec) remains: the masked
|
||||
# Lagrange aggregate equals central z WITHOUT forming the master secret;
|
||||
# hint from PUBLIC w'; the only open assumption is a STANDARD Module-LWE/MSIS
|
||||
# reduction. Correctness core MACHINE-CHECKED in Lean (Crypto.Pulsar.
|
||||
# NoLeakAggregate + BoundaryClearance + Crypto.Threshold_Lagrange).
|
||||
#
|
||||
# Real `admit.` tactics = 0 (the repo's own scripts/checks/ec-admits.sh, which
|
||||
# matches ^admit.$, is authoritative). ADMIT=12 below is the budget regex
|
||||
# counting the WORD "admit" in comments; informational only.
|
||||
# Counts below are the comment-aware machine counts (axiom-budget.sh strips
|
||||
# (* *) comments first, so prose like "DISCHARGED (no admit)" no longer
|
||||
# inflates): real `admit`/`abort` tactics = 0; AXIOM = real declaration count
|
||||
# (was 80 hand-counted; 80 - 5 deleted V04 axioms = 75).
|
||||
SORRY=0
|
||||
ADMIT=12
|
||||
AXIOM=89
|
||||
ADMIT=0
|
||||
AXIOM=75
|
||||
VACUOUS=0
|
||||
|
||||
+5
-1
@@ -471,7 +471,11 @@ ok github.com/luxfi/pulsar/ref/go/pkg/pulsar 6.026s
|
||||
```
|
||||
|
||||
Jasmin corpus: 23/23 compile (per commit `04cdc24`). EasyCrypt theory
|
||||
`V04_Sign_Ctx.ec` ships in `proofs/easycrypt/`.
|
||||
`V04_Sign_Ctx.ec` was **deleted** (forward-only): it proved byte-equality for
|
||||
the v0.4 ctx-bound `AlgebraicAggregateCtx` — the ctx sibling of the removed
|
||||
v0.3 reconstruct-then-sign leaking path — never compiled (missing
|
||||
`FIPS204_Axioms` theory, no `.eco`), and is no longer in `proofs/easycrypt/`.
|
||||
The remaining 12 top-level theories machine-check clean under `easycrypt compile`.
|
||||
|
||||
## 6. Audit verdict
|
||||
|
||||
|
||||
+12
-8
@@ -212,15 +212,18 @@ underlying op/constant (a verify-gated refactor); not a security claim.
|
||||
| B39 | `committee_quorum_uniq` | …:209 | the canonical quorum is duplicate-free. |
|
||||
| B40 | `committee_quorum_nonempty` | …:210 | the canonical quorum is non-empty. |
|
||||
|
||||
### B.5 — V04 ctx-encoding byte facts
|
||||
### B.5 — V04 ctx-encoding byte facts — **REMOVED (forward-only)**
|
||||
|
||||
| # | Axiom | File:line | Justification |
|
||||
|---|---|---|---|
|
||||
| B41 | `empty_bytes_len` / `byte_of_zero` / `bytes_cat_empty_l` | V04_Sign_Ctx.ec:120–122 | Empty-byte algebra used by `mu_ctx_empty_eq_mu_empty` (counted as one row; three declarations over abstract `empty_bytes`/`byte_of`/`bytes_cat`). |
|
||||
The `V04_Sign_Ctx.ec` proof file was **deleted**: it proved byte-equality for
|
||||
the v0.4 ctx-bound `AlgebraicAggregateCtx` path — the ctx sibling of the v0.3
|
||||
reconstruct-then-sign leaking path removed under PULSAR-V13-HINT-LEAK. The file
|
||||
never compiled (it `require`d a non-existent `FIPS204_Axioms` theory; no `.eco`).
|
||||
Its former axioms `empty_bytes_len` / `byte_of_zero` / `bytes_cat_empty_l` (was
|
||||
B41) are gone from the live set. Historical note only; no proof target imports it.
|
||||
|
||||
---
|
||||
|
||||
## Bucket C — OPEN SECURITY ASSUMPTION (21) — **MUST STAY OPEN**
|
||||
## Bucket C — OPEN SECURITY ASSUMPTION (19) — **MUST STAY OPEN**
|
||||
|
||||
These carry security-relevant content the EC reduction has **not** closed.
|
||||
Every one assumes the extracted/aggregated body equals the **centralised
|
||||
@@ -250,12 +253,13 @@ EC-proven**. Tracked: `BLOCKERS.md` § "EC reconstruct-then-sign model".
|
||||
| C12 | `sign_body_cs1_spec` | …:662 | extracted c·s₁ = `apply_c_to_s1 …` (z-stage sub). |
|
||||
| C13 | `sign_body_w_low_spec` | …:704 | extracted libjade w_low = `central_w_low …` (h-stage). |
|
||||
| C14 | `sign_no_reject_on_accepted_honest_layout` | …:826 | layout + accept ⇒ status=0 (libjade κ-loop accept-path). |
|
||||
| C15 | `mldsa_sign_ctx_axiom` | V04_Sign_Ctx.ec:163 | FIPS 204 §5.4 ctx-bound single-party sign is the trusted base (circl SignTo with ctx). |
|
||||
| C16 | `algebraic_aggregate_ctx_body_axiom` | V04_Sign_Ctx.ec:201 | **The v0.4 reconstruct-then-sign axiom in its starkest form**: `AlgebraicAggregateCtx` output = FIPS 204 §5.4 `SignCtx(sk_master, ctx, M)` where `sk_master` is the **reconstructed** master secret (existentially quantified, "NOT materialised" in Go but assumed to exist and to be what the aggregate equals). Go-discharge is by test + AST sweep, not EC. |
|
||||
| ~~C15~~ | ~~`mldsa_sign_ctx_axiom`~~ | **REMOVED** | Lived in the deleted `V04_Sign_Ctx.ec`; gone with the v0.4 ctx path. |
|
||||
| ~~C16~~ | ~~`algebraic_aggregate_ctx_body_axiom`~~ | **REMOVED** | The v0.4 reconstruct-then-sign axiom in its starkest form — **deleted** with `V04_Sign_Ctx.ec` (forward-only). It is no longer in the proof set; the production no-leak path never instantiated it. |
|
||||
|
||||
> C-cone bundling note: C1/C2 are the section-local module contracts; C3–C14
|
||||
> are the per-stage byte-walk axioms the `*_byte_equality` lemma transitively
|
||||
> rests on; C15–C16 are the V04 ctx path. The histogram lists 21; the table
|
||||
> rests on; C15–C16 (the V04 ctx path) are **removed** with the deleted file.
|
||||
> The histogram lists 19; the table
|
||||
> above enumerates 16 rows. The remaining 5 C-declarations are the
|
||||
> `combine_body_{matrix_a,mask_y}` / `sign_body_{matrix_a,mask_y}` /
|
||||
> `*_no_reject` already shown — i.e. per *declaration* the C set is the 16
|
||||
|
||||
@@ -1,301 +0,0 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Pulsar -- Class N1 byte-equality reduction, v0.4 ctx-bound path *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* *)
|
||||
(* STATUS *)
|
||||
(* Discharged at the abstract level: under the FIPS 204 dispatch *)
|
||||
(* axiom and the polynomial-Shamir reconstruction axiom (both *)
|
||||
(* reused verbatim from Pulsar_N1.ec for the empty-ctx case), the *)
|
||||
(* v0.4 ctx-bound threshold output is byte-equal to a single-party *)
|
||||
(* FIPS 204 §5.4 SignCtx on the same (sk, ctx, M) tuple. The *)
|
||||
(* refinement of the concrete v0.4 algebraic-aggregate body to the *)
|
||||
(* abstract `AlgebraicAggregateCtxAbs` model is the section-local *)
|
||||
(* declared axiom `algebraic_aggregate_ctx_body_axiom` -- discharged *)
|
||||
(* Go-side by the existing graduation gates (TestOrchestrateV03Sign *)
|
||||
(* Ctx_VerifyMatchesFIPS204, TestAlgebraic_NoSkAccess/ *)
|
||||
(* AlgebraicAggregateCtx) and AST-structurally by the *)
|
||||
(* `runAlgebraicAggregateASTChecks` sweep over BOTH *)
|
||||
(* AlgebraicAggregate and AlgebraicAggregateCtx in *)
|
||||
(* threshold_v03_test.go. *)
|
||||
(* *)
|
||||
(* WHAT THIS FILE GIVES REVIEWERS *)
|
||||
(* 1. The v0.4 module-level abstraction: FIPS 204 §5.4 step-2 mu *)
|
||||
(* encoding is decomplected into ONE EasyCrypt operator *)
|
||||
(* `mu_ctx` matching the Go-side `deriveMuCtx`. *)
|
||||
(* 2. A backwards-compat lemma `mu_ctx_empty_eq_mu_empty` that *)
|
||||
(* pins `mu_ctx(tr, nil, M) = mu_empty(tr, M)` where *)
|
||||
(* `mu_empty` is Pulsar_N1.ec's existing empty-ctx mu. *)
|
||||
(* 3. The headline theorem *)
|
||||
(* `threshold_sign_ctx_equiv_fips204_sign_with_ctx` *)
|
||||
(* reducing AlgebraicAggregateCtx output bytes to *)
|
||||
(* MLDSA.signCtx(sk, ctx, M) under the same abstract reductions *)
|
||||
(* Pulsar_N1.ec discharges for the empty-ctx path. *)
|
||||
(* *)
|
||||
(* REFERENCES *)
|
||||
(* - FIPS 204 §5.4 (Algorithm 22 -- M' = 0x00 || |ctx| || ctx || M) *)
|
||||
(* - Pulsar_N1.ec (the empty-ctx companion theory) *)
|
||||
(* - threshold_v03.go::deriveMuCtx (the single Go-side helper this *)
|
||||
(* EasyCrypt operator mirrors byte-for-byte) *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Distr SmtMap.
|
||||
require import FIPS204_Axioms. (* reuses the dispatch axioms from N1 *)
|
||||
require import Pulsar_N1. (* mu_empty, MLDSA.sign, etc. *)
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 1. FIPS 204 §5.4 ctx-bound mu encoding. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* `bytes` is the standard byte-string type carried over from Pulsar_N1. *)
|
||||
type bytes.
|
||||
|
||||
(* SHAKE-256 absorption-and-squeeze, modeled as a deterministic operator
|
||||
over input bytes. The concrete Go implementation lives in
|
||||
golang.org/x/crypto/sha3.NewShake256(); EasyCrypt models it as a ROM
|
||||
in the security argument and as a deterministic function here for the
|
||||
byte-equality reduction (a single dispatch chain, not a security
|
||||
property). *)
|
||||
op shake256_64 (input : bytes) : bytes.
|
||||
|
||||
(* `bytes_cat` is the EasyCrypt concatenation of byte strings (already
|
||||
declared in Pulsar_N1.ec; re-declared here for self-containment). *)
|
||||
op bytes_cat : bytes -> bytes -> bytes.
|
||||
|
||||
(* Single-byte encoding of a length value -- FIPS 204 §5.4 single-byte
|
||||
length prefix. The Go side: `[]byte{byte(len(ctx))}`. *)
|
||||
op byte_of (n : int) : bytes.
|
||||
|
||||
(* The 0x00 length-delimiter byte. *)
|
||||
op zero_byte : bytes.
|
||||
|
||||
(* `bytes_len` reads the byte-length of a byte-string. *)
|
||||
op bytes_len : bytes -> int.
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* The Go-side `deriveMuCtx` mirrored EXACTLY in EasyCrypt. *)
|
||||
(* *)
|
||||
(* The byte-for-byte mirror lets us state *)
|
||||
(* `algebraic_aggregate_ctx_body_axiom : forall sk ctx M, ...` *)
|
||||
(* with the abstract aggregator using `mu_ctx` and the concrete Go *)
|
||||
(* aggregator using `deriveMuCtx`. The structural test *)
|
||||
(* `runAlgebraicAggregateASTChecks` enforces that BOTH *)
|
||||
(* AlgebraicAggregate and AlgebraicAggregateCtx call ONLY this helper. *)
|
||||
(* *)
|
||||
(* mu_ctx(tr, ctx, M) *)
|
||||
(* := shake256_64(tr || 0x00 || byte_of(|ctx|) || ctx || M) *)
|
||||
(* *)
|
||||
(* When ctx = [], |ctx| = 0 and byte_of(0) = 0x00, so *)
|
||||
(* *)
|
||||
(* mu_ctx(tr, [], M) = shake256_64(tr || 0x00 || 0x00 || [] || M) *)
|
||||
(* = shake256_64(tr || 0x00 || 0x00 || M) *)
|
||||
(* *)
|
||||
(* which IS mu_empty(tr, M) verbatim. This is the *)
|
||||
(* `mu_ctx_empty_eq_mu_empty` lemma below. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
op mu_ctx (tr ctx M : bytes) : bytes =
|
||||
shake256_64
|
||||
(bytes_cat tr
|
||||
(bytes_cat zero_byte
|
||||
(bytes_cat (byte_of (bytes_len ctx))
|
||||
(bytes_cat ctx M)))).
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 2. Backwards-compat: empty-ctx ≡ Pulsar_N1.mu_empty. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* Empty bytes -- the empty string carrying length 0. *)
|
||||
op empty_bytes : bytes.
|
||||
|
||||
(* The Pulsar_N1 mu_empty operator (re-imported here for the equality
|
||||
lemma; the model in N1.ec is the same SHAKE-256 absorption shape we
|
||||
restate in `mu_ctx_empty_unfold` for clarity). *)
|
||||
op mu_empty (tr M : bytes) : bytes =
|
||||
shake256_64
|
||||
(bytes_cat tr
|
||||
(bytes_cat zero_byte
|
||||
(bytes_cat zero_byte M))).
|
||||
|
||||
(* AXIOM-FREE algebraic facts about empty bytes. *)
|
||||
axiom empty_bytes_len : bytes_len empty_bytes = 0.
|
||||
axiom byte_of_zero : byte_of 0 = zero_byte.
|
||||
axiom bytes_cat_empty_l (b : bytes) : bytes_cat empty_bytes b = b.
|
||||
|
||||
(* ----------------------------------------------------------------------
|
||||
THE BACKWARDS-COMPAT INVARIANT.
|
||||
|
||||
Holds STRUCTURALLY by the encoding: when ctx = empty, the FIPS 204
|
||||
§5.4 prefix is `0x00 0x00` which is byte-identical to the historical
|
||||
empty-ctx prefix used by Pulsar_N1.mu_empty.
|
||||
|
||||
The Go-side mirror of this lemma is
|
||||
TestOrchestrateV03SignCtx_EmptyCtx_MatchesV03Sign which compares
|
||||
wire bytes from OrchestrateV03Sign(msg) and OrchestrateV03SignCtx(
|
||||
nil, msg) under identical deterministic RNG seeds.
|
||||
---------------------------------------------------------------------- *)
|
||||
|
||||
lemma mu_ctx_empty_eq_mu_empty (tr M : bytes) :
|
||||
mu_ctx tr empty_bytes M = mu_empty tr M.
|
||||
proof.
|
||||
rewrite /mu_ctx /mu_empty empty_bytes_len byte_of_zero.
|
||||
by rewrite (bytes_cat_empty_l M).
|
||||
qed.
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 3. FIPS 204 §5.4 SignCtx as a model dispatch. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* `MLDSA.signCtx` is the FIPS 204 §5.4 single-party ctx-bound sign *)
|
||||
(* dispatch. The empty-ctx variant `MLDSA.sign` in Pulsar_N1.ec is *)
|
||||
(* recovered as `MLDSA.signCtx sk empty_bytes M`. *)
|
||||
|
||||
module type MLDSA_SIGNER_CTX = {
|
||||
proc sign_ctx (sk : bytes, ctx : bytes, M : bytes) : bytes
|
||||
}.
|
||||
|
||||
(* The FIPS 204 dispatch axiom for ctx-bound sign. This is the v0.4 *)
|
||||
(* sibling of the empty-ctx `mldsa_sign_axiom` in Pulsar_N1.ec. *)
|
||||
(* *)
|
||||
(* In words: cloudflare/circl's mldsa{44,65,87}.SignTo with ctx parameter*)
|
||||
(* is the FIPS 204 reference implementation; this axiom names the *)
|
||||
(* trusted base. *)
|
||||
|
||||
axiom mldsa_sign_ctx_axiom :
|
||||
forall (sk ctx M : bytes),
|
||||
bytes_len ctx <= 255 =>
|
||||
exists (s : bytes),
|
||||
Pr[ MLDSA_SIGNER_CTX.sign_ctx (sk, ctx, M) @ &m : true ] = 1%r /\
|
||||
s = mu_ctx (tr_of sk) ctx M.
|
||||
|
||||
(* `tr_of sk` extracts the FIPS 204 §6 tr = SHAKE-256(pk, 64) hash *)
|
||||
(* from sk. Same operator used in Pulsar_N1.ec. *)
|
||||
op tr_of : bytes -> bytes.
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 4. Abstract v0.4 ctx-bound aggregator. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* Abstract model of AlgebraicAggregateCtx. Carries ctx as an explicit *)
|
||||
(* parameter; the underlying field arithmetic and rejection-restart *)
|
||||
(* loop are byte-identical to AlgebraicAggregate, modulo mu_ctx replacing*)
|
||||
(* mu_empty as the prehash. *)
|
||||
|
||||
module type ALGEBRAIC_AGGREGATE_CTX = {
|
||||
proc aggregate_ctx
|
||||
(setup : bytes, (* group public material (no sk) *)
|
||||
ctx : bytes,
|
||||
M : bytes,
|
||||
round1 : bytes list,
|
||||
round2 : bytes list) : bytes
|
||||
}.
|
||||
|
||||
(* Refinement axiom: the concrete Go-side AlgebraicAggregateCtx body *)
|
||||
(* is observationally equivalent to FIPS 204 §5.4 SignCtx on the *)
|
||||
(* RECONSTRUCTED master sk, with mu derived via mu_ctx. The Go-side *)
|
||||
(* discharge: TestOrchestrateV03SignCtx_VerifyMatchesFIPS204 (mldsa65. *)
|
||||
(* Verify accepts the wire bytes under (pk, M, ctx)). The structural *)
|
||||
(* discharge: runAlgebraicAggregateASTChecks /AlgebraicAggregateCtx *)
|
||||
(* confirms the body cannot reach a sk-bearing primitive, so the Class *)
|
||||
(* N1 dispatch must factor through the FIPS 204 verifier verbatim. *)
|
||||
|
||||
axiom algebraic_aggregate_ctx_body_axiom :
|
||||
forall (setup ctx M : bytes) (round1 round2 : bytes list)
|
||||
(sk : bytes),
|
||||
(* sk is the master ML-DSA secret reconstructed from any t-quorum of
|
||||
the algebraic shares -- the value EXISTS in the security model
|
||||
but is NOT materialised anywhere in the Go body (enforced AST-
|
||||
structurally by TestAlgebraic_NoSkAccess/AlgebraicAggregateCtx). *)
|
||||
is_master_sk_for_setup sk setup =>
|
||||
bytes_len ctx <= 255 =>
|
||||
Pr[ ALGEBRAIC_AGGREGATE_CTX.aggregate_ctx
|
||||
(setup, ctx, M, round1, round2) @ &m : true ] = 1%r =>
|
||||
exists (s : bytes),
|
||||
(* The byte-identity step: AlgebraicAggregateCtx output = FIPS 204
|
||||
§5.4 SignCtx(sk, ctx, M). *)
|
||||
Pr[ MLDSA_SIGNER_CTX.sign_ctx (sk, ctx, M) @ &m : true ] = 1%r =>
|
||||
s = mu_ctx (tr_of sk) ctx M.
|
||||
|
||||
(* `is_master_sk_for_setup` is the predicate stating that sk is the
|
||||
master ML-DSA private key whose public key is bound into setup.Pub.
|
||||
The Pulsar threshold protocol guarantees existence of such an sk
|
||||
(by FIPS 204 keygen + Shamir-share reconstruction in the security
|
||||
model) but the aggregator NEVER computes it. *)
|
||||
|
||||
op is_master_sk_for_setup : bytes -> bytes -> bool.
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 5. THE HEADLINE THEOREM. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* THEOREM threshold_sign_ctx_equiv_fips204_sign_with_ctx *)
|
||||
(* *)
|
||||
(* For any setup, any t-quorum's (round1, round2) transcripts, any *)
|
||||
(* ctx string of length <= 255, and any message M, the output of *)
|
||||
(* AlgebraicAggregateCtx is byte-equal to FIPS 204 §5.4 *)
|
||||
(* SignCtx(sk_master, ctx, M) where sk_master is the (existentially- *)
|
||||
(* quantified) master secret key whose public key is bound into *)
|
||||
(* setup.Pub. *)
|
||||
(* *)
|
||||
(* This is the v0.4 sibling of `pulsar_n1_byte_equality` in *)
|
||||
(* Pulsar_N1.ec. *)
|
||||
|
||||
lemma threshold_sign_ctx_equiv_fips204_sign_with_ctx :
|
||||
forall (setup ctx M : bytes) (round1 round2 : bytes list)
|
||||
(sk : bytes),
|
||||
is_master_sk_for_setup sk setup =>
|
||||
bytes_len ctx <= 255 =>
|
||||
Pr[ ALGEBRAIC_AGGREGATE_CTX.aggregate_ctx
|
||||
(setup, ctx, M, round1, round2) @ &m : true ] = 1%r =>
|
||||
Pr[ MLDSA_SIGNER_CTX.sign_ctx (sk, ctx, M) @ &m : true ] = 1%r =>
|
||||
exists (s_agg s_mldsa : bytes),
|
||||
s_agg = mu_ctx (tr_of sk) ctx M /\
|
||||
s_mldsa = mu_ctx (tr_of sk) ctx M /\
|
||||
s_agg = s_mldsa.
|
||||
proof.
|
||||
move=> setup ctx M round1 round2 sk Hmaster Hctxlen Hagg Hsign.
|
||||
have Hb := algebraic_aggregate_ctx_body_axiom
|
||||
setup ctx M round1 round2 sk Hmaster Hctxlen Hagg.
|
||||
have Hsx := mldsa_sign_ctx_axiom sk ctx M Hctxlen.
|
||||
case: Hb => s_agg Hagg_eq.
|
||||
case: Hsx => s_mldsa [_ Hmldsa_eq].
|
||||
exists s_agg s_mldsa.
|
||||
split; first by apply Hagg_eq; apply Hsign.
|
||||
split; first by apply Hmldsa_eq.
|
||||
have Hagg_val : s_agg = mu_ctx (tr_of sk) ctx M.
|
||||
by apply Hagg_eq; apply Hsign.
|
||||
by rewrite Hagg_val Hmldsa_eq.
|
||||
qed.
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
(* Section 6. Corollary -- empty-ctx specialisation. *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* When ctx = empty_bytes the headline theorem specialises to the *)
|
||||
(* v0.3 empty-ctx byte-equality from Pulsar_N1.ec, modulo the rename *)
|
||||
(* MLDSA.sign = MLDSA.signCtx(_, empty_bytes, _). *)
|
||||
|
||||
lemma threshold_sign_empty_ctx_equiv_v03 :
|
||||
forall (setup M : bytes) (round1 round2 : bytes list)
|
||||
(sk : bytes),
|
||||
is_master_sk_for_setup sk setup =>
|
||||
Pr[ ALGEBRAIC_AGGREGATE_CTX.aggregate_ctx
|
||||
(setup, empty_bytes, M, round1, round2) @ &m : true ] = 1%r =>
|
||||
Pr[ MLDSA_SIGNER_CTX.sign_ctx (sk, empty_bytes, M) @ &m : true ] = 1%r =>
|
||||
exists (s : bytes),
|
||||
s = mu_empty (tr_of sk) M.
|
||||
proof.
|
||||
move=> setup M round1 round2 sk Hmaster Hagg Hsign.
|
||||
have Hctxlen : bytes_len empty_bytes <= 255.
|
||||
by rewrite empty_bytes_len; smt().
|
||||
have Hthm := threshold_sign_ctx_equiv_fips204_sign_with_ctx
|
||||
setup empty_bytes M round1 round2 sk
|
||||
Hmaster Hctxlen Hagg Hsign.
|
||||
case: Hthm => s_agg s_mldsa [Hagg_val [Hmldsa_val Hbyte_eq]].
|
||||
exists s_agg.
|
||||
rewrite Hagg_val.
|
||||
by apply mu_ctx_empty_eq_mu_empty.
|
||||
qed.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* End of theory V04_Sign_Ctx. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
Reference in New Issue
Block a user