Re: RC5-32/12/9 converted to 3SAT



On 11/09/2010 19:49, Paul Rubin wrote:
People have tried SAT solvers on crypto problems before, with
no luck as far as I know,

There are notable recent sucesses: weak stream ciphers
of the MiFare Classic contactless card, and/or DECT, and/GSM.

<http://eprint.iacr.org/2008/166>
<http://www.cs.virginia.edu/~kn5f/pdf/Research.Statement.Karsten.Nohl.pdf>
using some cousin of this stat-of-the-art, crypto-optimized SAT solver
<http://www.msoos.org/cryptominisat2>

Francois Grieu
.