Re:Applying Satisfiability to the Analysis of Cryptography
by BrainInAJar on Monday September 28, 2015 @06:30PM
(#10293634)
Err, The site is pretty sparse on info, but "Applying SAT to crypto" wouldn't really gain you much would it? "Applying an NP-complete problem to the analysis of a definitely-not-NP-complete-&-maybe-not-even-NP-hard problem" ?
Re:Applying Satisfiability to the Analysis of Cryptography
by 9mit3t2m9h9a on Monday September 28, 2015 @07:35PM
(#10293868)
As for info: there is a link to full slides.
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.
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.