Over time, I’ve developed various tools to assist in the analysis of cryptographic algorithms. A collection of tools can be found here, along with their source code.

Toolkit for Counting Active S-boxes using Mixed-Integer Linear Programming (MILP)

This toolkit can be used to prove the security of cryptographic ciphers against linear and differential cryptanalysis. The toolkit generates a Mixed-Integer Linear Programming (MILP) problem which counts the minimum number of (linearly or differentially) active S-boxes for a given cipher. Currently, AES and xAES are implemented (both in the single-key and related-key setting), as well as Enocoro-128v2 (in the related-key setting). The technique is very general, and can be adapted to other ciphers with little effort.

Toolkit for Bounding Characteristics using SAT/SMT Solvers

This toolkit can be used to prove the security of cryptographic ciphers against differential cryptanalysis. It is developed specifically for Addition-Rotation-XOR (ARX) ciphers. It generates a SAT/SMT problem that calculates finds differential characteristics of a specific weight, to be solved using STP. The code applies this approach to the Salsa20 stream cipher. Again, the technique is general and can easily be adapted to other ciphers.

Toolkit for the differential cryptanalysis of S-functions

An increasing number of cryptographic primitives use operations such as addition modulo 2n, multiplication by a constant and bitwise Boolean functions as a source of non-linearity. We generalize such constructions by introducing the concept of S-functions, which calculates the i-th output bit using only the inputs of the i-th bit position and a finite state S[i]. Although S-functions have been analyzed before, our toolkit is the first to present a fully general and efficient framework to determine their differential properties. We show how to calculate the probability that given input differences lead to given output differences, as well as how to count the number of output differences with non-zero probability. The toolkit also provides a general algorithm to efficiently list the output differences with the highest probability, for a given type of difference and operation.