Paper 2018/1031

Sharing Independence & Relabeling: Efficient Formal Verification of Higher-Order Masking

Roderick Bloem, Rinat Iusupov, Martin Krenn, and Stefan Mangard


The efficient verification of the security of masked hardware implementations is an important issue that hinders the development and deployment of randomness-efficient masking techniques. At EUROCRYPT 2018, Bloem et al. [6] introduced the first practical formal tool to prove the side-channel resilience of masked circuits in the probing model with glitches. Most recently Barthe et al.[2] introduced a more efficient formal tool that builds upon the findings of Bloem et al. for modeling the effects of glitches. While Barthe et al.'s approach greatly improves the first-order verification performance, it shows that higher-order verification in the probing model with glitches is still enormously time-consuming for larger circuits like a second-order AES S-box, for instance. Furthermore, the results of Barthe et al. underline the discrepancy between state-of-the-art formal security notions that allow for faster verification of circuits. Namely the strong non-interference (SNI) notion, and existing masked hardware implementations that are secure in the probing model with glitches. In this work, we extend and improve the formal approaches of Bloem et al. and Barthe et al. on manifold levels. We first introduce a so-called sharing independence notion which helps to reason about the independence of shared variables. We then show how to use this notion to test for the independence of input and output sharings of a module which allows speeding up the formal verification of circuits that do not fulfill the SNI notion. With this extension, we are for the time able to verify the security of a second-order masked DOM AES S-box which takes about 3 seconds, and up to a fifth-order AES S-box which requires about 47 days for verification. Furthermore, we discuss in which case the independence of input and output sharings lead to composability.

Available format(s)
Publication info
Preprint. MINOR revision.
maskingformal verificationdomain-oriented maskinghardware securityside-channel analysisprivate circuits
Contact author(s)
hannes gross @ iaik tugraz at
2018-12-17: revised
2018-10-30: received
See all versions
Short URL
Creative Commons Attribution


      author = {Roderick Bloem and Rinat Iusupov and Martin Krenn and Stefan Mangard},
      title = {Sharing Independence & Relabeling: Efficient Formal Verification of Higher-Order Masking},
      howpublished = {Cryptology ePrint Archive, Paper 2018/1031},
      year = {2018},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.