4
$\begingroup$

What is the conjunctive normal form (CNF) representation of $\text{SHA-256}(m)=h$, where $m$ is of fixed (or bounded) size and $h$ is 256 bit?

$\endgroup$
3
  • 4
    $\begingroup$ The equation $\text{SHA-256}(m)=h$ where $m$ is of fixed (or bounded) size, and $h$ 256-bit, CAN easily be written in CNF by applying the definition of SHA-256, step by step; the CNF problem resulting will not be huge. and can legitimately be considered a CNF representation of the SHA-256 algorithm. A standard CNF solver using it will compute $h$ from $m$; or a few missing bits of $m$ from the other bits and $h$.$\;$ Asking for "the simplest" such representation is not well defined (and it will likely be hard to get the simplest); what's your criteria for "simple"? (please edit question) $\endgroup$ Apr 21, 2015 at 5:50
  • $\begingroup$ @fgrieu I've incorporated your good suggestion into improving the question. thank you. $\endgroup$
    – Geremia
    Apr 21, 2015 at 6:00
  • $\begingroup$ Dejan Jovanović and Predrag Janičić's Logical Analysis of Hash Functions (in Frontiers of Combining Systems, 2005) has a section on Encoding of Hash Functions into Instances of SAT Problem, which is what you are looking for. $\;$ Caveat: I only glanced at it; this is a pointer, not a recommendation. $\endgroup$ Apr 21, 2015 at 6:09

2 Answers 2

3
$\begingroup$

This answer was for the original question:

What is the simplest conjunctive normal form (CNF) representation of the SHA-256 algorithm?


There is none. Conjunctive normal form is for Boolean formulas, which have a single truth value. SHA-256 is not a Boolean formula (SHA-256(x) is not "true" or "false.") Furthermore, CNF is only applicable if you have a fixed number of variables; this is not true for SHA-256, which has variable-length input. At best you could have 256 different formulas, each for one bit of the output, and have $2^{64}+63$ different variables in each formula.

You've probably confused decision problems with function problems. Any algorithm that returns "true" or "false" can be represented, ultimately, as a gigantic Boolean formula. Anything not just returning "true" or "false" cannot, as a Boolean formula returns only "true" or "false." While there is a $2^{64}+63+256$-variable formula that evaluates to "is $x_1\ldots x_{256}$ the SHA-256 hash of the $x_{257}\ldots x_{320}$-bit number stored in $x_{321}\ldots x_{\text{last}}$," the formula is really just one of those things that exists in theory and not in practice.

$\endgroup$
10
  • $\begingroup$ Where "in theory" is the «$2^{64}+63+256$-variable formula that evaluates to "is $x_1\ldots x_{256}$ the SHA-256 hash of the $x_{257}\ldots x_{320}$-bit number stored in $x_{321}\ldots x_{\text{last}}$»? Are there any papers or books on this? thanks $\endgroup$
    – Geremia
    Apr 21, 2015 at 1:40
  • $\begingroup$ @Geremia SHA-256 supports inputs up to $2^{64}-1$ bits in length; then you add $64$ inputs because you need to know how long the message actually is (an input to a Boolean formula can only be 1 or 0, and so you need to supply both enough inputs for any SHA-256 input and enough inputs for the length of the SHA-256 input, which is an additional 64 bits). The "in theory" is "that's a really big formula, so you aren't going to find a version that is physically capable of being written down." $\endgroup$
    – cpast
    Apr 21, 2015 at 1:43
  • 3
    $\begingroup$ @Geremia It would be much easier to write SHA and generate the CNF using one of many tools. $\endgroup$ Apr 21, 2015 at 5:53
  • 1
    $\begingroup$ @fgrieu That appears to only cover a fixed input length less than the length of the output of the hash function. The huge number of variables here are absolutely required -- you cannot encode a generic SHA-256 input with less than $2^{64}$ variables, since there are a bare minimum of $2^{2^{64}}$ possible inputs.of maximal length (leaving aside shorter inputs). All the paper describes is SAT-equivalence, not actual equivalence. $\endgroup$
    – cpast
    Apr 21, 2015 at 6:27
  • 1
    $\begingroup$ @cpast: indeed, the CNF formula is of manageable size only for bounded message size. The CNF formula is many times as big as the message is, and about proportional to that; the number of variables also is about proportional. $\endgroup$ Apr 21, 2015 at 7:31
2
$\begingroup$

Depending on whether you use Tseitin adders or espresso logic minimization adders, SHA256 can be encoded in CNF. The number of variables with the former would be around 100000 vs 30000 but the clauses far fewer with the former and far more with the latter. There is a tradeoff and SAT solvers practically will work better on one or the other which must be determined experimentally as they are heuristical solvers.

The other answer here is simply wrong, there are several repositories on github with practical code generating sha256 instances. A bit suspicious it's up voted. Worse yet it's been done for sha256(sha256(x)). E.g. satcoin, etc.

Its not only practically possible but used for cryptanalysis. Granted beyond 16 or so bits the instance becomes usually harder than mere brute force.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.