×

zbMATH — the first resource for mathematics

Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. (English) Zbl 07199588
Summary: In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. In the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Then, we describe the Transalg software tool developed based on these principles with SAT-based cryptanalysis specifics in mind. We demonstrate the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We compare the functional capabilities of the proposed tool with that of other domain-specific software tools which can be used to reduce cryptanalysis problems to SAT, and also with the CBMC system widely employed in symbolic verification. The paper also presents vast experimental data, obtained using the SAT solvers that took first places at the SAT competitions in the recent several years.

MSC:
03B70 Logic in computer science
68 Computer science
PDF BibTeX XML Cite
Full Text: Link arXiv
References:
[1] Parosh Aziz Abdulla, Per Bjesse, and Niklas E´en. Symbolic reachability analysis based on SAT-solvers. InTools and Algorithms for the Construction and Analysis of Systems (TACAS),
[2] Gilles Audemard and Laurent Simon. Glucose and Syrup in the SAT’17. In Tom´as Balyo, Marijn J. H. Heule, and Matti J¨arvisalo, editors,SAT Competition 2017, volume B-2017-1, pages 16-17, 2017.
[3] Gregory V. Bard.Algebraic Cryptanalysis. Springer Publishing Company, Incorporated, 1st edition, 2009. · Zbl 1183.94019
[4] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. InProc. of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 1579 ofLecture Notes in Computer
[5] Charles Bouillaguet, Patrick Derbez, and Pierre-Alain Fouque. Automatic search of attacks on round-reduced AES and applications. InProc. of Advances in Cryptology (CRYPTO), volume 6841 ofLecture Notes in Computer Science, pages 169-187, 2011. · Zbl 1287.94056
[6] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors.Handbook of Satisfiability, volume 185 ofFrontiers in Artificial Intelligence and Applications. IOS Press, 2009. · Zbl 1183.68568
[7] Armin Biere. The AIGER And-Inverter Graph (AIG) format version 20071012. Technical Report 07/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2007.
[8] Armin Biere. Yet another local search solver and lingeling and friends entering the SAT Competition 2014. In Anton Belov, Daniel Diepold, Marijn Heule, and Matti J¨arvisalo, editors,
[9] Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2017. In Tom´as Balyo, Marijn J. H. Heule, and Matti J¨arvisalo, editors,SAT Competition
[10] Christian Bessiere, George Katsirelos, Nina Narodytska, and Toby Walsh. Circuit complexity and decompositions of global constraints. InProc. of the 21st International Joint Conference · Zbl 1248.68457
[11] J. Bruer. On pseudo-random sequences as crypto generators. InProc. of the Int. Zurich Seminar on Digital Comm., volume 46, pages 157-161, 1984.
[12] Robert King Brayton, Alberto L. Sangiovanni-Vincentelli, Curtis T. McMullen, and Gary D. Hachtel.Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Norwell, MA, USA, 1984. · Zbl 0565.94020
[13] Vadim Bulavintsev, Alexander Semenov, Oleg Zaikin, and Stepan Kochemazov. A bitslice implementation of Anderson’s attack on A5/1.Open Engineering, 8(1):7-16, 2018.
[14] Christophe De Canni‘ere. Trivium: A stream cipher construction inspired by block cipher design principles. InProc. of the 9th International Conference on Information Security (ISC), volume · Zbl 1156.94345
[15] Nicolas T. Courtois and Gregory V. Bard. Algebraic cryptanalysis of the data encryption standard. InProc. of Cryptography and Coding, volume 4887 ofLecture Notes in Computer · Zbl 1154.94386
[16] Nicolas T. Courtois, Jerzy A. Gawinecki, and Guangyan Song. Contradiction immunity and guess-then-determine attacks on GOST.Tatra Mountains Mathematical Publications, 53(1):2-13, · Zbl 1308.94066
[17] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 ofLecture Notes in Computer Science, pages 168-176, 2004. · Zbl 1126.68470
[18] Stephen A. Cook and David G. Mitchell. Finding hard instances of the satisfiability problem: A survey. InDIMACS Series in Discr. Math. and Theoretical Comp. Sci., volume 35, pages 1-17. American Mathematical Society, 1997. · Zbl 0889.68073
[19] Stephen A. Cook. The complexity of theorem-proving procedures. InProc. of the 3rd Annual ACM Symposium on Theory of Computing, pages 151-158, 1971. · Zbl 0253.68020
[20] Nicolas T. Courtois. Low-complexity key recovery attacks on GOST block cipher.Cryptologia, 37(1):1-10, 2013.
[21] Nicolas T. Courtois. Algebraic complexity reduction and cryptanalysis of GOST. Cryptology ePrint Archive, Report 2011/626, 2011-2015.http://eprint.iacr.org/2011/626.
[22] Ivan Damg˚ard. A design principle for hash functions. InProc. of Advances in Cryptology (CRYPTO), volume 435 ofLecture Notes in Computer Science, pages 416-427, 1989.
[23] William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae.J. Log. Program., 1(3):267-284, 1984. · Zbl 0593.68062
[24] Debapratim De, Abishek Kumarasubramanian, and Ramarathnam Venkatesan. Inversion attacks on secure hash functions using SAT solvers. InProc. of Theory and Applications of · Zbl 1214.68350
[25] Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. · Zbl 0217.54002
[26] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InProc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 ofLecture Notes in Computer Science, pages 337-340, 2008.
[27] Hans Dobbertin. The first two rounds of MD4 are not one-way. InProc. of Fast Software Encryption (FSE), volume 1372 ofLecture Notes in Computer Science, pages 284-292. Springer, 1998. · Zbl 1385.94030
[28] Martin Davis and Hilary Putnam. A computing procedure for quantification theory.J. ACM, 7(3):201-215, 1960. · Zbl 0212.34203
[29] Bruno Dutertre. Yices 2.2. InProc. of Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 737-744, 2014.
[30] Levent Erk¨ok, Magnus Carlsson, and Adam Wick. Hardware/software co-verification of cryptographic algorithms using Cryptol. InProc. of 9th International Conference on Formal Methods
[31] Levent Erk¨ok and John Matthews. Pragmatic equivalence and safety checking in Cryptol. In Proc. of the 3rd Workshop on Programming Languages Meets Program Verification (PLPV),
[32] Tobias Eibach, Enrico Pilz, and Gunnar V¨olkel. Attacking Bivium using SAT solvers. InTheory and Applications of Satisfiability Testing (SAT), volume 4996 ofLecture Notes in Computer Science, pages 63-76, 2008. · Zbl 1138.68536
[33] Niklas E´en and Niklas S¨orensson. Temporal induction by incremental SAT solving.Electr. Notes Theor. Comput. Sci., 89(4):543-560, 2003. · Zbl 1271.68215
[34] Niklas E´en and Niklas S¨orensson. An extensible SAT-solver. InProc. of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 2919 ofLecture
[35] Tobias Eibach, Gunnar V¨olkel, and Enrico Pilz. Optimising Gr¨obner bases on Bivium.Mathematics in Computer Science, 3(2):159-172, Apr 2010. · Zbl 1205.94081
[36] Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon. painless-maplecomsps. In Tom´as Balyo, Marijn J. H. Heule, and Matti J¨arvisalo, editors,SAT Competition 2017, · Zbl 06807229
[37] P. Geffe. How to protect data with ciphers that are really hard to break.Electronics, 46(1):99- 101, 1973.
[38] Michael R. Garey and David S. Johnson.Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York, NY, USA, 1979. · Zbl 0411.68039
[39] Martin Gebser, Benjamin Kaufmann, Andr´e Neumann, and Torsten Schaub. clasp: A conflictdriven answer set solver. InProc. of Logic Programming and Nonmonotonic Reasoning, volume
[40] Fred Glover and Manuel Laguna.Tabu Search. Kluwer Academic Publishers, Norwell, MA, USA, 1997. · Zbl 0930.90083
[41] Oded Goldreich.Computational Complexity: A Conceptual Perspective. Cambridge University Press, New York, NY, USA, 1 edition, 2008. · Zbl 1154.68056
[42] Irina Gribanova and Alexander Semenov. Using automatic generation of relaxation constraints to improve the preimage attack on 39-step MD4. InProc. of the 41st International Convention
[43] Martin Hell, Thomas Johansson, and Willi Meier. Grain: a stream cipher for constrained environments.Int. J. Wire. Mob. Comput., 2(1):86-93, May 2007.
[44] Antti E. J. Hyv¨arinen.Grid Based Propositional Satisfiability Solving. PhD thesis, Aalto University, 2011.
[45] Alexey Ignatiev. mkplot: a Python script to create cactus and scatter plots based on matplotlib. URL: https://github.com/alexeyignatiev/mkplot.
[46] Alexey Ignatiev, Antonio Morgado, and Jo˜ao P. Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. InProc. of Theory and Applications of Satisfiability Testing · Zbl 06916321
[47] Predrag Janicic. URSA: a system for uniform reduction to SAT.Logical Methods in Computer Science, 8(3):1-39, 2012. · Zbl 1248.68456
[48] Matti J¨arvisalo, Armin Biere, and Marijn Heule. Simulating circuit-level simplifications on CNF.J. Autom. Reasoning, 49(4):583-619, 2012. · Zbl 1267.94144
[49] Dejan Jovanovic and Predrag Janicic. Logical analysis of hash functions. InProc. of the 5th International Workshop on Frontiers of Combining Systems (FroCoS), volume 3717 ofLecture Notes in Computer Science, pages 200-215, 2005. · Zbl 1171.94351
[50] Matti J¨arvisalo and Tommi Junttila. Limitations of restricted branching in clause learning. Constraints, 14(3):325-356, Sep 2009. · Zbl 1192.68643
[51] James C. King. Symbolic execution and program testing.Commun. ACM, 19(7):385-394, July 1976. · Zbl 0329.68018
[52] Daniel Kroening. Software verification. In Biere et al. [BHvMW09], pages 505-532. · Zbl 1381.68143
[53] Ga¨etan Leurent. MD4 is not one-way. InProc. of Fast Software Encryption (FSE), volume 5086 ofLecture Notes in Computer Science, pages 412-428, 2008.
[54] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. InProc. of Theory and Applications of Satisfiability Testing · Zbl 06623509
[55] J. R. Lewis and B. Martin. Cryptol: high assurance, retargetable crypto development and validation. InIEEE Military Communications Conference, 2003. MILCOM 2003., volume 2,
[56] Fr´ed´eric Lafitte, Olivier Markowitch, and Dirk Van Heule. SAT based analysis of LTE stream cipher ZUC.Journal of Information Security and Applications, 22:54 - 65, 2015. Special Issue on Security of Information and Networks.
[57] Filip Mari´c. Formalization and implementation of modern SAT solvers.J. Autom. Reason., 43(1):81-119, 2009. · Zbl 1187.68557
[58] Fabio Massacci. Using Walk-SAT and Rel-SAT for cryptographic key search. InProc. of the 16th International Joint Conference on Artifical Intelligence (IJCAI), pages 290-295. Morgan
[59] Irkutsk Supercomputer Center of SB RAS. URL:http://hpc.icc.ru.
[60] Cameron Mcdonald, Chris Charnes, and Josef Pieprzyk. Attacking Bivium with MiniSat. Technical Report 2007/040, ECRYPT Stream Cipher Project, 2007.
[61] Ralph C. Merkle. A certified digital signature. InProc. of Advances in Cryptology (CRYPTO), volume 435 ofLecture Notes in Computer Science, pages 218-238, 1989.
[62] Fabio Massacci and Laura Marraro. Logical cryptanalysis as a SAT problem.J. Autom. Reasoning, 24(1/2):165-203, 2000. · Zbl 0968.68052
[63] Willi Meier and Othmar Staffelbach. Analysis of pseudo random sequences generated by cellular automata. InProc. of Advances in Cryptology (EUROCRYPT), volume 547 ofLecture Notes in · Zbl 0791.68121
[64] Jo˜ao P. Marques-Silva and Karem A. Sakallah. GRASP: a search algorithm for propositional satisfiability.IEEE Trans. Computers, 48(5):506-521, 1999. · Zbl 1392.68388
[65] Jo˜ao P. Marques-Silva. Practical applications of Boolean satisfiability. InProc. of the 9th International Workshop on Discrete Event Systems, pages 74-80, 2008.
[66] Jo˜ao P. Marques-Silva, Inˆes Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Biere et al. [BHvMW09], pages 131-153.
[67] Jo˜ao P. Marques-Silva and Karem A. Sakallah. GRASP: a new search algorithm for satisfiability. InProc. of the 1996 IEEE/ACM International Conference on Computer-aided Design (ICCAD), pages 220-227, 1996.
[68] N Metropolis and S Ulam. The Monte Carlo method.J. Amer. statistical assoc., 44(247):335-341, 1949. · Zbl 0033.28807
[69] Alfred J. Menezes, Scott A. Vanstone, and Paul C. Van Oorschot.Handbook of Applied Cryptography. CRC Press, Inc., Boca Raton, FL, USA, 1st edition, 1996. · Zbl 0868.94001
[70] Ilya Mironov and Lintao Zhang. Applications of SAT solvers to cryptanalysis of hash functions. InProc. of Theory and Applications of Satisfiability Testing (SAT), volume 4121 ofLecture · Zbl 1187.94028
[71] Karsten Nohl. Attacking phone privacy. InProc. of BlackHat 2010 Lecture Notes, Las-Vegas, USA, pages 1-6, 2010.
[72] Vegard Nossum. SAT-based preimage attacks on SHA-1. Master’s thesis, University of Oslo, Department of Informatics, 2012.
[73] Alexander Nadel and Vadim Ryvchin. Chronological backtracking. InProc. Theory and Applications of Satisfiability Testing (SAT), volume 10929 ofLecture Notes in Computer Science, · Zbl 1442.68219
[74] Ilya Otpuschennikov, Irina Gribanova, and Alexander Semenov. Transalg repository, URL: https://gitlab.com/transalg/transalg.
[75] Ilya Otpuschennikov, Irina Gribanova, Oleg Zaikin, and Alexander Semenov. The repository of SAT encodings for various cryptographic primitives constructed by Transalg, URL: https://gitlab.com/satencodings/satencodings.
[76] Chanseok Oh. COMiniSatPS Pulsar and GHackCOMSPS. In Tom´as Balyo, Marijn J. H. Heule, and Matti J¨arvisalo, editors,SAT Competition 2017, volume B-2017-1, pages 12-13, 2017.
[77] Ilya Otpuschennikov and Alexander Semenov. Technology for translating combinatorial problems into boolean equations.Prikl. Diskr. Mat., 1(11):96-115, 2011.
[78] Mukul R. Prasad, Armin Biere, and Aarti Gupta. A survey of recent advances in SAT-based formal verification.International Journal on Software Tools for Technology Transfer, 7(2):156-
[79] Artem Pavlenko, Maxim Buzdalov, and Vladimir Ulyantsev. Fitness comparison by statistical testing in construction of SAT-based guess-and-determine cryptographic attacks. InProc. of
[80] Artem Pavlenko, Alexander Semenov, and Vladimir Ulyantsev. Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis. InProc. of the 22nd
[81] Mikhail Posypkin, Alexander Semenov, and Oleg Zaikin. Using BOINC desktop grid to solve large scale SAT problems.Computer Science, 13(1):25, 2012.
[82] Thomas Siegenthaler. Correlation-immunity of nonlinear combining functions for cryptographic applications.IEEE Trans. Information Theory, 30(5):776-780, 1984. · Zbl 0554.94010
[83] Marc Stevens, Pierre Karpman, and Thomas Peyrin. Freestart collision for full SHA-1. InProc. of Advances in Cryptology (EUROCRYPT), volume 9665 ofLecture Notes in Computer Science, · Zbl 1385.94073
[84] Carsten Sinz, Florian Merz, and Stephan Falke. LLBMC: A bounded model checker for LLVM’s intermediate representation. InProc. of Tools and Algorithms for the Construction and Analysis
[85] Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. InProc. of Theory and Applications of Satisfiability Testing (SAT), volume 5584 of
[86] Mate Soos. Grain of Salt - an automated way to test stream ciphers through SAT solvers. In Proc. of Workshop on Tools for Cryptanalysis (Tools), pages 131-144, 2010.
[87] Marc Stevens. Single-block collision attack on MD5.IACR Cryptology ePrint Archive, 2012:40, 2012.
[88] Ko Stoffelen. Optimizing S-box implementations for several criteria using SAT solvers. In Proc. of the 23rd International Conference on Fast Software Encryption (FSE), volume 9783 of Lecture Notes in Computer Science, pages 140-160. Springer Berlin Heidelberg, 2016. · Zbl 1387.94100
[89] Yu Sasaki, Lei Wang, Kazuo Ohta, and Noboru Kunihiro. New message difference for MD4. In Proc. of Fast Software Encryption (FSE), volume 4593 ofLecture Notes in Computer Science, · Zbl 1186.94469
[90] Alexander Semenov and Oleg Zaikin. Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem. InProc. of the 13th International Conference on
[91] Alexander Semenov and Oleg Zaikin. Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions.
[92] Alexander Semenov, Oleg Zaikin, Dmitry Bespalov, and Mikhail Posypkin. Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system. InProc. of the 11th International · Zbl 1335.94078
[93] Grigori S Tseitin. On the complexity of derivation in propositional calculus.Studies in constructive mathematics and mathematical logic, part II, Seminars in mathematics, pages 115-125, 1970.
[94] John von Neumann. The general and logical theory of automata. In L. A. Jeffress, editor, Cerebral Mechanisms in Behavior - The Hixon Symposium, pages 1-31. John Wiley & Sons,
[95] Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. InProc. of the 18th International Joint Conference on Artificial Intelligence (IJCAI), pages
[96] Stephen Wolfram. Random sequence generation by cellular automata.Advances in Applied Mathematics, 7(2):123 - 169, 1986. · Zbl 0603.68053
[97] Xiaoyun Wang and Hongbo Yu. How to break MD5 and other hash functions. InProc. of Advances in Cryptology (EUROCRYPT), volume 3494 ofLecture Notes in Computer Science, · Zbl 1137.94359
[98] Yang Xu, Guanfeng Wu, Qingshan Chen, and Shuwei Chen. Maple LCM Scavel and Maple LCM Scavel 200. In Marijn Heule, Matti J¨arvisalo, and Martin Suda, editors,Proc. of
[99] Takeru Yasumoto and Takumi Okuwaga. Rokk 1.0.1. In Anton Belov, Daniel Diepold, Marijn Heule, and Matti J¨arvisalo, editors,SAT Competition 2014, page 70, 2014.
[100] Oleg Zaikin and Stepan Kochemazov. An improved SAT-based guess-and-determine attack on the alternating step generator. InProc. of the 20th Information Security Conference (ISC), · Zbl 06916320
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.