Using SAT Solvers to Finding Short Cycles in Cryptographic Algorithms

• Autorzy: Dudzic Władysław , Kanciak Krzysztof

Identyfikatory

DOI

10.24425/ijet.2020.131897

• Języki publikacji: EN

Abstrakty

EN

A desirable property of iterated cryptographic algorithms, such as stream ciphers or pseudo-random generators, is the lack of short cycles. Many of the previously mentioned algorithms are based on the use of linear feedback shift registers (LFSR) and nonlinear feedback shift registers (NLFSR) and their combination. It is currently known how to construct LFSR to generate a bit sequence with a maximum period, but there is no such knowledge in the case of NLFSR. The latter would be useful in cryptography application (to have a few taps and relatively low algebraic degree). In this article, we propose a simple method based on the generation of algebraic equations to describe iterated cryptographic algorithms and find their solutions using an SAT solver to exclude short cycles in algorithms such as stream ciphers or nonlinear feedback shift register (NLFSR). Thanks to the use of AIG graphs, it is also possible to fully automate our algorithm, and the results of its operation are comparable to the results obtained by manual generation of equations. We present also the results of experiments in which we successfully found short cycles in the NLFSRs used in Grain-80, Grain-128 and Grain-128a stream ciphers and also in stream ciphers Bivium and Trivium (without constants used in the initialization step).

Słowa kluczowe

EN

NLFSR; short cycles; stream ciphers; trivium; bivium; Grain-80; Grain-128

• Wydawca: Polish Academy of Sciences, Committee of Electronics and Telecommunication
• Czasopismo: International Journal of Electronics and Telecommunications
• Rocznik: 2020
• Tom: Vol. 66, No. 3
• Strony: 443--448
• Opis fizyczny: Bibliogr. 22 poz., rys., tab., wykr.

Twórcy

autor

Dudzic Władysław

• Military University of Technology, Warsaw, Poland

autor

Kanciak Krzysztof

• Military University of Technology, Warsaw, Poland

Bibliografia

• [1] A. Biere, "CADICAL, LINGELING, PLINGELING, TREENGELING and YALSAT Entering the SAT Competition 2017".
• [2] A. Biere, "The AIGER And-Inverter Graph (AIG) Format", 2007.
• [3] A. Maximov, M. Hell, T. Johansson and W. Meier, "A Stream Cipher Proposal: Grain-128", IEEE International Symposium on Information Theory, 2006, doi: 10.1109/ISIT.2006.261549.
• [4] C. De Canniere and B. Preneel, "Trivium Specifications", Springer Berlin Heidelberg, pages 244-266, 2008, doi: 10.1007/978-3-540-68351-3_18.
• [5] E. Dubrova and M. Teslenko, "An efficient SAT-based algorithm for finding short cycles in cryptographic algorithms", Proceedings of the Third Annual ACM Symposium on Theory of Computing, 2018, doi: 10.1109/HST.2018.8383892.
• [6] E. Dubrova and M. Teslenko, "On Finding Short Cycles in Cryptographic Algorithms", Cryptology ePrint Archive, Report 2016/1068, 2016.
• [7] E. Homsirikamol, P. Morawiecki, M. Rogawski and M. Srebrny, "Security Margin Evaluation of SHA-3 Contest Finalists through SAT-Based Attacks", Computer Information Systems and Industrial Management, pages 56–67, 2012, doi: 10.1007/978-3-642-33260-9_4.
• [8] J. Borghoff, L. R. Knudsen and M. Stolpe, "Bivium as a Mixed-Integer Linear Programming Problem", Lecture Notes in Computer Science (LNCS), Vol. 5921, pp 133-152, 2009, doi: 10.1007/978-3-642-10868-6_9.
• [9] K. Carter, A. Foltzer, J. Hendrix, B. Huffman, A. Tomb, "SAW: the software analysis workbench", Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, pages 15-18, 2013, doi: 10.1145/2527269.2527277.
• [10] M. Ågren, M. Hell, T. Johansson and W. Meier, "Grain-128a: a new version of Grain-128 with optional authentication", International Journal of Wireless and Mobile Computing, 2011, doi: 10.1504/IJWMC.2011.044106.
• [11] M. Davis and H. Putnam, "A Computing Procedere for Quantification Theory", Journal of the ACM, 1960, doi: 10.1145/321033.321034.
• [12] M. Davis, G. Logemann, D. Loveland, "A Machine Program for Theorem Proving", Communications of the ACM, 1962, doi: 10.1145/368273.368557.
• [13] M. Hell, T. Johansson and W. Meier, "Grain: a stream cipher for constrained environments", International Journal of Wireless and Mobile Computing, 2007, doi: 10.1504/IJWMC.2007.013798.
• [14] N. T. Courtois and G. V. Bard, "Algebraic cryptanalysis of the data encryption standard", Springer Berlin Heidelberg, pages 152–169, 2007, doi: 10.1007/978-3-540-77272-9_10.
• [15] T. Rachwalik, J. Szmidt, R. Wicik and J. Zabłocki, "Generation of Nonlinear Feedback Shift Registers with Special-Purpose Hardware", 2012 Military Communications and Information Systems Conference, MCC 2012, 2012.
• [16] S. Babbage, J. Borghoff and V. Velichkov, "The eSTREAM Portfolio in 2012", ICT-2007-216676. ECRYPT II, 2012.
• [17] S. Cook, "The complexity of theorem proving procedures", Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971, doi: 10.1145/800157.805047.
• [18] S. Hassoun and S. Tsutomu, "Logic Synthesis and Verification", Kluwer Academic Publishers, 2002, doi: 10.1007/978-1-4615-0817-5.
• [19] S. W. Golomb, "Shift Register Sequences", Aegean Park Press, 1981, doi: 10.5555/578271.
• [20] P. Augustynowicz and K. Kanciak, "Scalable Method of Searching for Full-period Nonlinear Feedback Shift Registers with GPGPU. New List of Maximum Period NLFSRs" International Journal of Electronics and Telecommunications, 2018, doi: 10.24425/119365.
• [21] P. Dąbrowski, G. Łabuzek, T. Rachwalik and J. Szmidt "Searching for Nonlinear Feedback Shift Registers with Parallel Computing", Information Processing Letters, 2013, 10.1016/j.ipl.2013.12.002.
• [22] R. Brayton, A. Mishchenko, "ABC: An Academic Industrial-Strength Verification Tool", Springer Berlin Heidelberg, pages 24-40, 2010, doi: 10.1007/978-3-642-14295-6_5.

Uwagi

This work was presented at the International Scientific Conference Mathematical Cryptology & Cybersecurity (MC&C 2020), Warsaw, 16-17.01.2020.

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).