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. SAT solvers allow us to show that these states are reachable when 64 bits of ZUC's initial state can be chosen (i.e. R₁,R₂) in reduced round versions of ZUC's initialization. We also use SAT-solvers to disprove the existence of such weak inputs in full round versions or in reduced round versions in which the initial values of R₁,R₂ are set to zero, as required by the official specifications. Finally, we discuss to what extent the redundancy introduced in ZUC's output function helps mounting SAT-solver based guess-and-determine attacks given a few keystream digits.