Differential Cryptanalysis with SAT, SMT, MILP and CP - a detailed comparison for bit-oriented primitives

Sep 14, 2026

Uploaded by Mack Lee

SAT, SMT, MILP, and CP have become central formalisms for differential cryptanalysis of cryptographic primitives. This paper reviews techniques for building differential characteristic search models within these four frameworks and conducts a systematic comparison across more than 20 primitives. The evaluation spans easy and hard instances, covering optimization, enumeration, and differential probability estimation, and includes 16 solvers to assess modeling choices and solver performance.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages25

Reading Time1 h 3 min

AccessFree to download

Introduction

Contributions

Preliminaries

Differential characteristic search as declarative solving

Modeling differences and probabilities

Models and propagation rules

Linear components and deterministic propagation

Non-linear components and stochastic propagation

Differential cryptanalysis with SAT, SMT, MILP, and CP: a detailed comparison for bit-oriented primitives Emanuele Bellini2[0000−0002−2349−0247], Alessandro De Piccoli 1[0000−0002−6399−3164], Mattia Formenti2[0009−0001−0069−6146], David Gerault2[0000−0001−8583−0668], Paul Huynh2[0000−0002−6965−3427], Simone Pelizzola 1[0009−0006−3991−1161], Sergio Polese, and Andrea Visconti 1[0000−0001−5689−8575] 1 Universit`a degli Studi di Milano, Milano, Italia {[name.lastname](name.lastname}@unimi.it)[}](name.lastname}@unimi.it)[@unimi.it](name.lastname}@unimi.it) 2 Technology Innovation Institute, Abu Dhabi, UAE {[name.lastname](name.lastname}@tii.ae)[}](name.lastname}@tii.ae)[@tii.ae](name.lastname}@tii.ae) Abstract. SAT, SMT, MILP, and CP, have become prominent in the differential cryptanalysis of cryptographic primitives. In this paper, wereview the techniques for constructing differential characteristic search models in these four formalisms. Additionally, we perform a systematic comparison encompassing over 20 cryptographic primitives and 16 solvers, on both easy and hard instances of optimisation, enumeration and differential probability estimation problems. Keywords: Differential cryptanalysis · SAT · SMT · MILP · CP. 1 Introduction The design and analysis of block ciphers is a time-consuming and error-prone task that involves tracing the propagation of bit-level or word-level patterns of all sorts, following intricate rules. Automatic tools have made such tasks significantly easier. In the case of differential cryptanalysis [9], one of the most widely used analysis technique, the studied patterns (differential characteristics) represent the propagation of a XOR difference between the inputs through the cipher, and are studied through the following methods: (1) ad hoc (include search algorithms implemented from scratch in general purpose programming languages, e.g. Matsui algorithm [34]); (2) Boolean Satisfiability and Satisfiability Modulo Theory (SAT/SMT); (3) Mixed-Integer Linear Programming (MILP); (4) Constraint Programming (CP) . In this paper, we provide an extensive review and performance comparison for the last three techniques for the search of differential characteristics for various ciphers. Contributions Our contributions are twofold: 2 Bellini et al. – We provide an extensive review of modeling techniques in SAT, SMT, MILP and CP for the search of differential characteristics, in Section 3; – We extensively compare these 4 methods on 3 different tasks: finding one optimal differential characteristic, enumerating all optimal differential characteristics, and estimating the probability of a differential. These tests are performed with 7 SAT solvers, 3 SMT solvers, 2 MILP solvers, 4 CP solvers, on over 20 primitives, resulting in the largest scale comparison of differential cryptanalysis models to date. The results are presented in Section 4 . The research community stands to benefit greatly from this extensive review and comparison of techniques, which provides a further steps towards a better understanding of how to solve the instances that are still out of reach. 2 Preliminaries A symmetric cryptographic primitive is usually a sequence of linear and nonlinear components transforming a plaintext (possibly with a key) into a ciphertext, usually by applying a simple round function to update the state for a number of rounds, each round using a round key derived from a key schedule algorithm. Differential cryptanalysis focuses on studying the probability of differentials, which map an XOR difference in the plaintexts to a differences in the ciphertexts. This probability is usually bounded by the probability of a differential characteristics, i.e. , a sequence of expected differences at each round (as described in Section A); the probability of the corresponding differential is related to the combined probabilities of all differential characteristics sharing the corresponding input and outpu

FAQs

What four formalisms does the paper compare for differential cryptanalysis?

The paper compares SAT, SMT, MILP, and CP as declarative approaches for searching differential characteristics.

Which tasks are evaluated in the systematic comparison?

The comparison covers finding one optimal differential characteristic, enumerating all optimal differential characteristics, and estimating the probability of a differential.

What kinds of cryptographic primitives and solver setups are included?

Experiments span over 20 cryptographic primitives and use 7 SAT solvers, 3 SMT solvers, 2 MILP solvers, and 4 CP solvers.

Sep 14, 2026

Uploaded by Mack Lee