Sciweavers

Share
SAT
2009
Springer

Extending SAT Solvers to Cryptographic Problems

10 years 6 months ago
Extending SAT Solvers to Cryptographic Problems
Cryptography ensures the confidentiality and authenticity of information but often relies on unproven assumptions. SAT solvers are a powerful tool to test the hardness of certain problems and have successfully been used to test hardness assumptions. This paper extends a SAT solver to efficiently work on cryptographic problems. The paper further illustrates how SAT solvers process cryptographic functions using automatically generated visualizations, introduces techniques for simplifying the solving process by modifying cipher representations, and demonstrates the feasibility of the approach by solving three stream ciphers. To optimize a SAT solver for cryptographic problems, we extended the solver’s input language to support the XOR operation that is common in cryptography. To better understand the inner workings of the adapted solver and to identify bottlenecks, we visualize its execution. Finally, to improve the solving time significantly, we remove these bottlenecks by altering t...
Mate Soos, Karsten Nohl, Claude Castelluccia
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SAT
Authors Mate Soos, Karsten Nohl, Claude Castelluccia
Comments (0)
books