From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

Computer Science > Cryptography and Security [Submitted on 20 Apr 2026] From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification Ray Iskander, Khaled Kirah 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. Comments: 15 pages, 1 figure Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2604.18717 [cs.CR]   (or arXiv:2604.18717v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2604.18717 Focus to learn more Submission history From: Khaled Kirah Dr [view email] [v1] Mon, 20 Apr 2026 18:17:22 UTC (446 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-04 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)