Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions

  • Saeed NejatiEmail author
  • Jia Hui Liang
  • Catherine Gebotys
  • Krzysztof Czarnecki
  • Vijay Ganesh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)


SAT solvers are increasingly being used for cryptanalysis of hash functions and symmetric encryption schemes. Inspired by this trend, we present MapleCrypt which is a SAT solver-based cryptanalysis tool for inverting hash functions. We reduce the hash function inversion problem for fixed targets into the satisfiability problem for Boolean logic, and use MapleCrypt to construct preimages for these targets. MapleCrypt has two key features, namely, a multi-armed bandit based adaptive restart (MABR) policy and a counterexample-guided abstraction refinement (CEGAR) technique. The MABR technique uses reinforcement learning to adaptively choose between different restart policies during the run of the solver. The CEGAR technique abstracts away certain steps of the input hash function, replacing them with the identity function, and verifies whether the solution constructed by MapleCrypt indeed hashes to the previously fixed targets. If it is determined that the solution produced is spurious, the abstraction is refined until a correct inversion to the input hash target is produced. We show that the resultant system is faster for inverting the SHA-1 hash function than state-of-the-art inversion tools.


  1. 1.
    Aoki, K., Sasaki, Y.: Preimage attacks on one-block MD4, 63-step MD5 and more. In: Avanzi, R.M., Keliher, L., Sica, F. (eds.) SAC 2008. LNCS, vol. 5381, pp. 103–119. Springer, Heidelberg (2009). CrossRefGoogle Scholar
  2. 2.
    Audemard, G., Simon, L.: GLUCOSE: a solver that predicts learnt clauses quality. SAT Compet. 7–8 (2009)Google Scholar
  3. 3.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. IJCAI 9, 399–404 (2009)Google Scholar
  4. 4.
    Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 118–126. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  5. 5.
    Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 28–33. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  6. 6.
    Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. 4, 75–97 (2008)zbMATHGoogle Scholar
  7. 7.
    Biere, A.: Lingeling, Plingeling, Picosat and Precosat at SAT Race 2010. FMV Report Series Technical report, 10/1 (2010)Google Scholar
  8. 8.
    Biere, A.: Lingeling ayv (2015).
  9. 9.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)CrossRefGoogle Scholar
  10. 10.
    Biere, A., Fröhlich, A.: Evaluating CDCL restart schemes. In: Pragmatics of SAT (2015)Google Scholar
  11. 11.
    Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. (TISSEC) 12(2), 10 (2008)CrossRefGoogle Scholar
  12. 12.
    Chen, J.: A bit-encoding phase selection strategy for satisfiability solvers. In: Gopal, T.V., Agrawal, M., Li, A., Cooper, S.B. (eds.) TAMC 2014. LNCS, vol. 8402, pp. 158–167. Springer, Cham (2014). CrossRefGoogle Scholar
  13. 13.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). CrossRefGoogle Scholar
  14. 14.
    De, D., Kumarasubramanian, A., Venkatesan, R.: Inversion attacks on secure hash functions using sat solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 377–382. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  15. 15.
    De Cannière, C., Rechberger, C.: Finding SHA-1 characteristics: general results and applications. In: Lai, X., Chen, K. (eds.) ASIACRYPT 2006. LNCS, vol. 4284, pp. 1–20. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  16. 16.
    De Cannière, C., Rechberger, C.: Preimages for reduced SHA-0 and SHA-1. In: Wagner, D. (ed.) CRYPTO 2008. LNCS, vol. 5157, pp. 179–202. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  17. 17.
    Dobbertin, H.: Cryptanalysis of MD4. In: Gollmann, D. (ed.) FSE 1996. LNCS, vol. 1039, pp. 53–69. Springer, Heidelberg (1996). CrossRefGoogle Scholar
  18. 18.
    Eén, N., Sörensson, N.: Minisat 2.2.
  19. 19.
    Eichlseder, M., Mendel, F., Schläffer, M.: Branching heuristics in differential collision search with applications to SHA-512. IACR Cryptology ePrint Archive 2014:302 (2014)Google Scholar
  20. 20.
    Espitau, T., Fouque, P.-A., Karpman, P.: Higher-order differential meet-in-the-middle preimage attacks on SHA-1 and BLAKE. In: Gennaro, R., Robshaw, M. (eds.) CRYPTO 2015. LNCS, vol. 9215, pp. 683–701. Springer, Heidelberg (2015). CrossRefGoogle Scholar
  21. 21.
    Fiorini, C., Martinelli, E., Massacci, F.: How to fake an RSA signature by encoding modular root finding as a SAT problem. Discrete Appl. Math. 130(2), 101–127 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    PUB FIPS: 180–4. Federal Information Processing Standards Publication, Secure Hash (2011)Google Scholar
  23. 23.
    Gagliolo, M., Schmidhuber, J.: Learning restart strategies. In: IJCAI, pp. 792–797 (2007)Google Scholar
  24. 24.
    Garivier, A., Moulines, E.: On upper-confidence bound policies for switching bandit problems. In: Kivinen, J., Szepesvári, C., Ukkonen, E., Zeugmann, T. (eds.) ALT 2011. LNCS (LNAI), vol. 6925, pp. 174–188. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  25. 25.
    Haim, S., Walsh, T.: Restart strategy selection using machine learning techniques. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 312–325. Springer, Heidelberg (2009). CrossRefGoogle Scholar
  26. 26.
    Jovanović, D., Janičić, P.: Logical analysis of hash functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 200–215. Springer, Heidelberg (2005). CrossRefGoogle Scholar
  27. 27.
    Khovratovich, D., Rechberger, C., Savelieva, A.: Bicliques for preimages: attacks on Skein-512 and the SHA-2 family. In: Canteaut, A. (ed.) FSE 2012. LNCS, vol. 7549, pp. 244–263. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  28. 28.
    Knellwolf, S., Khovratovich, D.: New preimage attacks against reduced SHA-1. In: Safavi-Naini, R., Canetti, R. (eds.) CRYPTO 2012. LNCS, vol. 7417, pp. 367–383. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  29. 29.
    Lafitte, F., Nakahara Jr., J., Van Heule, D.: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages. J. Satisf. Boolean Model. Comput. 9, 1–25 (2014)MathSciNetGoogle Scholar
  30. 30.
    Lai, X., Massey, J.L.: Hash functions based on block ciphers. In: Rueppel, R.A. (ed.) EUROCRYPT 1992. LNCS, vol. 658, pp. 55–70. Springer, Heidelberg (1993). Google Scholar
  31. 31.
    Legendre, F., Dequen, G., Krajecki, M.: Encoding hash functions as a SAT problem. In: 2012 IEEE 24th International Conference on Tools with Artificial Intelligence (ICTAI), vol. 1, pp. 916–921. IEEE (2012)Google Scholar
  32. 32.
    Legendre, F., Dequen, G., Krajecki, M.: Logical reasoning to detect weaknesses about SHA-1 and MD4/5. IACR Cryptology ePrint Archive 2014:239 (2014)Google Scholar
  33. 33.
    Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). Google Scholar
  34. 34.
    Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: Proceedings of the 2nd Israel Symposium on the Theory and Computing Systems, pp. 128–133. IEEE (1993)Google Scholar
  35. 35.
    Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Massacci, F.: Using walk-SAT and Rel-SAT for cryptographic key search. In: IJCAI 1999, pp. 290–295 (1999)Google Scholar
  37. 37.
    Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reasoning 24(1–2), 165–203 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Mendel, F., Nad, T., Schläffer, M.: Finding SHA-2 characteristics: searching through a minefield of contradictions. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 288–307. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  39. 39.
    Mendel, F., Nad, T., Schläffer, M.: Improving local collisions: new attacks on reduced SHA-256. In: Johansson, T., Nguyen, P.Q. (eds.) EUROCRYPT 2013. LNCS, vol. 7881, pp. 262–278. Springer, Heidelberg (2013). CrossRefGoogle Scholar
  40. 40.
    Merkle, R.C.: One way hash functions and DES. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 428–446. Springer, New York (1990). CrossRefGoogle Scholar
  41. 41.
    Mironov, I., Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 102–115. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  42. 42.
    Morawiecki, P., Srebrny, M.: A SAT-based preimage analysis of reduced KECCAK hash functions. Inf. Process. Lett. 113(10), 392–397 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535. ACM (2001)Google Scholar
  44. 44.
    Nossum, V.: SAT-based preimage attacks on SHA-1 (2012)Google Scholar
  45. 45.
    Nossum, V.: Instance generator for encoding preimage, second-preimage, and collision attacks on SHA-1. In: Proceedings of the SAT Competition, pp. 119–120 (2013)Google Scholar
  46. 46.
    Rintanen, J.: Planning and SAT. Handbook of Satisfiability, vol. 185, pp. 483–504 (2009)Google Scholar
  47. 47.
    Soos, M.: CryptoMiniSat 4.5.3 (2015).
  48. 48.
    Srebrny, M., Srebrny, M., Stepien, L.: SAT as a programming environment for linear algebra and cryptanalysis. In: ISAIM (2008)Google Scholar
  49. 49.
    Stevens, M., Karpman, P., Peyrin, T.: Freestart collision for full SHA-1. Cryptology ePrint Archive (2015/967):1–21 (2015)Google Scholar
  50. 50.
    Sutton, R.S., Barto, A.G.: Introduction to Reinforcement Learning, vol. 135. MIT Press, Cambridge (1998)Google Scholar
  51. 51.
    Tomb, A.: Applying satisfiability to the analysis of cryptography (2015).
  52. 52.
    Wang, X., Yu, H.: How to break MD5 and other hash functions. In: Cramer, R. (ed.) EUROCRYPT 2005. LNCS, vol. 3494, pp. 19–35. Springer, Heidelberg (2005). CrossRefGoogle Scholar
  53. 53.
    Wang, X., Yu, H., Yin, Y.L.: Efficient collision search attacks on SHA-0. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 1–16. Springer, Heidelberg (2005). CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Saeed Nejati
    • 1
    Email author
  • Jia Hui Liang
    • 1
  • Catherine Gebotys
    • 1
  • Krzysztof Czarnecki
    • 1
  • Vijay Ganesh
    • 1
  1. 1.University of WaterlooWaterlooCanada

Personalised recommendations