CryptoSAT: A tool for SAT-based cryptanalysis

The security of symmetric key primitives comes from their exposure to public scrutiny in the context of competitions such as Advanced Encryption Standard, Secure Hash Algorithm 3, or currently CAESAR. However, due to the increasing number of primitives subjected to these competitions, the quality of the scrutiny relies on the availability of automated tools. Although SAT solvers have already proved useful for the automated analysis of these primitives, there is a lack of practical software tools for this purpose. This study describes a framework that aims to make SAT-based analyses accessible to cryptographers. The framework is implemented in a free open-source tool called CryptoSAT which is available in the public domain.