Paper 2022/1641

AlgSAT --- a SAT Method for Search and Verification of Differential Characteristics from Algebraic Perspective

Huina Li, Shanghai Jiao Tong University, Nanyang Technological University
Haochen Zhang, Shanghai Jiao Tong University
Guozhen Liu, Nanyang Technological University
Kai Hu, Nanyang Technological University
Jian Guo, Nanyang Technological University
Weidong Qiu

A good differential is a start for a successful differential attack. However, a differential might be invalid, i.e., there is no right pair following the differential, due to some contradictions in the conditions imposed by the differential. This paper presents a novel and handy method for searching and verifying differential trails from an algebraic perspective. From this algebraic perspective, exact Boolean expressions of differentials over a cryptographic primitive can be conveniently established, which allows for the convenient verification of a given differential trail. This verification process can be naturally formulated as a Boolean satisfiability problem (SAT). To demonstrate the power of our new tool, we apply it to Gimli, Ascon, and Xoodoo. For Gimli, we improve the efficiency of searching for a valid 8-round colliding differential trail compared to the previous MILP model (CRYPTO 2020). Based on this differential trail, a practical semi-free-start collision attack on the intermediate 8-round Gimli-Hash is thus successfully mounted. For Ascon, we check several differential trails reported at FSE 2021. Specifically, we find that a 4-round differential used in the forgery attack on Ascon-128’s iteration phase has been proven invalid. As a consequence, the corresponding forgery attack is also invalid. For Xoodoo, as an independent interest, we develop a SAT-based automatic search toolkit called XoodooSat to search for 3- and 4-round differential trail cores of Xoodoo. Our toolkit finds two more 3-round differential trail cores of weight 48 that were missed by the designers which enhance the security analysis of Xoodoo. Then, we verify tens of thousands of 3-round differential trails and two 4-round differential trails extended from the so-called differential trail cores. We find that all these differential trails are valid, which effectively demonstrates that there are no contradictions in the conditions imposed by the round differentials of the DTs in the trail core.

Available format(s)
Attacks and cryptanalysis
Publication info
Cryptographic PermutationSATAutomatic VerificationDifferential Characteristic SearchSemi-free-start Collision
Contact author(s)
lihuina @ sjtu edu cn
zhaohaochen @ sjtu edu cn
guozhen liu @ ntu edu sg
kai hu @ ntu edu sg
guojian @ ntu edu sg
qiuwd @ sjtu edu cn
2023-03-13: revised
2022-11-25: received
See all versions
Short URL
Creative Commons Attribution


      author = {Huina Li and Haochen Zhang and Guozhen Liu and Kai Hu and Jian Guo and Weidong Qiu},
      title = {AlgSAT --- a SAT Method for Search and  Verification of Differential Characteristics from Algebraic Perspective},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1641},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.