# What is SHA-256 in Conjunctive Normal Form?

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?

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

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.
• 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 – Geremia Apr 21 '15 at 1:40
• @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." – cpast Apr 21 '15 at 1:43
• @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. – cpast Apr 21 '15 at 6:27