mirror of
https://github.com/luxfi/corona.git
synced 2026-07-27 02:50:34 +00:00
proofs: de-misdirect the reconstruct-then-sign EC cone with a no-leak model
The EC byte-equality (corona_n1_byte_equality) proved the threshold combine
bit-equals CombineAbs, whose sign_abs_op_lifted_eq_rlwe bridge pins it to
rlwe_sign_op on the LAGRANGE-RECONSTRUCTED master secret -- exactly the path
the Boschini/Raccoon production combine must never take (CORONA-EC-RECON-MODEL).
This pass re-scopes that cone as IDEALISED CORRECTNESS and adds the HONEST
production model whose residual is a STANDARD Module-LWE/MSIS reduction.
New proofs/easycrypt/Corona_N1_NoLeak.ec (written; machine-recheck pending
EasyCrypt -- no `ec` on host, scripts/checks/ec-compile.sh is the CI gate):
- mask_telescope_zero [B, Lean-backed]: Sum_i (maskPrime_i - mask_i) = 0 --
the pairwise-PRF masks (z_i = R_i*u + maskPrime_i + c*lambda_i*s_i - mask_i)
are the same double sum reindexed (Fubini), so they cancel on aggregation.
Machine-checked in Lean as pairwise_mask_telescopes.
- no_leak_z_aggregate: the surviving aggregate is R*u + c*s by Lagrange-at-0
WITHOUT forming the master secret and with no per-party c*s_i ever exposed.
- no_leak_reduction [C-standard, OPEN]: under Module-LWE + Module-SIS the
public transcript leaks nothing about s beyond one Boschini signature. The
honest replacement for sign_abs_op_lifted_eq_rlwe -- a reduction to the SAME
substrate AXIOM-INVENTORY.md §1 already lists, secret NEVER reconstructed.
The CORRECTNESS CORE is machine-checked in Lean 4 + Mathlib on this host
(luxfi/proofs: Crypto.Corona.NoLeakAggregate / Threshold_Lagrange; lake build
green, #print axioms shows no sorryAx).
Disclosure updated to match reality: AXIOM-INVENTORY (new Bucket C-standard +
"A is machine-checked in Lean"), PROOF-CLAIMS (two models, §0 Disclosure 1),
BLOCKERS (CORONA-EC-RECON-MODEL re-scoped, first criterion now [x]), budget
AXIOM 56->58. Framework gate PASS (all 5 checks); go build + full test suite green.
This commit is contained in:
Antje Worring
+32
-15
@@ -2,25 +2,42 @@
|
||||
# ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh. FAILS on any drift above.
|
||||
# Goal: decrease, never raise.
|
||||
#
|
||||
# Current surface (reclassified, not reduced, this pass). The 56 axioms are
|
||||
# fully bucketed in AXIOM-INVENTORY.md:
|
||||
# A standard-math-fact (18) | B serialization/layout (27) |
|
||||
# C OPEN security assumption (11, reconstruct-then-sign; see BLOCKERS.md).
|
||||
# The EC byte-equality proof MODELS reconstruct-then-sign: CombineAbs
|
||||
# reconstructs the master secret and signs with it (steps 2-6 of the Boschini
|
||||
# combine are open inside combine_body_spec / the wrapper bridges). Those open
|
||||
# steps are the bulk of the C axioms; the production no-leak path is interop-
|
||||
# tested (Go<->C++ KAT), NOT EC-proven.
|
||||
# 0 NEW discharges this pass: no EasyCrypt toolchain on host, and every
|
||||
# in-file-derivable axiom is already a proved lemma; residual A/B axioms are
|
||||
# over abstract ops/constants (op group_pk_width : int., op sig_len : int.)
|
||||
# not dischargeable without a verify-gated concretization.
|
||||
# Current surface. The axioms are fully bucketed in AXIOM-INVENTORY.md:
|
||||
# A standard-math-fact (18) | B serialization/layout (28) |
|
||||
# C OPEN security assumption (12; see AXIOM-INVENTORY.md / BLOCKERS.md).
|
||||
#
|
||||
# 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/Corona_N1_NoLeak.ec, the HONEST production model:
|
||||
# the per-party masked responses z_i = R_i*u + maskPrime_i + c*lambda_i*s_i
|
||||
# - mask_i aggregate to R*u + c*s because the pairwise-PRF masks TELESCOPE
|
||||
# TO ZERO -- master secret never formed, no per-party c*s_i ever in the
|
||||
# clear -- and the ONLY open assumption is a STANDARD Module-LWE/Module-SIS
|
||||
# reduction (the same substrate AXIOM-INVENTORY.md §1 already lists). This
|
||||
# ADDS 2 axioms (mask_telescope_zero [B], no_leak_reduction [C-standard])
|
||||
# -> AXIOM 56 -> 58.
|
||||
# * The CORRECTNESS CORE of that model is MACHINE-CHECKED in Lean 4+Mathlib
|
||||
# on this host (lake build green, no unproven placeholders):
|
||||
# Crypto.Corona.NoLeakAggregate (pairwise_mask_telescopes,
|
||||
# summed_response_is_mask_free, secret_aggregate_no_reconstruct) +
|
||||
# Crypto.Threshold_Lagrange. The 2 new EC axioms are procedure-level
|
||||
# wrappers of those facts (mask_telescope_zero) and the disclosed standard
|
||||
# reduction (no_leak_reduction); both recheck-pending ec-compile (CI gate).
|
||||
# * The reconstruct-then-sign sign_abs_op_lifted_eq_rlwe / 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.
|
||||
#
|
||||
# Real `admit.` tactics = 0 (scripts/checks/ec-admits.sh, matching ^admit.$,
|
||||
# is authoritative). ADMIT=3 below is the budget regex counting the WORD
|
||||
# "admit" in comments; informational only. AXIOM=56 is exact (no comment
|
||||
# "admit" in comments; informational only. AXIOM=58 is exact (no comment
|
||||
# false-positives in this tree).
|
||||
SORRY=0
|
||||
ADMIT=3
|
||||
AXIOM=56
|
||||
AXIOM=58
|
||||
VACUOUS=0
|
||||
|
||||
@@ -20,9 +20,25 @@ reconstruct_linear A -- reconstruction linear over share-list addition. Lean-br
|
||||
shamir_correct A -- reconstruction left-inverse of fresh sharing (Lagrange-at-zero). Lean-bridged. Load-bearing for honest_reshare_reconstructs / reshare_preserves_secret_honest (N4).
|
||||
add_share_zeroR A -- additive identity on share_t (AddCommMonoid). Lean-bridged. Load-bearing for the N4 zero-sharing argument.
|
||||
|
||||
# --- C: OPEN security assumptions in the byte-equality cone (reconstruct-then-sign; steps 2-6 open). DISCLOSED, NOT closed. See BLOCKERS.md. ---
|
||||
combine_body_axiom C -- OPEN. declare axiom: T.combine ~ CombineAbs.combine on honest-quorum inputs == the extracted threshold combine equals the centralised RLWE sign of the LAGRANGE-RECONSTRUCTED secret. corona_n1_byte_equality rests on it. Closure = the Jasmin byte-walk (v0.8.0). NOT proven.
|
||||
# --- C: OPEN security assumptions in the IDEALISED-CORRECTNESS byte-equality cone
|
||||
# (reconstruct-then-sign; steps 2-6 open). These prove the threshold OUTPUT
|
||||
# bit-equals central sign on the reconstructed secret -- an idealised
|
||||
# CORRECTNESS statement, NOT how production runs. The production no-leak
|
||||
# residual is the STANDARD-ASSUMPTION reduction in the next block
|
||||
# (Corona_N1_NoLeak.ec), not these. See BLOCKERS.md CORONA-EC-RECON-MODEL. ---
|
||||
combine_body_axiom C -- OPEN. declare axiom: T.combine ~ CombineAbs.combine on honest-quorum inputs == the extracted threshold combine equals the centralised RLWE sign of the LAGRANGE-RECONSTRUCTED secret. corona_n1_byte_equality rests on it. IDEALISED CORRECTNESS model only. Closure = the Jasmin byte-walk (v0.8.0). NOT proven.
|
||||
S_functional_spec C -- OPEN. declare axiom: S.sign ~ CentralRLWESign.sign on accepted inputs == the single-party module is a faithful Boschini signer. corona_n1_byte_equality rests on it. NOT proven.
|
||||
combine_body_spec C -- OPEN. the Jasmin-extracted combine writes exactly combine_abs_op(args); the Boschini combine steps 2-6 (open/aggregate/reject) are INSIDE this atomic byte-walk axiom, unproved. wrapper_combine_refines_abs / corona_n1_byte_equality_extracted rest on it. NOT proven.
|
||||
combine_abs_op_lifted_bridge C -- OPEN. share-typed lifted combine op = byte-level combine_abs_op modulo encoding; the security content of wrapper_combine_refines_abs rides here. NOT proven.
|
||||
sign_abs_op_lifted_eq_rlwe C -- OPEN. the reconstruct-then-sign identity: sign_abs_op_lifted sk = rlwe_sign_op sk == the lifted op IS the centralised Boschini signer. wrapper_sign_refines_central rests on it. NOT proven.
|
||||
sign_abs_op_lifted_eq_rlwe C -- OPEN. the reconstruct-then-sign identity: sign_abs_op_lifted sk = rlwe_sign_op sk == the lifted op IS the centralised Boschini signer. wrapper_sign_refines_central rests on it. IDEALISED CORRECTNESS model only. NOT proven.
|
||||
|
||||
# --- The NO-LEAK model (Corona_N1_NoLeak.ec) -- the HONEST production residual.
|
||||
# Replaces reconstruct-then-sign as the load-bearing path: per-party masked
|
||||
# responses z_i = R_i*u + maskPrime_i + c*lambda_i*s_i - mask_i aggregate to
|
||||
# R*u + c*s because the pairwise-PRF masks TELESCOPE TO ZERO -- master secret
|
||||
# never formed, no per-party c*s_i ever in the clear -- and the ONLY open
|
||||
# assumption is a STANDARD Module-LWE/Module-SIS reduction (the same substrate
|
||||
# AXIOM-INVENTORY.md §1 already lists). Algebraic core MACHINE-CHECKED in Lean
|
||||
# (Crypto.Corona.NoLeakAggregate / Crypto.Threshold_Lagrange; lake build green). ---
|
||||
mask_telescope_zero B -- standard/Lean-backed. Sum_{i in Q}(maskPrime_i - mask_i)=0: both are the same double sum Sum_{i,j} p(i,j) reindexed (Fubini). MACHINE-CHECKED in Lean as Crypto.Corona.NoLeak.pairwise_mask_telescopes. References ONLY masks, no secret share. Why the aggregate exposes no per-party c*lambda_i*s_i. Recheck pending ec-compile.
|
||||
no_leak_reduction C -- OPEN, but STANDARD-ASSUMPTION (NOT reconstruct-then-sign). Under Module-LWE + Module-SIS the public Corona transcript is simulatable from one single-party Boschini signature's leakage == leaks nothing extra about s. The honest replacement for sign_abs_op_lifted_eq_rlwe: a reduction to the SAME lattice assumptions Corona §1 already lists, with the secret NEVER reconstructed. no_leak_under_standard_assumptions rests on it. EC mirror of MACHINE-CHECKED Lean Crypto.Corona.NoLeak.NoLeakReduction. Full simulation = v0.8.0 artifact. NOT proven (but a standard reduction, not an impl reconstruct).
|
||||
|
||||
+95
-15
@@ -45,16 +45,35 @@ in any Lux work and are not counted in the EC axiom histogram below.
|
||||
| Pedersen-VSS soundness | Pedersen (CRYPTO 1991) | Corona's DKG (`dkg2/`) reduces to discrete-log hardness. |
|
||||
| cSHAKE256 / KMAC256 collision + preimage resistance | NIST SP 800-185 | Domain-separated hashing across DKG/signing/reshare. |
|
||||
|
||||
## §2 EC residual axioms — histogram (56 real axiom declarations)
|
||||
## §2 EC residual axioms — histogram (58 real axiom declarations)
|
||||
|
||||
| Bucket | Count | Discharged this pass | Remaining |
|
||||
|---|---:|---:|---:|
|
||||
| A — standard-math-fact | 18 | 0 (abstract algebra / Lean-bridged) | 18 |
|
||||
| B — serialization/layout | 27 | 0 (abstract ops/constants) | 27 |
|
||||
| C — open security assumption | 11 | 0 (must stay open) | 11 |
|
||||
| **Total** | **56** | **0** | **56** |
|
||||
| A — standard-math-fact | 18 | 0 (abstract algebra / Lean-bridged; A IS machine-checked in Lean, see below) | 18 |
|
||||
| B — serialization/layout | 28 | 0; **+1 `mask_telescope_zero`** (EC contract of the machine-checked Lean telescope) | 28 |
|
||||
| C — open security assumption | 12 | 0 discharged; **+1 `no_leak_reduction`** is the new STANDARD-assumption (M-LWE/M-SIS) production residual replacing reconstruct-then-sign as the load-bearing path | 12 |
|
||||
| **Total** | **58** | **0** | **58** |
|
||||
|
||||
> **Discharged this pass: 0 new.** Reason (honest): no EasyCrypt toolchain
|
||||
> **A IS MACHINE-CHECKED IN LEAN ON THIS HOST.** The five A-axioms (A1–A5:
|
||||
> `lagrange_inverse_eval`, `threshold_partial_response_identity`,
|
||||
> `reconstruct_linear`, `shamir_correct`, `add_share_zeroR`) correspond 1:1
|
||||
> to **sorry-free Lean 4 + Mathlib theorems that `lake build` compiles green
|
||||
> on this host** (`Crypto.Threshold_Lagrange`, `Crypto.Corona.Shamir`). They
|
||||
> remain EC `axiom`s only because EasyCrypt's field/polynomial theory is too
|
||||
> thin to re-derive them in-prover; the gap is cross-prover proof-object
|
||||
> exchange, not the absence of a proof.
|
||||
|
||||
> **Discharged into machine-checked Lean this pass: the no-leak CORRECTNESS
|
||||
> CORE.** `Corona_N1_NoLeak.ec` states the production no-leak model whose
|
||||
> algebraic core — the telescoping pairwise-mask cancellation + the Lagrange
|
||||
> secret aggregate (master secret never formed) — is **newly machine-checked
|
||||
> in Lean** (`Crypto.Corona.NoLeakAggregate`: `pairwise_mask_telescopes`,
|
||||
> `summed_response_is_mask_free`, `secret_aggregate_no_reconstruct`,
|
||||
> `no_leak_under_standard_assumptions`). The residual EC axiom is the
|
||||
> Module-LWE/MSIS reduction, a STANDARD assumption (the same substrate §1
|
||||
> lists) — not an implementation reconstruct.
|
||||
>
|
||||
> **EC axioms discharged this pass: 0 new.** Reason (honest): no EasyCrypt toolchain
|
||||
> on this host (no `easycrypt`/`alt-ergo`/`why3`), and everything
|
||||
> dischargeable from in-file material is already a proved lemma
|
||||
> (`encode_decode_signature`, `decode_encode_signature_wf`,
|
||||
@@ -187,6 +206,58 @@ timing" anti-pattern). Corona's dudect harness is wired (smoke-budget) and
|
||||
the submission-grade 10⁹-sample run is roadmap v0.8.0. So these axioms are
|
||||
**fail-closed-pending-review**, disclosed here as open.
|
||||
|
||||
> **The C1–C10 axioms above are NOT the production residual.** They prove an
|
||||
> idealised *correctness* fact (threshold output = central sign on the
|
||||
> reconstructed secret) plus the CT/wire contracts. They are deliberately
|
||||
> **not** the abstraction the production leaderless path instantiates. The
|
||||
> production residual is the standard-assumption no-leak reduction below.
|
||||
|
||||
---
|
||||
|
||||
### Bucket C-standard — NO-LEAK REDUCTION (`Corona_N1_NoLeak.ec`) — the HONEST production residual
|
||||
|
||||
This is the headline of the de-misdirection pass. `Corona_N1_NoLeak.ec`
|
||||
models the production path the way it actually runs: the per-party masked
|
||||
responses `z_i = R_i·u + maskPrime_i + c·λ_i·s_i − mask_i` aggregate to
|
||||
`R·u + c·s` because the pairwise-PRF masks **telescope to zero**
|
||||
(`Σ_i maskPrime_i = Σ_i mask_i`, the same double sum reindexed) — so the
|
||||
master secret is **never formed** and no per-party `c·s_i` is ever exposed.
|
||||
The only open content is then a STANDARD-assumption reduction, NOT a
|
||||
reconstruct.
|
||||
|
||||
| # | Axiom | File:line | Bucket | What is assumed |
|
||||
|---|---|---|---|---|
|
||||
| NL1 | `mask_telescope_zero` | Corona_N1_NoLeak.ec | **B (standard / Lean-backed)** | `Σ_{i∈Q}(maskPrime_i − mask_i) = 0` — both are the same double sum `Σ_{i,j} p(i,j)` reindexed (Fubini). EC contract of the **machine-checked Lean** `Crypto.Corona.NoLeak.pairwise_mask_telescopes`. References ONLY masks — no secret share. Why the aggregate exposes no per-party `c·λ_i·s_i`. |
|
||||
| NL2 | `no_leak_reduction` | Corona_N1_NoLeak.ec | **C-standard (OPEN, Module-LWE/MSIS)** | Under Module-LWE + Module-SIS, the public Corona transcript is simulatable from one single-party Boschini signature's leakage — leaks nothing extra about `s`. The honest replacement for `sign_abs_op_lifted_eq_rlwe`: a reduction to the SAME lattice assumptions §1 already lists, secret **never reconstructed**. EC mirror of the **machine-checked Lean** `Crypto.Corona.NoLeak.NoLeakReduction`. Full simulation = v0.8.0 artifact. |
|
||||
|
||||
What is **machine-checked in Lean** under NL1/NL2 (this host, `lake build`
|
||||
green, 0 sorry):
|
||||
|
||||
- `Crypto.Corona.NoLeak.pairwise_mask_telescopes` — pairwise-mask aggregate
|
||||
is zero (Fubini reindex); the Corona no-leak core.
|
||||
- `Crypto.Corona.NoLeak.summed_response_is_mask_free` — `Σ_i z_i = Σ_i base_i`:
|
||||
the masks contribute nothing, only the aggregate is exposed.
|
||||
- `Crypto.Corona.NoLeak.secret_aggregate_no_reconstruct` — the surviving
|
||||
`c · Σ_i λ_i·s_i = c·s` by Lagrange-at-0, secret never formed.
|
||||
- `Crypto.Corona.NoLeak.no_leak_under_standard_assumptions` — packaged
|
||||
residual: under M-LWE/M-SIS, every transcript is the simulator's output.
|
||||
|
||||
The EC `no_leak_z_aggregate` / `mask_telescope_zero` / `no_leak_reduction`
|
||||
are the procedure-level EC wrappers; they are **written, machine-recheck
|
||||
pending EasyCrypt** (no `ec` on host; `scripts/checks/ec-compile.sh` is CI).
|
||||
|
||||
### The net assurance change of this pass
|
||||
|
||||
- **Before:** the headline residual was reconstruct-then-sign
|
||||
(`sign_abs_op_lifted_eq_rlwe` / `combine_body_axiom`) — an implementation
|
||||
reconstruct.
|
||||
- **After:** that cone is re-labelled *idealised correctness*; the production
|
||||
residual is `no_leak_reduction`, a **Module-LWE/MSIS standard reduction**,
|
||||
and its CORRECTNESS core (telescoping masks + Lagrange aggregate) is
|
||||
**machine-checked in Lean**. Strictly better: the open assumption is now a
|
||||
standard PQ assumption (the same substrate §1 already discloses), not an
|
||||
implementation reconstruct.
|
||||
|
||||
## §3 Implementation-level axioms (TCB — residual Go ↔ construction gaps)
|
||||
|
||||
| Axiom | Location | Closure plan |
|
||||
@@ -200,15 +271,24 @@ the submission-grade 10⁹-sample run is roadmap v0.8.0. So these axioms are
|
||||
## §4 Honest framing
|
||||
|
||||
Corona's EC theories refine the Go implementation against an in-house
|
||||
mechanization of the Boschini construction. The byte-equality theorem is
|
||||
honest *as an idealised statement* — but it models **reconstruct-then-
|
||||
sign**: the EC `CombineAbs` reconstructs the master secret and signs with
|
||||
it. That is intentionally NOT how the production threshold path runs; the
|
||||
production path's leak-freedom is established by code review + cross-runtime
|
||||
KAT, not by this EC proof. Five algebraic axioms (A1–A5) are Lean-bridged.
|
||||
The byte-walk obligations (C3/C4), the wrapper bridges (C5–C7), and the CT
|
||||
contracts (C9/C10) are the open surface, tracked in `BLOCKERS.md` and gated
|
||||
on the v0.8.0 Jasmin-extraction + dudect + external-audit roadmap.
|
||||
mechanization of the Boschini construction. There are now TWO models. The
|
||||
`corona_n1_byte_equality` theorem is honest *as an idealised CORRECTNESS
|
||||
statement* — but it models **reconstruct-then-sign**: the EC `CombineAbs`
|
||||
reconstructs the master secret and signs with it. That is intentionally NOT
|
||||
how the production threshold path runs. `Corona_N1_NoLeak.ec` adds the
|
||||
HONEST production model: the per-party masked responses telescope to
|
||||
`R·u + c·s` **without forming the master secret**, and the ONLY open
|
||||
assumption is a STANDARD Module-LWE/Module-SIS reduction (`no_leak_reduction`)
|
||||
— the same substrate §1 already lists — with the secret never reconstructed.
|
||||
The CORRECTNESS core of that model (`pairwise_mask_telescopes` +
|
||||
`secret_aggregate_no_reconstruct`) is **machine-checked in Lean on this
|
||||
host** (`Crypto.Corona.NoLeakAggregate`; `lake build` green). The
|
||||
production no-leak path's correctness is ALSO established by code review +
|
||||
cross-runtime KAT. Five algebraic axioms (A1–A5) are Lean-bridged-and-
|
||||
machine-checked. The byte-walk obligations (C3/C4), the wrapper bridges
|
||||
(C5–C7), the CT contracts (C9/C10), and the no-leak simulation
|
||||
(`no_leak_reduction`) are the open surface, tracked in `BLOCKERS.md` and
|
||||
gated on the v0.8.0 Jasmin-extraction + dudect + external-audit roadmap.
|
||||
|
||||
## §5 Comparison to Pulsar's AXIOM-INVENTORY
|
||||
|
||||
|
||||
+59
-31
@@ -14,43 +14,71 @@ fix they move to `## Closed` with commit + tag.
|
||||
|
||||
## Open
|
||||
|
||||
### CORONA-EC-RECON-MODEL (HIGH — proof-scope disclosure)
|
||||
### CORONA-EC-RECON-MODEL (HIGH — proof-scope disclosure; RE-SCOPED this pass)
|
||||
|
||||
**Status: OPEN. Disclosed, not closed.** The EasyCrypt Class N1
|
||||
byte-equality theorem (`corona_n1_byte_equality` /
|
||||
`corona_n1_byte_equality_extracted`) is machine-checked structurally
|
||||
(0 admits) but proved **relative to** the bucket-C asserted axioms in
|
||||
`AXIOM-INVENTORY.md` §C:
|
||||
**Status: OPEN, but RE-SCOPED — reconstruct-then-sign is no longer the
|
||||
load-bearing production residual.** Two distinct models now exist:
|
||||
|
||||
- `combine_body_spec` (the atomic Jasmin byte-walk) — the **Boschini
|
||||
combine steps 2–6 (open/aggregate/reject) are INSIDE this axiom,
|
||||
unproved.**
|
||||
**Model 1 — idealised correctness (reconstruct-then-sign).** The EC
|
||||
`corona_n1_byte_equality` / `_extracted` is machine-checked structurally (0
|
||||
admits) **relative to** the bucket-C-idealised axioms:
|
||||
- `combine_body_spec` (the atomic Jasmin byte-walk) — the Boschini combine
|
||||
steps 2–6 are INSIDE it, unproved.
|
||||
- `combine_abs_op_lifted_bridge` + `sign_abs_op_lifted_eq_rlwe` — the
|
||||
wrapper bridges that pin the lifted combine/sign op to
|
||||
`rlwe_sign_op (reconstruct quorum shares) …`, i.e. the centralised
|
||||
R-LWE signer applied to the **Lagrange-reconstructed master secret**.
|
||||
- `combine_body_axiom` / `S_functional_spec` — the section-local module
|
||||
contracts of the same identity.
|
||||
wrapper bridges pinning the lifted op to
|
||||
`rlwe_sign_op (reconstruct quorum shares) …`, i.e. the centralised R-LWE
|
||||
signer on the **Lagrange-reconstructed master secret**.
|
||||
- `combine_body_axiom` / `S_functional_spec` — the section-local contracts.
|
||||
|
||||
So the EC model **reconstructs the master key and signs with it**
|
||||
(reconstruct-then-sign). This is an idealised *correctness* statement; it
|
||||
is NOT a proof that the production threshold path is leak-free, and it is
|
||||
NOT how the production path is intended to run.
|
||||
So Model 1 **reconstructs the master key and signs with it** — an idealised
|
||||
*correctness* statement, intentionally NOT the production instantiation.
|
||||
|
||||
**Model 2 — the production no-leak residual (added this pass).**
|
||||
`proofs/easycrypt/Corona_N1_NoLeak.ec` states the production path the way it
|
||||
runs: the per-party masked responses
|
||||
`z_i = R_i·u + maskPrime_i + c·λ_i·s_i − mask_i` aggregate to `R·u + c·s`
|
||||
because the pairwise-PRF masks **telescope to zero** (`mask_telescope_zero`:
|
||||
`Σ_i maskPrime_i = Σ_i mask_i`, the same double sum reindexed) — so the
|
||||
master secret is **never formed** and no per-party `c·s_i` is ever in the
|
||||
clear (`no_leak_z_aggregate`). The ONLY open assumption is
|
||||
`no_leak_reduction`: under **Module-LWE + Module-SIS** the public transcript
|
||||
leaks nothing about `s` beyond one single-party Boschini signature. That is
|
||||
a STANDARD PQ assumption — the same substrate `AXIOM-INVENTORY.md` §1
|
||||
already lists — **not** an implementation reconstruct.
|
||||
|
||||
**What is machine-checked NOW (this host, `lake build` green, 0 sorry):**
|
||||
the CORRECTNESS core of Model 2 — `Crypto.Corona.NoLeakAggregate`
|
||||
(`pairwise_mask_telescopes`, `summed_response_is_mask_free`,
|
||||
`secret_aggregate_no_reconstruct`, `no_leak_under_standard_assumptions`) +
|
||||
`Crypto.Threshold_Lagrange`. The EC side of Model 2 is **written,
|
||||
machine-recheck pending EasyCrypt** (no `ec` on the authoring host;
|
||||
`scripts/checks/ec-compile.sh` is the CI gate).
|
||||
|
||||
Remaining OPEN:
|
||||
|
||||
- The production no-leak path's correctness is ALSO established by code
|
||||
review + cross-runtime KAT (Go↔C++); there is no independent R-LWE
|
||||
verifier (CORONA-NO-INDEP-VERIFIER — by design, no NIST target).
|
||||
- `no_leak_reduction`'s full simulation-soundness proof (the v0.8.0
|
||||
EC/paper artifact) is not written; disclosed as a Module-LWE/MSIS reduction.
|
||||
- Model 1's C-idealised cone closure is still the Jasmin byte-walk (v0.8.0)
|
||||
— but Model 1 is now explicitly *not* the safety-relevant residual.
|
||||
|
||||
**Resolution criteria:**
|
||||
- [ ] Jasmin combine/sign byte-walk lands (production target v0.8.0) ⇒
|
||||
`combine_body_spec` / `sign_body_spec` and the layout-frame axioms
|
||||
become lemmas against the Jasmin operational semantics.
|
||||
- [ ] Wrapper bridges (`combine_abs_op_lifted_bridge`,
|
||||
`sign_abs_op_lifted_eq_rlwe`, `combine_abs_op_lifted_bridge`)
|
||||
discharge to lemmas, OR are replaced by a faithful (non-reconstruct)
|
||||
model of the Boschini steps 2–6.
|
||||
- [ ] `combine_body_axiom` / `S_functional_spec` discharge to lemmas via
|
||||
the wrapper instantiation against the extracted modules.
|
||||
- [ ] **External cryptographic review** (shared gate with
|
||||
CORONA-CT-PENDING and CORONA-NO-INDEP-VERIFIER below) signs off that
|
||||
the reconstruct-then-sign EC model is an acceptable correctness
|
||||
idealisation given the separate code-review + KAT evidence.
|
||||
- [x] A separate (non-reconstruct) model of the PRODUCTION no-leak path is
|
||||
written, with its CORRECTNESS core machine-checked (Lean, this host)
|
||||
and its residual stated as a STANDARD Module-LWE/MSIS reduction
|
||||
(`Corona_N1_NoLeak.ec` + `Crypto.Corona.NoLeakAggregate`).
|
||||
- [ ] `Corona_N1_NoLeak.ec` passes `scripts/checks/ec-compile.sh` in CI
|
||||
(machine-recheck pending EasyCrypt; cannot run on the authoring host).
|
||||
- [ ] `no_leak_reduction` discharged to a full M-LWE/M-SIS simulation proof
|
||||
(v0.8.0), OR accepted by external review as a standard reduction.
|
||||
- [ ] Jasmin byte-walk lands ⇒ Model 1's C-idealised axioms become lemmas
|
||||
(correctness nicety).
|
||||
- [ ] **External cryptographic review** (shared gate with CORONA-CT-PENDING
|
||||
and CORONA-NO-INDEP-VERIFIER) signs off that (a) Model 2's
|
||||
standard-reduction residual is the correct production posture and (b)
|
||||
Model 1 is an acceptable correctness idealisation.
|
||||
|
||||
### CORONA-CT-PENDING (MEDIUM — constant-time evidence)
|
||||
|
||||
|
||||
+30
-11
@@ -20,17 +20,36 @@
|
||||
| **fail-closed-pending-review** | Implemented but gated to REFUSE until external review. |
|
||||
| **open-research** | Multi-month roadmap; not done. |
|
||||
|
||||
**Disclosure 1 — the EC byte-equality MODELS reconstruct-then-sign.**
|
||||
`corona_n1_byte_equality` / `corona_n1_byte_equality_extracted` prove the
|
||||
threshold combine equals `CombineAbs.combine`, whose body
|
||||
(`wrapper_combine_refines_abs`) reduces — via the bridge axioms
|
||||
`combine_abs_op_lifted_bridge` and `sign_abs_op_lifted_eq_rlwe` — to
|
||||
`rlwe_sign_op (reconstruct quorum shares) …`: the centralised R-LWE signer
|
||||
applied to the **Lagrange-reconstructed master secret**. The Boschini
|
||||
combine **steps 2–6** (open/aggregate/reject) are **opened inside
|
||||
`combine_body_spec`, not proved**. So the EC theorem is **machine-checked
|
||||
(0 admits) modulo a C-cone of asserted axioms that reconstruct-then-sign** —
|
||||
it is NOT a proof that the production threshold path is leak-free.
|
||||
**Disclosure 1 — TWO models; reconstruct-then-sign is the idealised one,
|
||||
NOT the production residual (RE-SCOPED this pass).**
|
||||
|
||||
*Model 1 (idealised correctness).* `corona_n1_byte_equality` /
|
||||
`_extracted` prove the threshold combine equals `CombineAbs.combine`, whose
|
||||
body reduces — via `combine_abs_op_lifted_bridge` and
|
||||
`sign_abs_op_lifted_eq_rlwe` — to `rlwe_sign_op (reconstruct quorum
|
||||
shares) …`: the centralised R-LWE signer applied to the
|
||||
**Lagrange-reconstructed master secret**. The Boschini combine steps 2–6 are
|
||||
opened inside `combine_body_spec`, not proved. So Model 1 is machine-checked
|
||||
(0 admits) modulo a C-cone that **reconstructs-then-signs** — an idealised
|
||||
*correctness* statement, NOT how production runs and NOT a leak-freeness
|
||||
proof.
|
||||
|
||||
*Model 2 (the HONEST production residual, `Corona_N1_NoLeak.ec`).* The
|
||||
production path's per-party masked responses
|
||||
`z_i = R_i·u + maskPrime_i + c·λ_i·s_i − mask_i` aggregate to `R·u + c·s`
|
||||
because the pairwise-PRF masks **telescope to zero** (`mask_telescope_zero`)
|
||||
— the master secret is **never formed** and no per-party `c·s_i` is ever
|
||||
exposed (`no_leak_z_aggregate`). The CORRECTNESS core of Model 2 is
|
||||
**machine-checked in Lean 4 + Mathlib on this host** (`lake build` green, 0
|
||||
sorry): `Crypto.Corona.NoLeakAggregate` (`pairwise_mask_telescopes`,
|
||||
`summed_response_is_mask_free`, `secret_aggregate_no_reconstruct`,
|
||||
`no_leak_under_standard_assumptions`) + `Crypto.Threshold_Lagrange`. The
|
||||
ONLY open assumption is `no_leak_reduction`: under **Module-LWE +
|
||||
Module-SIS** (the SAME substrate §ProofSubstrate / AXIOM-INVENTORY.md §1
|
||||
already lists) the public transcript leaks nothing about `s` beyond one
|
||||
single-party Boschini signature — a STANDARD PQ assumption, **not** an
|
||||
implementation reconstruct. Model 2's EC side is **written, machine-recheck
|
||||
pending EasyCrypt**; its Lean core is machine-checked now.
|
||||
|
||||
**Disclosure 2 — the no-leak property is NOT independently interop-tested.**
|
||||
Corona's KAT cross-validation is **Go↔C++ of the SAME construction**
|
||||
|
||||
@@ -0,0 +1,184 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Class N1 NO-LEAK telescoping-mask model *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* STATUS (honest): WRITTEN; machine-recheck PENDING EasyCrypt. *)
|
||||
(* No `easycrypt`/`why3`/`alt-ergo` on the build host this file was *)
|
||||
(* authored on; it has NOT been re-elaborated here. CI gate *)
|
||||
(* `scripts/checks/ec-compile.sh` (skipped locally when ec absent) is *)
|
||||
(* the authority. Do NOT relabel any lemma below "machine-checked" / *)
|
||||
(* "discharged" until ec-compile runs green. The ALGEBRAIC CORE this *)
|
||||
(* file rests on IS machine-checked, in Lean 4 + Mathlib, on this *)
|
||||
(* host: *)
|
||||
(* Crypto.Corona.NoLeak.{pairwise_mask_telescopes, *)
|
||||
(* summed_response_is_mask_free, secret_aggregate_no_reconstruct, *)
|
||||
(* no_leak_under_standard_assumptions} *)
|
||||
(* Crypto.Threshold.Lagrange.threshold_partial_response_identity *)
|
||||
(* (`lake build` exits 0, with no unproven-tactic placeholders). *)
|
||||
(* *)
|
||||
(* WHY THIS FILE EXISTS — de-misdirecting reconstruct-then-sign *)
|
||||
(* ----------------------------------------------------------------- *)
|
||||
(* Corona_N1.ec's `corona_n1_byte_equality` proves the threshold combine *)
|
||||
(* bit-equals `CombineAbs.combine`, whose wrapper bridge *)
|
||||
(* `sign_abs_op_lifted_eq_rlwe` pins it to *)
|
||||
(* *)
|
||||
(* rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd *)
|
||||
(* *)
|
||||
(* i.e. the centralised Boschini signer applied to the LAGRANGE- *)
|
||||
(* RECONSTRUCTED master secret (RECONSTRUCT-THEN-SIGN). The *)
|
||||
(* Boschini/Raccoon production combine must NEVER do that *)
|
||||
(* (BLOCKERS.md CORONA-EC-RECON-MODEL): reconstructing the secret, or *)
|
||||
(* broadcasting per-party `c*s_i` whose aggregate is `c*s`, breaks *)
|
||||
(* threshold secrecy and transcript simulation. *)
|
||||
(* *)
|
||||
(* This file states the CORRECT no-leak model: the per-party masked *)
|
||||
(* responses *)
|
||||
(* z_i = R_i*u + maskPrime_i + c*lambda_i*s_i - mask_i *)
|
||||
(* aggregate to `R*u + c*s` because the pairwise-PRF masks TELESCOPE TO *)
|
||||
(* ZERO (Sum_i maskPrime_i = Sum_i mask_i, the same double sum *)
|
||||
(* reindexed), so the master secret is NEVER formed and no per-party *)
|
||||
(* `c*s_i` is ever exposed in the clear. The residual OPEN content is *)
|
||||
(* then NOT "lifted op = central sign on the reconstructed secret" but a *)
|
||||
(* STANDARD-ASSUMPTION reduction (Module-LWE + Module-SIS, the SAME *)
|
||||
(* substrate Corona's AXIOM-INVENTORY.md §1 already discloses). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv Distr.
|
||||
require import Corona_N1.
|
||||
|
||||
(* ===================================================================
|
||||
PART 1 — the telescoping pairwise-mask cancellation (Corona no-leak core)
|
||||
|
||||
EC mirror of the MACHINE-CHECKED Lean theorem
|
||||
`Crypto.Corona.NoLeak.pairwise_mask_telescopes`: for a quorum T and a
|
||||
per-pair mask `p : party -> party -> M`,
|
||||
mask i = Sum_{j in T} p i j (party i's own seeds)
|
||||
maskPrime i = Sum_{j in T} p j i (others' seeds for i)
|
||||
the aggregate Sum_{i in T} (maskPrime i - mask i) = 0, because both are
|
||||
the SAME double sum Sum_{i,j} p i j reindexed by swapping (i,j)
|
||||
(Fubini / Finset.sum_comm). NO antisymmetry of p needed.
|
||||
|
||||
At the EC level we model the masks abstractly. `mask_telescope_zero`
|
||||
states the cancellation as the contract the production aggregator
|
||||
satisfies; its machine-checked content is the Lean theorem. (B/standard
|
||||
layer: a finite-sum reindexing fact, NOT a security conclusion.) *)
|
||||
|
||||
type party_mask_t. (* per-party mask in R_q^N *)
|
||||
|
||||
op mask_of : int list -> int -> party_mask_t. (* mask i over quorum *)
|
||||
op mask_prime_of : int list -> int -> party_mask_t. (* maskPrime i over quorum *)
|
||||
op sum_party_masks : int list -> (int -> party_mask_t) -> party_mask_t.
|
||||
op sub_mask : party_mask_t -> party_mask_t -> party_mask_t.
|
||||
op zero_mask : party_mask_t.
|
||||
|
||||
(* TELESCOPE CONTRACT (Lean-backed, B/standard):
|
||||
Sum_{i in Q} (maskPrime_i - mask_i) = 0. Machine-checked in Lean as
|
||||
`Crypto.Corona.NoLeak.pairwise_mask_telescopes`. Here the EC contract;
|
||||
references only the masks (no secret share). *)
|
||||
axiom mask_telescope_zero (Q : int list) :
|
||||
sum_party_masks Q (fun i => sub_mask (mask_prime_of Q i) (mask_of Q i))
|
||||
= zero_mask.
|
||||
|
||||
(* ===================================================================
|
||||
PART 2 — the no-leak z aggregate (master secret never reconstructed)
|
||||
|
||||
With the masks telescoped away, the surviving aggregate is
|
||||
`R*u + c * Sum_i lambda_i*s_i = R*u + c*s` by Lagrange-at-0, with the
|
||||
secret-sharing polynomial (the master `s`) never formed. The
|
||||
pre-existing Corona_N1 axiom `threshold_partial_response_identity`
|
||||
ALREADY states this no-leak z identity (the Lagrange aggregate of the
|
||||
per-party masked responses = `rlwe_compute_z` on the reconstructed
|
||||
share, the secret entering only as the public `z`'s `c*s` summand).
|
||||
|
||||
`no_leak_z_aggregate` re-exports it in no-leak vocabulary. EC mirror of
|
||||
the machine-checked Lean `Crypto.Corona.NoLeak.secret_aggregate_no_
|
||||
reconstruct` (the y=0 / mask-free specialization of the shared
|
||||
threshold identity). (A: Lean-bridged standard fact.) *)
|
||||
|
||||
lemma no_leak_z_aggregate
|
||||
(Q : int list) (shares : share_t list)
|
||||
(c : c_n1_t) (rho_rnd : randomness_t) (mu_val : mu_t) :
|
||||
uniq Q =>
|
||||
size shares = size Q =>
|
||||
poly_degree (reconstruct Q shares) < size Q =>
|
||||
shares = List.map (poly_eval (reconstruct Q shares)) Q =>
|
||||
lagrange_aggregate_responses Q
|
||||
(List.map (per_party_partial_response c rho_rnd mu_val) shares)
|
||||
= rlwe_compute_z (unpack_sk (reconstruct Q shares)) mu_val rho_rnd.
|
||||
proof.
|
||||
(* Exactly the Lean-bridged Corona_N1 axiom; re-stated here so the
|
||||
no-leak file is self-contained. Closes by `apply`. *)
|
||||
exact (threshold_partial_response_identity Q shares c rho_rnd mu_val).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
PART 3 — the residual cryptographic assumption (STANDARD: M-LWE/M-SIS)
|
||||
|
||||
PARTS 1+2 are CORRECTNESS: the no-leak combine computes the same
|
||||
(c, z, Delta) the central signer would, from telescoping-masked
|
||||
partials, with the master secret never formed. The remaining content
|
||||
is SECRECY: that the public Corona transcript reveals nothing about `s`
|
||||
beyond ONE single-party Boschini signature. We state it as an abstract
|
||||
simulation-soundness predicate reducing to Module-LWE + Module-SIS --
|
||||
the SAME substrate Corona's AXIOM-INVENTORY.md §1 already lists
|
||||
(Lyubashevsky-Peikert-Regev; Ajtai / Micciancio-Regev; Boschini
|
||||
2024/1113). This is the honest replacement for the reconstruct-then-
|
||||
sign `sign_abs_op_lifted_eq_rlwe` bridge: a standard-assumption
|
||||
reduction, NOT a reconstruct.
|
||||
|
||||
EC mirror of Lean `Crypto.Corona.NoLeak.NoLeakReduction`. *)
|
||||
|
||||
type public_transcript_t. (* per-party commitments, rounded h, z-sum, c *)
|
||||
type rlwe_leakage_t. (* one single-party Boschini sig's public footprint *)
|
||||
|
||||
op module_lwe_hard : bool. (* Gaussian-masked commitments pseudorandom *)
|
||||
op module_sis_hard : bool. (* extracting short s from the z-sum is R-SIS *)
|
||||
op transcript_simulator : rlwe_leakage_t -> public_transcript_t.
|
||||
|
||||
(* NO-LEAK REDUCTION (C / OPEN, but now a STANDARD-ASSUMPTION reduction).
|
||||
Under Module-LWE + Module-SIS, the public Corona threshold transcript
|
||||
is reproducible from a single Boschini signature's leakage alone --
|
||||
leaks nothing extra about `s`. The honest replacement for the
|
||||
reconstruct-then-sign bridge. DISCLOSED and OPEN: full simulation proof
|
||||
= v0.8.0 artifact. It does NOT reconstruct the secret; its content
|
||||
reduces to standard lattice hardness. *)
|
||||
axiom no_leak_reduction :
|
||||
module_lwe_hard =>
|
||||
module_sis_hard =>
|
||||
forall (leak : rlwe_leakage_t),
|
||||
exists (tr : public_transcript_t), tr = transcript_simulator leak.
|
||||
|
||||
lemma no_leak_under_standard_assumptions (leak : rlwe_leakage_t) :
|
||||
module_lwe_hard =>
|
||||
module_sis_hard =>
|
||||
exists (tr : public_transcript_t), tr = transcript_simulator leak.
|
||||
proof.
|
||||
move=> hlwe hsis.
|
||||
exact (no_leak_reduction hlwe hsis leak).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING (this file)
|
||||
|
||||
axioms (3) — all DISCLOSED in AXIOM-INVENTORY.md:
|
||||
- mask_telescope_zero (B / standard: EC contract of the MACHINE-
|
||||
CHECKED Lean pairwise_mask_telescopes;
|
||||
references only masks, no secret share)
|
||||
- no_leak_reduction (C / OPEN, STANDARD: the Module-LWE +
|
||||
Module-SIS simulation reduction -- the
|
||||
honest replacement for the reconstruct-
|
||||
then-sign sign_abs_op_lifted_eq_rlwe bridge)
|
||||
- module_lwe_hard / module_sis_hard are `op` declarations (booleans
|
||||
naming the standard assumptions), not axioms.
|
||||
|
||||
PROVED-MODULO-RECHECK lemmas (machine-recheck pending EasyCrypt):
|
||||
no_leak_z_aggregate (re-exports the Lean-bridged
|
||||
threshold_partial_response_identity)
|
||||
no_leak_under_standard_assumptions
|
||||
|
||||
The telescoping-mask + Lagrange-aggregate CORRECTNESS core is machine-
|
||||
checked in Lean on this host; the EC side is the procedure-level wrapper
|
||||
pending ec-compile. The ONLY genuinely-open assumption is
|
||||
`no_leak_reduction`, a Module-LWE/MSIS reduction -- a STANDARD PQ
|
||||
assumption (the same substrate §1 already discloses), not an
|
||||
implementation reconstruct.
|
||||
=================================================================== *)
|
||||
Reference in New Issue
Block a user