3
$\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
    $\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$ – fgrieu Apr 21 '15 at 5:50
  • $\begingroup$ @fgrieu I've incorporated your good suggestion into improving the question. thank you. $\endgroup$ – Geremia Apr 21 '15 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$ – fgrieu Apr 21 '15 at 6:09
3
$\begingroup$

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.

| improve this answer | |
$\endgroup$
  • $\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 '15 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 '15 at 1:43
  • 2
    $\begingroup$ @Geremia It would be much easier to write SHA and generate the CNF using one of many tools. $\endgroup$ – Thomas M. DuBuisson Apr 21 '15 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 '15 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$ – fgrieu Apr 21 '15 at 7:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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