SAT-Based Automatic Searching for Differential and Linear Trails: Applying to CRAX

Boolean satisfiability problem (SAT) is now widely applied in differential cryptanalysis and linear cryptanalysis for various cipher algorithms. It generated many excellent results for some ciphers, for example, Salsa20. In this research, we study the differential and linear propagations through the operations of addition, rotation and XOR (ARX), and construct the SAT models. We apply the models to CRAX to search differential trails and linear trails automatically. In this sense, our contribution can be broadly divided into two parts. We give the bounds for differential and linear cryptanalysis of Alzette both up to 12 steps, by which we present a 3-round differential attack and a 3-round linear attack for CRAX. We construct a 4-round key-recovery attack for CRAX with time complexity 2^89 times of 4-round encryption and data complexity 2^25 .