Paper 2026/050

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

, School of Cyber Science and Technology, Shandong University, Qingdao, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, 266237, China

Yanhong Fan, School of Cyber Science and Technology, Shandong University, Qingdao, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, 266237, China

Guowei Liu, School of Cyber Science and Technology, Shandong University, Qingdao, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, 266237, China

Chaoran Wang, School of Cyber Science and Technology, Shandong University, Qingdao, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, 266237, China

Meiqin Wang, School of Cyber Science and Technology, Shandong University, Qingdao, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, 266237, China

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, prior low-latency OPINI gadget, $\rm 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 $\rm HPC4$ idea--originally masking each share of one secret input with two bits of randomness--to masking each shared 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 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., $\rm 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 $\rm HPC4$-based implementation. We further construct higher-degree S-boxes from the PRESENT, PRINCE and AES ciphers and report their hardware performance as reference baselines. We also provide an apples-to-apples comparison with $\rm OTSM$. All masked S-boxes are successfully verified within 20~minutes using our formal verification method. Finally, FPGA-based experiments confirm the practical security of the masked implementations.

@misc{cryptoeprint:2026/050,
      author = {Lixuan Wu and Yanhong Fan and Guowei Liu and Chaoran Wang and Meiqin Wang},
      title = {Low-Latency Low-Randomness {OPINI} Gadgets and Their Formal Verification},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/050},
      year = {2026},
      url = {https://eprint.iacr.org/2026/050}
}