SAT based analysis of LTE stream cipher ZUC

Mobile security is of paramount importance. The security of LTE (long term evolution of radio networks), which is currently widely deployed as a long-term standard for mobile networks, relies upon three cryptographic primitives, among which the stream cipher ZUC. In this paper, we point out that the linear feedback shift register (LFSR) used in ZUC has about 2²⁵ encodings of the zero state (i.e. all LFSR variables are 0) due to the fact that operations are performed modulo 2³¹ - 1 on 32-bit operands. We use SAT solvers to show that these states are reachable when 64 bits of ZUC's initial state can be chosen (i.e. R₁, R₂). That is, for each key there are many initial vectors that lead to a weak state after ZUC's initialization. We also use SAT-solvers to disprove the existence of such weak inputs when the initial values of R₁, R₂ are set to zero as required by the official specifications. Finally, we discuss how the redundancy introduced in ZUC's output function might help mounting SAT-solver based guess-and-determine attacks given a few keystream digits.