Parallel SAT for Cryptanalysis

SAT solvers recently have increasingly been used in many applications, including AI, planning, verification and security. In this project we are trying to use SAT solvers and SAT-based techniques in the domain of Cryptography. Our approach mainly relies on tailoring the internals of the SAT solvers to the cryptographic problems. But we also made contributions that are useful for non-crypto problems as well (namely our splitting heuristic in our parallel SAT solver).

We are working on these lines of research:

  • Programmatic SAT for algebraic cryptanalysis
  • Machine learning for splitting heuristics in parallel SAT solvers