Author = Sadegh Sadeghi

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

Articles in Press, Accepted Manuscript, Available Online from 01 May 2026

https://doi.org/10.22042/isecure.2026.242936

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

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.

Differential Fault Analysis of the BipBip Block Cipher

Volume 17, Issue 2, July 2025, Pages 223-232

https://doi.org/10.22042/isecure.2025.217885

Narges Mokhtari, Navid Vafaei, Sadegh Sadeghi, Nasour Bagheri

Abstract Differential Fault Analysis (DFA) represents one of the most effective physical attacks against cryptographic algorithms. It exploits the implementation weaknesses by injecting faults. DFA is a cryptographic technique in which an attacker intentionally injects errors into a cryptographic system and leverages the differences caused by these deliberate faults while executing cryptographic algorithms. The attacker can gain insights into the cryptographic operations by comparing the correct and faulty ciphertexts. This research applies DFA to BipBip, an ultra-low-latency tweakable block cipher characterized by a 24-bit tweakable block and a 256-bit master key. Our primary assumption is that the tweak remains fixed within BipBip. This study’s findings reveal that the structural design of the BipBip block cipher is susceptible to differential fault analysis. We demonstrate a significant vulnerability by injecting a precise number of 30 random faults into different states of BipBip. Through an exhaustive search process, we successfully retrieved the master key. Furthermore, this research marks the first application of differential fault analysis in identifying implementation weaknesses within BipBip, highlighting a critical security concern.