ProverNG: Efficient Verification of Compositional Masking for Cryptosystem’s Side-Channel Security

Formal verification of masking schemes has seen notable progress in recent years. However, existing tools often involve a trade-off between accuracy and performance: some are fast but may yield incorrect results, while others ensure soundness but incur high computational costs. In this paper, we present ProverNG, a formal verification tool for Non-Interference-based (NI-based) security notions under both standard and glitch-extended probing models, which are in-depth formalized models to assessing the threat caused by ubiquitous information leakage. Built upon SILVER, ProverNG retains its rigorous correctness guarantees while offering competitive efficiency. To achieve this, we introduce two main techniques. First, we propose a variable reduction rule that simplifies the simulatability check, a critical component of the verification process. Second, we develop a heuristic strategy that improves the enumeration of simulation sets, allowing ProverNG to identify valid simulation sets more effectively. Our experiments show that while ProverNG does not outperform all existing tools in terms of speed, it consistently delivers sound results with solid efficiency.