Evaluating CNF/SMT Encodings for SAT-Based Differential Cryptanalysis of Lightweight Block Ciphers

Vahid Dastjerdi, Marzieh; Rahimi, Majid; Mirzaali Mazandarani, Iman; Sadeghi, Sadegh

doi:10.22042/isecure.2026.242936

Evaluating CNF/SMT Encodings for SAT-Based Differential Cryptanalysis of Lightweight Block Ciphers

Articles in Press

Document Type : Research Article

Authors

Marzieh Vahid Dastjerdi ¹^{, 2}

Majid Rahimi ²

Iman Mirzaali Mazandarani ²^{, 3}

Sadegh Sadeghi ¹

¹ Department of Mathematics, Institute for Advanced Studies in Basic Sciences (IASBS), Zanjan 45137-66731, Iran

² Computer Science Group, Research Center for Development of Advanced Technologies (RCDAT), Tehran, Iran

³ CPS2 Lab, Department of Communication, Faculty of Electrical Engineering, Shahid Rajaee Teacher Training University, Tehran, Iran

10.22042/isecure.2026.242936

Abstract

This study evaluates three encoding methods for automated differential cryptanalysis: (1) SMT formulations (using CVC), (2) standard CNF, and (3) size-optimised CNF (via Logic Friday). We assess these using four SAT/SMT solver types: single-core (CryptoMiniSat-v5, CaDiCaL), multicore (Treengeling), and massively parallel Mallob—novel to cryptanalysis. Encoding-solver combinations are tested on seven lightweight block ciphers representing distinct design philosophies: SPECK-32 and CHAM-64 (ARX structure), SIMON-32 (AND-RX structure), PRESENT, GIFT-128, and MIDORI-64 (4-bit S-box in SPN structure), and LBLOCK (Feistel structure). For each cipher, SAT/SMT instances targeting specific rounds and differential weights were generated, with wall-clock solving time, parallel efficiency, and modelling effort recorded. Our results establish criteria for optimal encoding-solver pairings that strike a balance between modelling simplicity and computational performance. Crucially, Mallob emerges as the state-of-the-art framework for large-scale automated differential cryptanalysis.

Keywords

Automated Cryptanalysis

CNF

SMT

CVC

Differential Cryptanalysis

Lightweight Block Cipher

[1] Eli Biham and Adi Shamir. Differential cryptanalysis of des-like cryptosystems. Journal of CRYPTOLOGY, 4:3–72, 1991.

[2] Nicky Mouha, Qingju Wang, Dawu Gu, and Bart Preneel. Differential and linear cryptanalysis using mixed-integer linear programming. In International Conference on Information Security and Cryptology, pages 57–76. Springer, 2011.

[3] A Mirzaie, S Ahmadi, and MR Aref. Division property-based integral attack on reduced-round sand-128. In 21st international ISC conference on information security & cryptology, 2024.

[4] Nicky Mouha and Bart Preneel. Towards finding optimal differential characteristics for arx: Application to salsa20. Cryptology ePrint Archive, 2013.

[5] Ling Sun, Wei Wang, and Meiqin Wang. Accelerating the search of differential and linear characteristics with the sat method. IACR Transactions on Symmetric Cryptology, pages 269–315, 2021.

[6] Harish Kumar Sahu, N Rajesh Pillai, Indivar Gupta, and Rajendra Kumar Sharma. Smt solver-based cryptanalysis of block ciphers. SN Computer Science, 1:1–12, 2020.

[7] David Gerault, Marine Minier, and Christine Solnon. Constraint programming models for chosen key differential cryptanalysis. In Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings 22, pages 584– 601. Springer, 2016.

[8] Hosein Hadipour, Sadegh Sadeghi, and Maria Eichlseder. Finding the impossible: Automated search for full impossible-differential, zerocorrelation, and integral attacks. In Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 128– 157. Springer, 2023.

[9] Hosein Hadipour, Simon Gerhalter, Sadegh Sadeghi, and Maria Eichlseder. Improved search for integral, impossible differential and zerocorrelation attacks: Application to ascon, forkskinny, skinny, mantis, present and qarmav2. IACR Transactions on Symmetric Cryptology, 2024(1):234–325, 2024.

[10] Emanuele Bellini, Alessandro De Piccoli, Mattia Formenti, David Gerault, Paul Huynh, Simone Pelizzola, Sergio Polese, and Andrea Visconti. Differential cryptanalysis with sat, smt, milp, and cp: a detailed comparison for bitoriented primitives. In International Conference on Cryptology and Network Security, pages 268– 292. Springer, 2023.

[11] Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244–257. Springer, 2009.

[12] Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133–152. Springer, 2024.

[13] Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In Proc. of SAT Competition 2017 – Solver and Benchmark Descriptions, volume B2017-1 of Department of Computer Science Series of Publications B, pages 14–15. University of Helsinki, 2017.

[14] Dominik Schreiber and Peter Sanders. Mallobsat: Scalable sat solving by clause sharing. Journal of Artificial Intelligence Research, 80, 2024.

[15] Stéphanie Delaune, Patrick Derbez, Paul Huynh, Marine Minier, Victor Mollimard, and Charles Prud’Homme. Skinny with scalpel-comparing tools for differential analysis. Cryptology ePrint Archive, 2020.

[16] Praveen Kumar Gundaram, Appala NaiduTentu, and Naresh Babu Muppalaneni. Performance of various smt solvers in cryptanalysis. In 2021 international conference on computing, communication, and intelligent systems (ICCCIS), pages 298–303. IEEE, 2021.

[17] Ling Sun and Meiqin Wang. Sok: modeling for large s-boxes oriented to differential probabilities and linear correlations. IACR Transactions on Symmetric Cryptology, pages 111–151, 2023.

[18] Tomáš Balyo, Nils Froleyks, Marijn JH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of sat competition 2020: Solver and benchmark descriptions. 2020.

[19] Murat Burhan Ilter and Ali Aydın Selçuk. Milp modeling of matrix multiplication: cryptanalysis of klein and prince. Turkish Journal of Electrical Engineering and Computer Sciences, 32(1):183– 197, 2024.

[20] Ahmed Abdelkhalek, Yu Sasaki, Yosuke Todo, Mohamed Tolba, and Amr M Youssef. Milp modeling for (large) s-boxes to optimize probability of differential characteristics. IACR Transactions on Symmetric Cryptology, pages 99–129, 2017.

[21] Helger Lipmaa and Shiho Moriai. Efficient algorithms for computing differential properties of addition. In International Workshop on Fast Software Encryption, pages 336–350. Springer, 2001.

[22] Stefan Kölbl, Gregor Leander, and Tyge Tiessen. Observations on the simon block cipher family. In Annual Cryptology Conference, pages 161–185. Springer, 2015.

[23] Carsten Sinz. Towards an optimal cnf encoding of boolean cardinality constraints. In International conference on principles and practice of constraint programming,pages827–831.Springer, 2005.

[24] Stefan Kölbl. CryptoSMT: An easy to use tool for cryptanalysis of symmetric primitives. https://github.com/kste/cryptosmt.

[25] Ray Beaulieu, Douglas Shors, Jason Smith, Stefan Treatman-Clark, Bryan Weeks, and Louis Wingers. The simon and speck lightweight block ciphers. In Proceedings of the 52nd annual design automation conference, pages 1–6, 2015.

[26] Bonwook Koo, Dongyoung Roh, Hyeonjin Kim, Younghoon Jung, Dong-Geon Lee, and Daesung Kwon. Cham: A family of lightweight block ciphers for resource-constrained devices. In International conference on information security and cryptology, pages 3–25. Springer, 2017.

[27] Dongyoung Roh, Bonwook Koo, Younghoon Jung, Il Woong Jeong, Dong-Geon Lee, Daesung Kwon, and Woo-Hwan Kim. Revised version of block cipher cham. In International Conference on Information Security and Cryptology, pages 1–19. Springer, 2019.

[28] Andrey Bogdanov, Lars R Knudsen, Gregor Leander, Christof Paar, Axel Poschmann, Matthew JB Robshaw, Yannick Seurin, and Charlotte Vikkelsoe. Present: An ultralightweight block cipher. In Cryptographic Hardware and Embedded Systems-CHES 2007: 9th International Workshop, Vienna, Austria, September 10-13, 2007. Proceedings 9, pages 450–466. Springer, 2007.

[29] Subhadeep Banik, Sumit Kumar Pandey, Thomas Peyrin, Yu Sasaki, Siang Meng Sim, and Yosuke Todo. Gift: A small present: Towards reaching the limit of lightweight encryption. In Cryptographic Hardware and Embedded Systems–CHES 2017: 19th International Conference, Taipei, Taiwan, September 25-28, 2017, Proceedings, pages 321–345. Springer, 2017.

[30] Subhadeep Banik, Andrey Bogdanov, Takanori Isobe, Kyoji Shibutani, Harunaga Hiwatari,Toru Akishita, and Francesco Regazzoni. Midori: A block cipher for low energy. In International Conference on the Theory and Application of Cryptology and Information Security, pages 411– 436. Springer, 2015.

[31] Wenling Wu and Lei Zhang. Lblock: a lightweight block cipher. In International conference on applied cryptography and network security, pages 327–344. Springer, 2011.