Main result for long keys: if , every satisfies (5) (corrected: not in the paper; fills the regime its proof omits)
ProvedNoSignalPA.secure_of_long_keycryptographynonlocalityp2o-correctedp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1privacy-amplificationquantum-information
Assume . Then every function is secure: for every choice of Eve's sets , every -partite nonsignaling box , every input of Bob and every input of Eve,
This statement is not in the paper. The paper proves the main result through Lemma 2, whose proof needs ; that constraint holds only when . This milestone covers the remaining key lengths, so that the main result holds for all as stated.
Differences from the source:
- correction: the proof of the main result via Lemma 2 for all Nr, Ns ('the chosen value for β satisfies the required constraint', p.5) → a separate statement for Nr + 2 ≤ Ns + √Nr, where every h is secure; reason: the constraint fails for long keys: at Nr = 144, Ns = 160 Lemma 2 is false for every h (see lemma_2), so the paper's proof does not reach these key lengths, while the main result still holds there
- reading: (Nr + 2)-partite nonsignaling distribution P_{a,b,e|x,y,z} → IsNonsignaling: for each of Alice's Nr systems, Bob (one system) and Eve, summing out that party's output leaves a quantity independent of that party's input; reason: pp. 1–2 define no signaling as 'the marginals only depend on their corresponding observables', with Bob's systems as one; the single-party conditions imply those for every subset of parties
- generalization: Eve's input z and output e, with Σ_e and max_z (no alphabets fixed) → Z and E arbitrary types in a universe u, P x y z a PMF on (a, b, e), max_z as ⨆ and Σ_e as tsum in ℝ≥0∞; reason: every finite alphabet is such a type and then ⨆ is the maximum and tsum the finite sum; the security predicate quantifies over more boxes, so it specializes to the paper's
- reading: P_{k,e|x=0,z}, P_{e|z} and P_{a,b|x,y} (inputs of other parties not shown) → key and Eve marginals read at x = 0 and any Bob input y; P_{a,b|x,y} read at any Eve input z₀; IsSecure quantifies over y and z₀; reason: under no signaling these marginals do not depend on the omitted inputs; quantifying over them is the stronger reading
Preamble
import Mathlib import Definitions.Def_NoSignalPA_IsSecure
Formal statement
namespace NoSignalPA
/-- **(Not in the paper.) For `Nr + 2 ≤ Ns + √Nr` every hash function is secure.**
Added for Ll. Masanes, *Universally-composable privacy amplification from causality constraints*,
arXiv:0807.2158v4, Main result, eq. (5), p. 2 (PDF p. 2). The paper's proof goes through Lemma 2, whose
proof needs `|β 5^M 8^{−Nr}| ≤ 1` (p. 5); "the chosen value for β satisfies the required
constraint" holds only when `Ns + √Nr ≤ Nr + 2`. This milestone covers the remaining key lengths.
If `Nr + 2 ≤ Ns + √Nr`, then every `h : {0,1}^{Nr} → {0,1}^{Ns}` satisfies the bound (5) for every
`(Nr + 2)`-partite nonsignaling box: `IsSecure h`.
**Formalization Note.** Together with `lemma_2` and `secure_of_entrywise` this yields the main
result for all `Nr, Ns`; the two regimes share the boundary `Ns + √Nr = Nr + 2`. -/
theorem secure_of_long_key.{u} {Nr Ns : ℕ} (hN : (Nr : ℝ) + 2 ≤ Ns + Real.sqrt Nr)
(h : Str Nr → Str Ns) : IsSecure.{u} h := by sorry
end NoSignalPA
Source
Masanes, Universally-composable privacy amplification from causality constraints, arXiv:0807.2158v4, Main result, eq. (5), p.2, for the regime excluded by the constraint of eq. (14), p.5 (not stated in the paper)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.