International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

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

Authors:
Ling Su , Key Laboratory of Cryptologic Technology and Information Security, Ministry of Education, Shandong University, Jinan, China; School of Cyber Science and Technology, Shandong University, Qingdao, China
Wei Wang , Key Laboratory of Cryptologic Technology and Information Security, Ministry of Education, Shandong University, Jinan, China; School of Cyber Science and Technology, Shandong University, Qingdao, China
Meiqin Wang , Key Laboratory of Cryptologic Technology and Information Security, Ministry of Education, Shandong University, Jinan, China; School of Cyber Science and Technology, Shandong University, Qingdao, China
Download:
DOI: 10.46586/tosc.v2021.i1.269-315
URL: https://tosc.iacr.org/index.php/ToSC/article/view/8840
Search ePrint
Search Google
Abstract: 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 260.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.
Video from TOSC 2021
BibTeX
@article{tosc-2021-30952,
  title={Accelerating the Search of Differential and Linear Characteristics with the SAT Method},
  journal={IACR Transactions on Symmetric Cryptology},
  publisher={Ruhr-Universität Bochum},
  volume={2021, Issue 1},
  pages={269-315},
  url={https://tosc.iacr.org/index.php/ToSC/article/view/8840},
  doi={10.46586/tosc.v2021.i1.269-315},
  author={Ling Su and Wei Wang and Meiqin Wang},
  year=2021
}