Problems of search for collisions of cryptographic hash functions of the MD family as variants of Boolean satisfiability problem
Authors
-
I.A. Bogachkova
-
O.S. Zaikin
-
S.E. Kochemazov
-
I.V. Otpushchennikov
-
A.A. Semenov
-
O.O. Khamisov
Keywords:
cryptographic hash functions
collisions
differential attacks
Boolean satisfiability problem
SAT
CDCL (Conflict-Driven Clause Learning)
parallel SAT solvers
Abstract
An implementation of the differential attacks on cryptographic hash functions MD4 (Message Digest 4) and MD5 (Message Digest 5) by reducing the problems of search for collisions of these hash functions to the Boolean satisfiability problem (SAT) is considered. The novelty of the results obtained consists in a more compact (compared to already known) SAT encodings for the algorithms considered and in the use of modern parallel and distributed SAT solvers in applications to the formulated SAT problems. Searching for single block collisions of MD4 in this approach turned out to be very simple. In addition, several dozens of double block collisions of MD5 are found. In the process of the corresponding numerical experiments, a certain class of messages that produce the collisions is found: in particular, a set of pairs of such messages with first 10 zero bytes is constructed.
Section
Section 1. Numerical methods and applications
References
- R. L. Rivest, “The MD4 Message Digest Algorithm,” in Lecture Notes in Computer Science (Springer, Heidelberg, 1991), Vol. 537, pp. 303-311.
- R. L. Rivest, “The MD5 Message-Digest Algorithm,” Request for Comments (RFC): 1321.
http://www.rfc-base.org/txt/rfc-1321.txt . Cited January 15, 2015.
- X. Wang, X. Lai, D. Feng, et al., “Cryptanalysis of the Hash Functions MD4 and RIPEMD,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2005), Vol. 3494, pp. 1-18.
- X. Wang and H. Yu, “How to Break MD5 and Other Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2005), Vol. 3494, pp. 19-35.
- V. Klima, “Finding MD5 Collisions on a Notebook PC Using Multimessage Modifications,” Cryptology ePrint Archive. Report 2005/102. 2005.
http://eprint.iacr.org/2005/102 . Cited January 15, 2015.
- C. de Canniere and C. Rechberger, “Finding SHA-1 Characteristics: General Results and Applications,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2006), Vol. 4284, pp. 1-20.
- C. de Canniere, F. Mendel, and C. Rechberger, “Collisions for 70-Step SHA-1: On the Full Cost of Collision Search,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2007), Vol. 4876, pp. 56-73.
- E. A. Grechnikov and A. V. Adinets, “Finding a Collision for the 75-Round SHA-1 Hash Function Using Clusters of GPUs,” Vychisl. Metody Programm. 13 (2), 82-89 (2012).
- G. A. Karpunin and E. Z. Ermolaeva, “Estimates of Collision Search Complexity for the Hash Function RIPEMD,” Prikl. Diskr. Mat. Suppl., No. 5, 43-44 (2012).
- M. Stevens, “Single-Block Collision Attack on MD5,” Cryptology ePrint Archive. Report 2012/040. 2012.
http://eprint.iacr.org/2012/040 . Cited January 15, 2015.
- I. Mironov and L. Zhang, “Applications of SAT Solvers to Cryptanalysis of Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2006), Vol. 4121, pp. 102-115.
- R. A. Merkle, “Certified Digital Signature,” in Lecture Notes in Computer Science (Springer, Heidelberg, 1990), Vol. 435, pp. 218-238.
- I. A. Damg@@{a}rd, “A Design Principle for Hash Functions, “ in Lecture Notes in Computer Science (Springer, Heidelberg, 1990), Vol. 435, pp. 416-427.
- E. Biham and A. Shamir, “Differential Cryptanalysis of DES-like Cryptosystems,” in Proc. 10th Annu. Int. Cryptology Conf. on Advances in Cryptology, Santa Barbara, USA, August 11-15, 1990 (Springer, London, 1991), pp. 2-21.
- S. A. Cook, “The Complexity of Theorem-Proving Procedures,” in Proc. 3rd Annu. ACM Symp. on Theory of Computing, Shaker Heights, USA, May 3-5, 1971 (ACM Press, New York, 1971), pp. 151-158.
- G. S. Tseitin, “On the Complexity of Proof in Prepositional Calculus,” Zap. Nauch. Sem. LOMI 8, 234-259 (1968).
- A. Biere, V. Heule, H. van Maaren, and T. Walsh, Handbook of Satisfiability (IOS Press, Amsterdam, 2009).
- M. Soos, K. Nohl, and C. Castelluccia, “Extending SAT Solvers to Cryptographic Problems,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2009), Vol. 5584, pp. 244-257.
- A. Semenov, O. Zaikin, D. Bespalov, and M. Posypkin, “Parallel Logical Cryptanalysis of the Generator A5/1 in BNB-Grid System,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2011), Vol. 6873, pp. 473-483.
- D. Jovanović and P. Janičić, “Logical Analysis of Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2005), Vol. 3717, pp. 200-215.
- I. V. Otpushchennikov and A. A. Semenov, “Technology for Translating Combinatorial Problems into Boolean Equations,” Prikl. Diskr. Mat., No. 1, 96-115 (2011).
- I. Otpushchennikov, A. Semenov, S. Kochemazov, Transalg: A Tool for Translating Procedural Descriptions of Discrete Functions to SAT (tool paper) , arXiv preprint: 1405.1544 [cs.AI] (Cornell Univ. Library, Ithaca, 2014).
http://arxiv.org/abs/1405.1544 . Cited January 15, 2015.
- J. C. King, “Symbolic Execution and Program Testing,” Commun. ACM 19 (7), 385-394 (1976).
- B. W. Kernighan and D. M. Ritchie, The C Programming Language (Prentice Hall, Englewood Cliffs, 1988; Vil’yams, Moscow, 2006).
- A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools (Addison-Wesley, Boston, 1986; Vil’yams, Moscow, 2001).
- A. J. Menezes, P. C. van Oorschot, and S. A. Vanstone, Handbook of Applied Cryptography (CRC Press, Boca Raton, 1996).
- J. P. Marques-Silva and K. A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Comput. 48 (5), 506-521 (1999).
- M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem Proving,” Commun. ACM 5 (7), 394-397 (1962).
- A. Haken, “The Intractability of Resolution,” Theor. Comp. Sci. 39, 297-308 (1985).
- P. Beame, H. Kautz, and A. Sabharwal, “Towards Understanding and Harnessing the Potential of Clause Learning,” J. Artif. Intell. Res. 22, 319-351 (2004).
- S. A. Cook and D. G. Mitchell, “Finding Hard Instances of the Satisfiability Problem: A Survey,” in Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (AMS Press, Providence, 1997), Vol. 35, pp. 1-17.
- F. Massacci and L. Marraro, “Logical Cryptanalysis as a SAT Problem,” J. Autom. Reason. 24 (1-2), 165-203 (2000).
- A. A. Semenov, O. S. Zaikin, D. V. Bespalov, and A. A. Ushakov, “SAT-approach for Cryptoanalysis of Some Stream Ciphering Systems,” Vychisl. Tekhnol. 13 (6), 134-150 (2008).
- O. S. Zaikin and A. A. Semenov, “Large-Block Parallelism Technology in SAT Problems,” Probl. Upr., No. 1, 43-50 (2008).
- A. A. Semenov, O. S. Zaikin, D. V. Bespalov, et al., “Inversion of Discrete Functions Using Multiprocessor Computers,” in Proc. 4th Int. Conf. on Parallel Computations and Control Problems, Moscow, October 27-29, 2008 (Trapeznikov Inst. Control Sci., Moscow, 2008), pp. 152-176.
- Yu. Evtushenko, M. Posypkin, and I. Sigal, “A Framework for Parallel Large-Scale Global Optimization,” Comput. Sci. Res. Dev. 23 (3-4), 211-215 (2009).
- M. A. Posypkin, O. S. Zaikin, D. V. Bespalov, and A. A. Semenov, “Solving the Cryptanalysis Problems of Stream Ciphers on Distributed Computer Systems,” Tr. Inst. Systems Anal., Ross. Akad. Nauk 46, 119-137 (2009).
- A. A. Semenov and O. S. Zaikin, “Application of the Monte Carlo Method for Estimating the Total Time of Solving the SAT Problem in Parallel,” Vychisl. Metody Programm. 15 (1), 22-35 (2014).
- O. S. Zaikin, M. A. Posypkin, A. A. Semenov, and N. P. Khrapov, “Using Volunteer Computation by the Example of the OPTIMA@home and SAT@home Projects,” Vestn. Univ. Nizhni Novgorod, No. 5, 340-347 (2012).
- O. S. Zaikin, A. A. Semenov, and M. A. Posypkin, “Procedures of Constructing Decomposition Sets for the Distributed Solution of SAT problems in the SAT@home Project,” in Large System Control (Inst. Problem Upravl., Moscow, 2013), Issue 43, pp. 138-156.
- O. S. Zaikin, “Implementation of Prediction Procedures to Evaluate the Complexity of Parallel Solution of SAT Problems,” Vestn. Ufimsk. Gos. Aviats. Tekhn. Univ. 14 (4), 210-220 (2010).
- O. S. Zaikin, I. V. Otpuschennikov, and A. A. Semenov, “Parallel Algorithms for Solving SAT-Problems in Application to Optimization Problems with Boolean Constraints,” Vychisl. Metody Programm. 12, 205-212 (2011).
- A. E. J. Hyv854rinen, T. A. Junttila, and I. Niemel854, “A Distribution Method for Solving SAT in Grids,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2006), Vol. 4121, pp. 430-435.
- A. E. J. Hyv854rinen, Grid Based Propositional Satisfiability Solving , Ph.D. Thesis (Aalto Univ., Aalto, 2011).
- D. De, A. Kumarasubramanian, and R. Venkatesan, “Inversion Attacks on Secure Hash Functions Using SAT Solvers,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2007), Vol. 4501, pp. 377-382.