Paper 2025/185

AutoDiVer: Automatically Verifying Differential Characteristics and Learning Key Conditions

Marcel Nageler, Graz University of Technology
Shibam Ghosh, University of Haifa, French Institute for Research in Computer Science and Automation
Marlene Jüttler, Graz University of Technology
Maria Eichlseder, Graz University of Technology
Abstract

Differential cryptanalysis is one of the main methods of cryptanalysis and has been applied to a wide range of ciphers. While it is very successful, it also relies on certain assumptions that do not necessarily hold in practice. One of these is the hypothesis of stochastic equivalence, which states that the probability of a differential characteristic behaves similarly for all keys. Several works have demonstrated examples where this hypothesis is violated, impacting the attack complexity and sometimes even invalidating the investigated prior attacks. Nevertheless, the hypothesis is still typically taken for granted. In this work, we propose AutoDiVer, an automatic tool that allows to thoroughly verify differential characteristics. First, the tool supports calculating the expected probability of differential characteristics while considering the key schedule of the cipher. Second, the tool supports estimating the size of the space of keys for which the characteristic permits valid pairs, and deducing conditions for these keys. AutoDiVer implements a custom SAT modeling approach and takes advantage of a combination of features of advanced SAT solvers, including approximate model counting and clause learning. To show applicability to many different kinds of block ciphers like strongly aligned, weakly aligned, and ARX ciphers, we apply AutoDiVer to GIFT, PRESENT, RECTANGLE, SKINNY, WARP, SPECK, and SPEEDY.

Note: Added note about fixed typo in SKINNY characteristic.

Metadata
Available format(s)
PDF
Category
Attacks and cryptanalysis
Publication info
A minor revision of an IACR publication in TOSC 2025
DOI
10.46586/tosc.v2025.i1.471-514
Keywords
Differential cryptanalysisHypothesis of stochastic equivalenceToolSAT solver
Contact author(s)
marcel nageler @ tugraz at
shibam ghosh @ inria fr
marlene juettler @ student tugraz at
maria eichlseder @ tugraz at
History
2025-03-12: revised
2025-02-08: received
See all versions
Short URL
https://ia.cr/2025/185
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2025/185,
      author = {Marcel Nageler and Shibam Ghosh and Marlene Jüttler and Maria Eichlseder},
      title = {{AutoDiVer}: Automatically Verifying Differential Characteristics and Learning Key Conditions},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/185},
      year = {2025},
      doi = {10.46586/tosc.v2025.i1.471-514},
      url = {https://eprint.iacr.org/2025/185}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.