Analysis of the LTE Security Algorithm ZUC with SAT Solver

Abstract

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

ÖZ: Dördüncü nesil mobil geniş bant radyo ağı olan Uzun Vadeli Dönüşüm (LTE), özellikle güvenlik konusu dikkate alınarak tasarlanmıştır. LTE’nin hava radyo ağı üzerinden iletişim sağlamak üzere üç şifreleme algoritması 3. Nesil Ortaklık Projesi (3GPP) tarafından onaylanmıştır. Bu algoritmalardan biri olan ZUC, LTE’nin üçüncü alternatifidir. ZUC, SNOW3G şifreleme algoritmasından bazı özellikleri alarak, ilgili özelliklerin geliştirilmesiyle tasarlanmıştır. Ancak, ilgili anahtarlarla ilgili olarak, öncülü olan SNOW3G’de zayıf anahtar durumunun mevcut olduğu görülmüştür. Buna ek olarak, Güvenlik Algoritmaları Grubu Uzmanları’nın (SAGE) bakış açısına göre kripto analizi alanındaki iyileştirmelerin ZUC ve öncülü üzerinde etkili olabilir. Bunun nedeni ise tasarım benzerlikleri ve SNOW3G zayıf anahtar özellikleridir. Bu çalışma, ZUC’un son sürümünü analiz etmeyi amaçlamıştır. Analiz, anahtar ve başlatma vektörü (IV) ile doğrusal geribesleme öteleme kaydının (LFSR) başlatılmasının sonunda, zayıf anahtar durumunu denetlemek amacıyla yapılmıştır. Şifreleme algoritmalarının analizinde yükselmekte olan bir yöntem olarak Boolean sağlanabilirlik problem çözücü (SAT çözücü) programı kullanılmıştır. Algoritmanın anahtar başlatma prosedürü denklemleri, Bağlaçlı Normal Biçim’de (CNF) SAT çözücüleri için özel bir girdi biçimi olan SAT örneklerine dönüştürülmüştür ve ardından SAT Çözücüsü’ne yerleştirilmiştir. Sonuçlara göre, ZUC LFSR’nin son sürümünün aynı değerlerle başlatılmadığı ortaya çıkmış ve ZUC algoritmasında zayıf anahtar durumunun mevcut olmadığı anlaşılmıştır. Anahtar Sözcükler: ZUC, zayıf anahtar, Sağlanabilirlik, SAT çözücü, Mantıksal kripto analizi.