Abstract
Differential and linear cryptanalysis are crucial tools for designing and evaluating the security of symmetric cryptographic primitives. Modern symmetric cryptographic designs, such as AES and Keccak, utilize the "wide trail strategy", which aims to create round functions with strong resistance against differential and linear cryptanalysis. Good resistance requires the absence of high-probability differential propagation patterns, called differential trails, and high-correlation propagation patterns, called linear trails. Thus, proving bounds on the probability of differential trails and correlation of linear trails is essential.
For some cryptographic primitives, these bounds can be proved analytically. For example, in AES, a 4-round differential trail has a probability of at most 2^{-150}. Proving this bound is straightforward for AES because its round functions operate on groups of bits (bytes) and process state bits within these groups, a property known as strong alignment.
In contrast, primitives like Keccak have weak alignment, meaning their round functions operate on single bits. In this case, computer assistance is required to prove such bounds. Computer-aided tools are categorized into general-purpose solvers (like SAT or MILP) and dedicated tools. This thesis focuses on performing trail searches using dedicated tools in various unaligned primitives, while also investigating certain properties of their round functions.
