Robust but Relaxed Probing Model

Abstract

Masking has become a widely applied and heavily researched method to protect cryptographic implementations against Side-Channel Analysis (SCA) attacks. The success of masking is primarily attributed to its strong theoretical foundation enabling it to formally prove security by modeling physical properties through socalled probing models. Specifically, the robust d-probing model enables us to prove the security for arbitrarily masked hardware circuits, manually or with the assistance of automated tools, even when considering the imperfect nature of physical hardware, including the occurrence of physical defaults such as glitches. However, the generic strategy employed by the robust d-probing model comes with a downside: It tends to over-conservatively model the information leakage caused by glitches meaning that the robust d-probing model considers glitches that can never occur in practice. This implies that in theory, an adversary could gain more information than she would obtain in practice. From a designer’s perspective, this entails that (1) securely designed hardware circuits may need to be withdrawn due to potential insecurity under the robust d-probing model and (2) designs that satisfy the security requirements of the robust d-probing model may incur unnecessary overhead, such as increased circuit size or latency.
In this work, we refine the formal treatment of glitches within the robust d-probing model to address glitches more accurately within a formal adversary model. Unlike the robust d-probing model, our approach considers glitches based on the operations performed and the data processed, ensuring that only manifesting glitches are accounted for. As a result, we introduce the Robust but Relaxed (RR) d-probing model, a formal adversary model maintaining the same level of security as the robust d-probing model but without the overly conservative treatment of glitches. Leveraging our new model, we prove the security of LUT-based Masked Dual-Rail with Pre-charge Logic (LMDPL) gadgets, a class of physically secure gadgets reported as insecure based on the robust d-probing model. We provide manual proofs and automated security evaluations employing an updated version of PROLEAD capable of verifying the security of masked circuits under our new model.