International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

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

Authors:
Jan Richter-Brockmann , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Jakob Feldtkeller , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Pascal Sasdrich , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Tim Güneysu , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany; DFKI, Bremen, Germany
Download:
DOI: 10.46586/tches.v2022.i4.255-284
URL: https://tches.iacr.org/index.php/TCHES/article/view/9820
Search ePrint
Search Google
Presentation: Slides
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.
BibTeX
@article{tches-2022-32363,
  title={VERICA - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering},
  journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
  publisher={Ruhr-Universität Bochum},
  volume={2022, Issue 4},
  pages={255-284},
  url={https://tches.iacr.org/index.php/TCHES/article/view/9820},
  doi={10.46586/tches.v2022.i4.255-284},
  author={Jan Richter-Brockmann and Jakob Feldtkeller and Pascal Sasdrich and Tim Güneysu},
  year=2022
}