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.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Delaune, Stéphanie; Derbez, Patrick; Huynh, Paul; Minier, Marine; Mollimard, Victor; Prud’homme, Charles: Efficient methods to search for best differential characteristics on SKINNY (2021)
- Gerault, David; Lafourcade, Pascal; Minier, Marine; Solnon, Christine: Computing AES related-key differential characteristics with constraint programming (2020)
- Lafitte, Frédéric; Nakahara, Jorge jun.; van Heule, Dirk: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages (2014)