Oct 01

On the resolution of cryptographic SAT instances

For decades, a tremendous amount of research is being devoted to the design of efficient algorithms to solve the Boolean satisfiability problem (SAT). In practice, modern SAT solvers are able to solve a variety of difficult problems with surprising performances, including cryptanalysis-related problems. The purpose of this thesis is to investigate strategies for tuning SAT solvers to the cryptanalysis of a family of symmetric-key functions in order to gain insight into what makes these functions difficult to break.

Supervisor: Frédéric Lafitte, Director: Olivier Markowitch