New Results in Direct SAT-Based Cryptanalysis of DES-Like Ciphers

  • Michał ChowaniecEmail author
  • Mirosław Kurkowski
  • Michał Mazur
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 889)


SAT based cryptanalysis is one of efficient ways to investigate about desire properties of symmetric ciphers. In this paper we show our research and new experimental results in the case of SAT based, direct cryptanalysis of DES-like ciphers. For this, having a given cipher, we built firstly propositional logical formula that encode the cipher’s algorithm. Next, having a randomly generated plaintext, and a key we compute the proper ciphertext. Finally, using SAT solvers, we explore cipher properties in the case of plaintext and ciphertext cryptanalysis. In our work we compare several SAT solvers: new ones and some rather old but so far efficient. We present our results in the case of original version of DES cipher and its some modifications.


Symmetric ciphers Satisfiability SAT based cryptanalysis 


  1. 1.
    Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75 – 97 (2008). Delft UniversityGoogle Scholar
  2. 2.
    Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)Google Scholar
  3. 3.
    Biere, A.: Lingeling, Plingeling, Picosat and Precosat at SAT Race 2010. Technical Report FMV Reports Series 10/1, Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria (2010)Google Scholar
  4. 4.
    Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Balint, A., Belov, A., Heule, M., Jarvisalo, M. (eds.) Proceedings of SAT Competition 2013, vol. B-2013-1, Department of Computer Science Series of Publications B, pp. 51–52, University of Helsinki (2013)Google Scholar
  5. 5.
    Biham, E., Shamir, A.: Differential cryptanalysis of DES-like cryptosystems. J. Cryptol. 4(1), 3–72 (1991)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Chen, J.: Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, vol. B-2017-1, Department of Computer Science Series of Publications B, University of Helsinki (2017)Google Scholar
  7. 7.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Dudek, P., Kurkowski, M., Srebrny, M.: Towards parallel direct SAT-based cryptanalysis. In: PPAM 2011 Proceedings. LNCS, vol. 7203, pp. 266-275. Springer (2012)Google Scholar
  10. 10.
    Dwivedi, A.D., et al.: SAT-based cryptanalysis of authenticated ciphers from the CAESAR Competition. In: Proceedings of the 14th International Joint Conference on e-Business and Telecommunications (ICETE 2017). SECRYPT, vol. 4, pp. 237–246 (2017)Google Scholar
  11. 11.
  12. 12.
    Lafitte, F., Lerman, L., Markowitch, O., van Heule, D.: SAT-based cryptanalysis of ACORN, IACR Cryptology ePrint Archive, vol. 2016, p. 521 (2016)Google Scholar
  13. 13.
    Lafitte, F., Nakahara Jr., J., van Heule, D.: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages. JSAT 9, 1–25 (2014)MathSciNetGoogle Scholar
  14. 14.
    Massacci, F.: Using Walk-SAT and Rel-SAT for cryptographic key search. In: Dean, T. (ed.) IJCAI, pp. 290–295. Morgan Kaufmann (1999)Google Scholar
  15. 15.
    Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reason. 24(165), 165–203 (2000)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Matsui, M.: The first experimental cryptanalysis of the data encryption standard. In: Desmedt, Y. (ed.) CRYPTO. LNCS, vol. 839, pp. 1–11. Springer (1994)Google Scholar
  17. 17.
    Menezes, A., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)Google Scholar
  18. 18.
    Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Proceedings of 12th International Conference on Theory and Applications of Satisfiability Testing - SAT 2009, Swansea, UK, pp. 244 – 257 (2009)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Michał Chowaniec
    • 1
    Email author
  • Mirosław Kurkowski
    • 1
  • Michał Mazur
    • 1
  1. 1.Institute of Computer SciencesCardinal Wyszynski UniversityWarsawPoland

Personalised recommendations