Paper 2026/050 Original: eprint.iacr.org/2026/050 ↗

Low-Latency Low-Randomness First-Order OPINI Gadgets and Their Formal Verification

Abstract

Masking is an essential countermeasure against side-channel attacks, yet implementing secure and low-latency hardware masking remains challenging. In particular, although OPINI provides strong composability guarantees for single-cycle iterative architectures, the prior low-latency OPINI gadget, HPC4, is limited to two-input multiplication. In this work, we present a low-latency, low-randomness, first-order OPINI gadget applicable to arbitrary Boolean functions, denoted as $\rm GOM$. Independent and concurrent work by Rahimi and Moradi proposes OTSM, which is also a generic, low-latency first-order OPINI gadget. Our construction involves two new techniques: (i)~extending the HPC4 idea---originally masking each share of one secret input with two bits of randomness---to masking each monomial derived from the input shares accordingly, and (ii)~a randomness-reassignment technique that enables the two circuits generating the output shares to reuse the same set of randomness while preserving the first-order OPINI security. To validate OPINI security, we propose a formal verification technique based on three symbolic reduction rules, and use it to verify multiple low-latency OPINI gadgets (i.e., HPC4, $\rm GOM$ and $\rm OTSM$). Leveraging the generality of our gadget, we instantiate several OPINI-secure S-boxes across different algebraic degrees. For the algebraic-degree-2 Ascon S-box, our gadget achieves a 21\% reduction in area and a 28\% reduction in randomness compared to the HPC4-based implementation. We further construct higher-degree S-boxes from the PRESENT, PRINCE and AES ciphers, report their hardware performance, and provide a comparison with the concurrent work $\rm OTSM$. The first-order OPINI security of all masked S-boxes is successfully verified within 20~minutes using our formal verification method. Finally, FPGA-based experiments confirm the practical security of the masked implementations.