4 papers
Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
Ray Iskander, Khaled Kirah
Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation. Existing composition frameworks (ISW, t-SNI, PINI, DOM) address Boole…
Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware
Ray Iskander, Khaled Kirah
Post-quantum cryptographic (PQC) accelerators for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) rely on pipelined Number Theoretic Transform (NTT) stages over . Our prior w…
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…
Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators
Ray Iskander, Khaled Kirah
Post-quantum cryptographic (PQC) accelerators implementing ML-KEM (FIPS 203) and ML-DSA (FIPS 204) require side-channel resistance evidence for FIPS 140-3 certification. However, e…