mirror of https://github.com/luxfi/crypto.git synced 2026-10-30 16:59:13 +00:00

Files

T

zeekay 810a3bb501 mlkem/jasmin: keygen + encaps + decaps wrappers around libjade

Lux Jasmin wrappers around libjade's verified ML-KEM-768 kernel:

  lib/mlkem_params.jinc      - Lux-side parameter constants
                               + X-Wing hybrid sizes
                               + Pulsar envelope wire-format constants
  keygen.jazz                - lux_mlkem768_keygen
  encaps.jazz                - lux_mlkem768_encaps + lux_xwing_encaps
  decaps.jazz                - lux_mlkem768_decaps + lux_xwing_decaps

libjade's mlkem768 is functional-spec verified against FIPS 203
(Barbosa et al. Eurocrypt 2021) and -checkCT verified against
BGL (Almeida-Barbosa et al. IEEE S&P 2020).

Lux wrapper exists to give a single Lux-side entrypoint matching
the Go ABI in mlkem.go and to host the X-Wing hybrid combine.

Pending: pin libjade commit in fetch.sh + jasminc -checkCT pass
(GATE-4 in CRYPTOGRAPHER-SIGN-OFF.md).

2026-05-19 08:41:52 -07:00

2.7 KiB

Raw Permalink Blame History

Lux ML-KEM-768 -- Jasmin high-assurance track

This directory holds the Jasmin sources for the Lux ML-KEM-768 high-assurance implementation track. The Lux Jasmin entrypoints are thin wrappers around libjade's already-verified ML-KEM-768 kernel.

File layout

File	Purpose
`lib/mlkem_params.jinc`	Lux-side parameter constants.
`keygen.jazz`	ML-KEM-768 keygen wrapper.
`encaps.jazz`	ML-KEM-768 + X-Wing encaps wrappers.
`decaps.jazz`	ML-KEM-768 + X-Wing decaps wrappers.

libjade integration

The single-party ML-KEM-768 kernel is fetched from libjade (https://github.com/formosa-crypto/libjade) at a pinned commit. The libjade tree is not committed to this repository; the fetch is explicit and reproducible:

cd jasmin
./fetch.sh                 # clones libjade at the pinned commit

(Per the same protocol as ~/work/lux/pulsar/jasmin/ml-dsa-65/.)

The libjade ML-KEM-768 kernel is:

Functional-spec verified against FIPS 203 (Barbosa et al., Eurocrypt 2021).
Constant-time verified against the BGL leakage model (Almeida-Barbosa et al., IEEE S&P 2020).

Why a wrapper?

The Lux ML-KEM-768 Tier A track is intentionally narrow: we do not re-implement what libjade already verifies. Instead, the wrapper gives the artifact pack:

A single visible Lux-side entrypoint matching the Go ABI in ~/work/lux/crypto/mlkem/mlkem.go.
A canonical citation surface for the Pulsar identity-stage sealEnvelope (which is the same lux_mlkem768_encaps plus an HKDF + AEAD wrapping layer) and the Quasar handshake.
A drop-in slot for the X-Wing hybrid (which combines ML-KEM-768 with X25519 per draft-connolly-cfrg-xwing-kem).

How to build

./fetch.sh                              # one-time libjade fetch
jasminc -checkCT keygen.jazz            # CT check
jasminc -checkCT encaps.jazz            # CT check
jasminc -checkCT decaps.jazz            # CT check

Each invocation should succeed with no constant-time violations reported.

Citations

Almeida, Barbosa, Barthe, Blot, Gregoire, Laporte, Oliveira, Pacheco, Schwabe, Strub, "The last mile: High-assurance and high-speed cryptographic implementations", IEEE S&P 2020.
Barbosa, Barthe, Doczkal, Don, Fehr, Gregoire, Huang, Hulsing, Lee, Wu, "Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium", CRYPTO 2023.
Hofheinz, Hovelmanns, Kiltz, "A Modular Analysis of the Fujisaki-Okamoto Transformation", TCC 2017.
Bos et al., "CRYSTALS-Kyber: A CCA-secure module-lattice-based KEM", EuroS&P 2018.
Connolly, Schwabe, Westerbaan, "X-Wing: The Hybrid KEM You've Been Looking For", draft-connolly-cfrg-xwing-kem.

2.7 KiB Raw Permalink Blame History