Welcome to the resource topic for 2022/1641
Title:
AlgSAT — a SAT Method for Search and Verification of Differential Characteristics from Algebraic Perspective
Authors: Huina Li, Guozhen Liu, Haochen Zhang, Kai Hu, Jian Guo, Weidong Qiu
Abstract: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 differential1, due to some complicated contradictions that are hard to be considered. In this paper, we present a novel and handy method to search and verify a differential characteristic (DC) based on a recently proposed algebraic perspective on the differential(-linear) cryptanalysis (CRYPTO 2021).
From this algebraic perspective, exact Boolean expressions of differentials over a cryptographic primitive can be conveniently established, thus verifying a given DC is naturally a Boolean satisfiability problem (SAT problem). With this observation, our approach simulates the round function of the target cipher symbolically and derives a set of Boolean equations in Algebraic Normal Form (ANF). These Boolean equations can be solved by off-the-shelf SAT solvers such as Bosphorus, which accept ANFs as their input.
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 DC compared with the previous MILP model (CRYPTO 2020). Our approach takes about one minute to find a valid 8-round DC, while the previous MILP model could not find any such DCs in practical time. Based on this DC, a practical semi-free-start collision attack on the intermediate 8-round Gimli-Hash is thus successfully mounted, i.e., a colliding message pair is found. For Ascon, we check several DCs reported at FSE 2021. Firstly, we verify a 2-round DC used in the collision attack on Ascon-Hash by giving a right pair (such a right pair requires 2^{156} attempts to find in a random search). Secondly, a 4-round differential used in the forgery attack on Ascon-128’s iteration phase is proven invalid, as a result, the corresponding forgery attack is invalid, too. For Xoodoo, we verify tens of thousands of 3-round DCs and two 4-round DCs extended from the so-called differential trail cores found by the designers or our search tool. We find all of these DCs are valid, which well demonstrates the sound independence of the differential propagation over Xoodoo’s round functions. Besides, as an independent interest, we develop a SAT-based automatic search toolkit called XoodooSat to search for 2-, 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.
ePrint: https://eprint.iacr.org/2022/1641
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .