Paper 2021/213

Accelerating the Search of Differential and Linear Characteristics with the SAT Method

Ling Sun, Wei Wang, and Meiqin Wang


The introduction of the automatic search boosts the cryptanalysis of symmetric-key primitives to some degree. However, the performance of the automatic search is not always satisfactory for the search of long trails or ciphers with large state sizes. Compared with the extensive attention on the enhancement for the search with the mixed integer linear programming (MILP) method, few works care for the acceleration of the automatic search with the Boolean satisfiability problem (SAT) or satisfiability modulo theories (SMT) method. This paper intends to fill this vacancy. Firstly, with the additional encoding variables of the sequential counter circuit for the original objective function in the standard SAT method, we put forward a new encoding method to convert the Matsui's bounding conditions into Boolean formulas. This approach does not rely on new auxiliary variables and significantly reduces the consumption of clauses for integrating multiple bounding conditions into one SAT problem. Then, we evaluate the accelerating effect of the novel encoding method under different sets of bounding conditions. With the observations and experience in the tests, a strategy on how to create the sets of bounding conditions that probably achieve extraordinary advances is proposed. The new idea is applied to search for optimal differential and linear characteristics for multiple ciphers. For PRESENT, GIFT-64, RECTANGLE, LBlock, TWINE, and some versions in SIMON and SPECK families of block ciphers, we obtain the complete bounds (full rounds) on the number of active S-boxes, the differential probability, as well as the linear bias. The acceleration method is also employed to speed up the search of related-key differential trails for GIFT-64. Based on the newly identified 18-round distinguisher with probability $2^{-58}$, we launch a 26-round key-recovery attack with $2^{60.96}$ chosen plaintexts. To our knowledge, this is the longest attack on GIFT-64. Lastly, we note that the attack result is far from threatening the security of GIFT-64 since the designers recommended users to double the number of rounds under the related-key attack setting.

Available format(s)
Secret-key cryptography
Publication info
Published elsewhere. IACR-ToSC 2021 (Issue 1)
Automatic searchSAT methodDifferential cryptanalysisLinear cryptanalysisMatsui’s bounding condition
Contact author(s)
lingsun @ sdu edu cn
weiwangsdu @ sdu edu cn
mqwang @ sdu edu cn
2021-03-02: received
Short URL
Creative Commons Attribution


      author = {Ling Sun and Wei Wang and Meiqin Wang},
      title = {Accelerating the Search of Differential and Linear Characteristics with the SAT Method},
      howpublished = {Cryptology ePrint Archive, Paper 2021/213},
      year = {2021},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.