Question about preimage handling

[twine-lifa-sifa]

When generating CNF for SHA-256 preimage attacks, does the tool model the first preimage (finding any message that hashes to the given target) or the second preimage (finding a different message that hashes to the same target as a known message)?

[nahiyan]

Hi,

Thanks for checking out my work! The SHA-256 CNF generator currently supports only collision attacks. For pre-image attacks, encoders exist only for MD4 and MD5 — not SHA-256. Would you need one for SHA-256 as well?

[twine-lifa-sifa]

Hi,
Thanks for the clarification.

Yes, I’m planning to model and encode first preimage for SHA-256 into CNF.
Has any work already been done in this direction?

The existing encoder in encoders/nejati-preimage seems to be modeling second preimage for SHA-2 and other hash functions — is that correct?

[nahiyan]

Sorry for the confusion — you’re right. There is a version of Nejati’s encoder that supports pre-image attacks for SHA-256, though I’ve only ever used it for MD4 and MD5. While there are many papers on SHA-256 pre-image attacks, I’m not sure if SAT solvers were actually used in those cases.

I don’t believe Nejati’s encoder handles second pre-image attacks. Perhaps lines 93–98 in main.cpp caused the confusion? If you check the hash instance constructor in hash.cpp, it encodes only a single message, not a message pair. In other words, it’s focused solely on finding a message (optionally with some bits fixed) for a given hash.

If you’re exploring encoders for inversion attacks on SHA-256, you might want to look into Transalg — a CNF encoder that compiles high-level C-like code. Its adders might outperform Nejati’s for pre-image attacks, though only benchmarks can confirm that. For example, I think this Transalg code encodes a SHA-256 (first) pre-image attack. Hope this helps!

[twine-lifa-sifa]

Thanks for your detailed response!

From my testing, when specifying the target — whether randomly generated or manually provided — the tool requires both a 512-bit input message and its corresponding 256-bit digest via stdin. In other words, it expects a message–digest pair. Then, when the generated CNF is solved and the verify-sha256 script is run, it finds a different input message that produces the same digest. If I’m not mistaken, that matches the definition of a second preimage attack.

Is it possible to provide only the 256-bit digest as the target (without the original 512-bit message) and have the encoder still work, or is that unsupported?

Thanks for the suggestion about Transalg — I’ll definitely take a look at it.

One question: if I simply reduce the number of rounds in the SHA-256 implementation within the encoder’s code, will the generated CNF then correspond to a reduced-round first preimage attack? Or would additional modifications to the encoding be required for it to correctly handle fewer rounds?

[nahiyan]

Thanks for trying out the encoder!

I don't see the encoder taking or requiring an input message from the user. Can you describe how you provided the input message?

I'll get back to your other concerns after we work out this issue.

[twine-lifa-sifa]

Thanks for the quick reply.

What I’m seeing locally

When I run with --target random, the encoder itself generates both a 512-bit message and its 256-bit digest. If I also pass --print_target, it prints both lines (message first, then digest) and exits. Example:

./main --function sha256 --rounds 20 --target random --print_target > sha256-20-print.txt

The output file contains two lines: first 16 hex words (512-bit message), then 8 hex words (256-bit digest).

When I switch to --target stdin, the program expects me to provide both the 512-bit input message and the 256-bit digest on stdin (again: two lines, message first, then digest). If I supply only the digest, it aborts with the input/output read assertions. Example that works:

target.txt (two lines):

63afa978 6bead539 11150d59 27b0d0fd 63307303 01db8c73 7f216d20 3c14ff63 40001595 421918bc 33c018e6 2ae271b8 6ac8360e 318d0e6c 3e8a23f0 5a1b302a
48938777 1cc030d6 5211fa6d 224c66e9 460ffd29 f3925498 9a6ee2ca 9d7b82db

Command to generate the CNF:

./main --function sha256 --rounds 20 --target stdin < target.txt > sha256-20-preimage.cnf

If I provide only the second line (the 8 digest words), I hit the assertion that checks rcnt == f->inputSize (and similarly for outputSize), which matches what I observed earlier.

After solving the generated CNF, the verify-sha256 script reports a different input message that hashes to the same digest as the provided pair, which (to me) looks like a second-preimage workflow: the known message–digest pair is treated as the reference, and the solver is driven to find a distinct message with the same digest.

Is there a supported mode where I can pass only the 256-bit digest (no original 512-bit message) so the CNF encodes a first preimage instance directly?

[nahiyan]

I see now — you’re using Saeed Nejati’s original encoder, not my modified version from this repository. I’ve modified Nejati’s crypto encoders from https://github.com/saeednj/SAT-encoding for my research with SHA-256 collision attacks and MD4/MD5 inversion attacks in mind.

The original encoder works with a message–hash pair, either randomized or provided by the user. However, your command didn’t set the number of fixed input bits, so it defaulted to -F 0. In that case, the provided message has no effect on the encoding. You can confirm this by generating two CNFs with the same hash but different messages — they’ll be identical.

With -F 0, the SAT solver can choose any message bits that produce the given hash. That’s why your solution differs from the provided message — you’ve found a second pre-image by chance, but the encoder wasn’t configured for a second pre-image attack.

For a first pre-image attack (inversion), use my version of the encoder from this repository — it takes the hash/digest directly as an argument, not via stdin. It currently supports only 128-bit hashes (MD4, MD5), not 256-bit ones like SHA-256, but I can add SHA-256 support and run integrity tests if you want.

[twine-lifa-sifa]

Yes, that’s correct — since I couldn’t find the verify_sha256 module in your repository, I turned to Nejati’s original repo and assumed its behavior would be the same as yours.

I’d really appreciate it if you could add SHA-256 support as well, or let me know the required modifications to enable it.

Thanks in advance!

[nahiyan]

Okay, I'll add support for SHA-256 soon and let you know. I have excluded the verifier since I created my own version in another directory, but I can add it back.

To answer your previous question about round-reduction — yes, the encoder will only encode the hash function for the provided number of rounds. You don't need any further modifications, and you can also verify the solutions just to be sure they correspond to the provided number of steps.

[twine-lifa-sifa]

Thank you for the clarification and for planning to add SHA-256 support.

In the meantime, I’ve generated the encodings with Transalg, and I’ll benchmark and compare them against your encoder once it’s ready.

Thanks again!

[nahiyan]

I've found a simple way you can modify Saeed Nejati's encoder to take only the digest through stdin. Simply comment out lines 87-89. Make sure to not set any fixed input bits through the --fix/-F option (by default it's 0, which is what you want). You can also comment out lines 101-106 to remove the functionality of the --fix/-F option altogether.

I've tested for 12 rounds of SHA-256, and it passes the verifier. Remember that this is first preimage (inversion) attack. Let me know if you need a version for second preimage. Just a heads up, I might be rolling out a brand-new encoder in Rust to address all the limitations of the existing encoders.

[twine-lifa-sifa]

Thanks a lot for the clarification and for sharing the modification steps. That’s exactly what I needed — I’m only interested in the first preimage (inversion) case, so this works for my purpose.

By the way, do you know if there’s currently a noticeable difference in speed or efficiency between Nejati’s original encoder and your modified version?

I’ll be looking forward to your new Rust-based encoder with great interest!