Evaluating Coppersmith’s Criteria by way of SAT Solving

S-boxes are the non-linear part of DES cryptosystem. Along the years it has became clear that any kind of edit to the structure of DES S-boxes increases the probability of success of breaking the algorithm, which was very carefully designed. The reason why the S-boxes were built in this way was clarified by Coppersmith, years after the publication of the encryption algorithm. The aim of this thesis is to investigate on Coppersmith’s DES S-boxes design criteria and to evaluate them by way of SAT Solving, in order to analyze the performance of SAT-Solvers for different versions of DES algorithm, in which S-boxes respect only a sample of Coppersmith’s design criteria. This aim is achieved thanks to the implementation of a Python tool: DESBoxGen. The main challenge in the design of DESBoxGen is the one of finding a way to efficiently generating S-boxes satisfying certain criteria.