ARX (Addition

Rotation

Xor) algorithms are based on three operations:modular addition

exclusive-OR and bitwise rotation

which execute very fast in both software and hardware. Impossible differential cryptanalysis and zero-correlation linear cryptanalysis are among the most powerful attacks for ARX ciphers. The key problem for the attacks is searching more and longer impossible differentials and zero-correlation linear approximations. Although there are many automatic search algorithms

these approaches do not fully utilize the non-linear component properties

which cannot reach their potential. A SAT (Satisfiability) -based model to automatic search for impossible differentials and zero-correlation linear approximations in ARX is proposed.By exploiting behaviors of every component

especially the differential and linear propagation properties through general modular addition and key modular addition operations

we generate computable and easily implementable constraints and establish the SAT-based model. As applications

we apply our model to Chaskey

SPECK and HIGHT. For Chaskey

we are able to find 13 4-round impossible differentials and 1 4-round zero-correlation linear approximation for the first time. For SPECK

we first find 10 6-round zero-correlation linear approximations of SPECK32 and 15 6-round zero-correlation linear approximations of SPECK48. Besides

we find 4 17-round impossible differentials and zero-correlation linear approximations of HIGHT in a few minutes. Compared with the existing results

both the number and the search time of distinguishers are significantly improved. In addition

by repackaging the output interface of the STP solver

we establish the automated SAT\\SMT model

which can give the upper bound of rounds of impossible differentials and zero-correlation linear approximations under special input and output differential and mask sets for ARX algorithm.