Analysis of the LTE Security Algorithm ZUC with SAT Solver

Long Term Evolution (LTE) the 4th generation (4G) mobile broadband radio network is designed with special attention given to security. In order to secure the communication over the air radio network of LTE, three confidentiality and integrity cryptographic algorithms are approved by 3rd Generation Partnership Project (3GPP). ZUC, which is one of the algorithms is the third alternative to LTE. ZUC is designed using inherited properties from SNOW3G cryptographic algorithm with some improvements. However, it has been found that related keys, which are result of weak key state exists in its predecessor. Moreover, from the view point of Security Algorithms Group of Experts (SAGE) advancement in cryptanalysis may have effect on both ZUC and its predecessor, due to their design similarity, and SNOW3G weak key property. This thesis analyzed the latest version of ZUC; the analysis is to check the existence of weak key state in ZUC at the end of initialization of Linear Feedback Shift Register (LFSR) with key and initialization vector (IV). The analysis is done by Boolean satisfiability problem solver (SAT solver) program, emerging logical cryptographic algorithms analysis technique. For the analysis the key initialization procedure equations of the algorithm are converted to SAT instance, which is special input format for SAT solvers in Conjunctive Normal Form (CNF), and are fed to SAT Solver. The result showed that the latest version of ZUC LFSR after the initialization is not initialized with same value that indicates there is no weak key state problem in the key generation procedure of ZUC algorithm. Keywords: ZUC, weak key, Satisfiability, SAT solver, Logical cryptanalysis