Search papers, labs, and topics across Lattice.
This paper presents a machine-checked, universal proof in Lean 4 of a key theorem related to the soundness of structural dependency analysis for verifying masking in post-quantum cryptographic (PQC) hardware. The proof demonstrates that value-independence implies identical marginal distributions for any modulus q > 0, addressing a critical gap in prior work that relied on finite enumeration. By establishing commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the appropriate abstraction, the work simplifies and strengthens the formal verification of masked PQC implementations.
Forget enumerating billions of cases: a five-line Lean proof now universally validates a core theorem for formally verifying masked post-quantum crypto hardware.
Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator [3, 4], but its core soundness result (Theorem 3.9.1) was machine-checked only at $q = 5$ via $2^{25}$ Boolean wire functions. This left portability to ML-KEM ($q = 3{,}329$, FIPS 203 [5]) and ML-DSA ($q = 8{,}380{,}417$, FIPS 204 [6]) as an open gap. NIST IR 8547 [7] (March 2025) motivates closing such gaps. We present the first machine-checked universal proof of the $r$-free sub-theorem of Theorem 3.9.1: for every $q>0$, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. The proof, in Lean 4 [8] with Mathlib [9], requires five lines versus $2^{25}$ finite evaluations. It is sorry-free, reducing the trusted base from \{Z3 [10], CVC5 [11], Python\} to the Lean 4 kernel. We provide nine theorems (T1--T6, T1', T3') covering reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all $q \geq 2$. The results establish commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the natural abstraction layer for arithmetic masking verification.
