[Cryptography] List of Proven Secure Ciphers / Hashes

[R. Hirschfeld]

> Date: Thu, 11 Sep 2014 01:13:33 +1200
> From: Peter Gutmann <pgut001 at cs.auckland.ac.nz>
> 
> "R. Hirschfeld" <ray at unipay.nl> writes:
> 
> >Translate your factoring instance into a SAT instance via a poly-time (or
> >log-space) reduction.
> 
> Yeah, and now you're back to the how-to-travel-to-Mars problem:
> 
> 1. Build a big rocket.
> 2. Round up some astronauts.
> 3. Fly to Mars.  QED.
> 
> The fact that you can state a solution doesn't mean that you can actually do
> it.  I specifically chose SAT because of its everything-maps-to-SAT status,
> but was trying to point out that having a SAT solver doesn't automatically
> break RSA or DH or whatever.

The reduction is something you can actually do.  See for example
http://cstheory.stackexchange.com/questions/6755/fast-reduction-from-rsa-to-sat
for some ideas (and links to some running code).  Even if you use the
construction from the proof of Cook's Theorem (which builds a Boolean
formula from the tableau of the computation of a Turing machine such
that the formula is satisfiable iff the machine accepts, or at least
that's how it was done way back when I learned it) it would be a pain
in the ass and a big mess, but it's not travel-to-Mars-hard.  ;-)