Paper 2022/484

VERICA - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering

Jan Richter-Brockmann
Jakob Feldtkeller
Pascal Sasdrich
Tim Güneysu
Abstract

Physical attacks, including passive Side-Channel Analysis and active Fault Injection Analysis, are considered among the most powerful threats against physical cryptographic implementations. These attacks are well known and research provides many specialized countermeasures to protect cryptographic implementations against them. Still, only a limited number of combined countermeasures, i.e., countermeasures that protect implementations against multiple attacks simultaneously, were proposed in the past. Due to increasing complexity and reciprocal effects, design of efficient and reliable combined countermeasures requires longstanding expertise in hardware design and security. With the help of formal security specifications and adversary models, automated verification can streamline development cycles, increase quality, and facilitate development of robust cryptographic implementations. In this work, we revise and refine formal security notions for combined protection mechanisms and specifically embed them in the context of hardware implementations. Based on this, we present the first automated verification framework that can verify physical security properties of hardware circuits with respect to combined physical attacks. To this end, we conduct several case studies to demonstrate the capabilities and advantages of our framework, analyzing secure building blocks (gadgets), S-boxes build from Toffoli gates, and the ParTI scheme. For the first time, we reveal security flaws in analyzed structures due to reciprocal effects, highlighting the importance of continuously integrating security verification into modern design and development cycles.

Note: Revised Table 2 after Siemen Dhooghe pointed us to a bug in the combined composability verifications for detection-based countermeasures. Thanks! The tool has been adapted as well.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
A minor revision of an IACR publication in TCHES 2022
Keywords
SCAFIAFormal VerificationBDDSymbolic SimulationCombined Analysis
Contact author(s)
jan richter-brockmann @ rub de
jakob feldtkeller @ rub de
pascal sasdrich @ rub de
tim gueneysu @ rub de
History
2023-07-07: revised
2022-04-23: received
See all versions
Short URL
https://ia.cr/2022/484
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2022/484,
      author = {Jan Richter-Brockmann and Jakob Feldtkeller and Pascal Sasdrich and Tim Güneysu},
      title = {{VERICA} - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering},
      howpublished = {Cryptology {ePrint} Archive, Paper 2022/484},
      year = {2022},
      url = {https://eprint.iacr.org/2022/484}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.