Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、M