Applying Satisfiability to the Analysis of Cryptography

SAT-solvers are (mostly) not used to directly attack cryptography software in this talk; they are used to rule out some classes of attacks.

In the most general case, program property verification is intractable, but specific instances can still be solved. When you have some industry-standard key sizes, you need to verify only a specific program, and then constants matter. So a good SAT solver can give you some useful information in a few minutes on a modern desktop computer about some real cryptography implementations.