mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
c177bda8f7
Tier A formalization paper for the Lux ML-KEM-768 stack:
- Encaps/Decaps correctness theorem (Section 3) via FO-K
recovery + CPAPKE decrypt-of-encrypt inverse.
- IND-CCA2 reduction with explicit advantage bound (Section 4)
composing HHK17 FO-K and Bos et al. CRYSTALS-Kyber MLWE/MLWR.
- FIPS 203 wire-format byte-equality (Section 5) via the
circl_fips203_compliant_* axiom block + KAT vectors.
- Constant-time (Section 6) with Decaps as the CT-critical
routine; implicit-rejection branch indistinguishability.
- Integration use cases (Section 7): X-Wing hybrid, Pulsar
identity-stage envelope binding, Quasar handshake.
- Machine-checked-proof traceability table.
PDF: 10 pages, compiled by pdflatex 2025.
Closes the Pulsar CR-8 audit gate (KEM-wrapped DKG / reshare
envelopes) at the level of the Tier A artifact pack.