This work presents an experimental investigation on the performance diferences among various SMT solvers in generating diferential cryptanalysis collisions for the SHA-2 family of cryptographic hash functions, a widely adopted hash function, critical for maintaining data integrity and security of protocols like TLS. The research involved examining diferent parameters with these solvers, and their efects on the overall solving performance. These findings provide both a methodological baseline and actionable insights regarding solver efectiveness tailored towards helping shape future research in automated cryptanalysis.
RQ1 How does SMT solver choice influence SHA-256 performance 1? RQ2 Which SMT solver parameters afect SHA-256 performance most? RQ3 How do diferential cryptanalysis encodings impact SHA-256 collisions?
In Section 2, we describe SHA-256 and previous work on diferential cryptanalysis using automated reasoning tools. Building on this foundation, Section 3 presents a series of experiments and methodologies for investigating the research questions given above. Finally, Section 4 analyses the results of our experiments.
2.1. SHA-2 We will use ≫ to denote right roll by a constant, ⊕ to denote Exclusive Or (XOR) and + represents modulo addition (respectively rotate_right, bvxor and bvadd in SMT-LIB).
The SHA-2 family, designed by the National Security Agency (NSA) in 1995, standardised by NIST in
2001, comprises of six primary hash functions: SHA-224, SHA-256, SHA-384, SHA-512, SHA-512/224,
and SHA-512/256. These algorithms employ the Merkle–Damgård construction with a Davies–Meyer
compression function, difering primarily in digest size (224 to 512 bits), initial values, and round counts
(64 for SHA-256, 80 for SHA-512) [
The SHA-2 algorithm processes input through a series of deterministic transformations governed by its Merkle–Damgård structure.
Message Processing Input messages undergo a pre-processing step to conform to the 512-bit block for SHA-256 (1024-bit block for SHA-512 respectively). This step is necessary only when converting an input message to a digest. However, this step is irrelevant for automated reasoning tools like SMTs, which directly use arbitrary message blocks to reason about values.
functions are defined as:
Each SHA-2 hash function uses its own set of constants for functions. SHA-256 0() = ( ≫ 7) ⊕ ( ≫ 18) ⊕ ( ≫ 3) 1() = ( ≫ 17) ⊕ ( ≫ 19) ⊕ ( ≫ 10) Σ0() = ( ≫ 2) ⊕ ( ≫ 13) ⊕ ( ≫ 22) Σ1() = ( ≫ 6) ⊕ ( ≫ 11) ⊕ ( ≫ 25) Maj (, , ) = ( ∧ ) ⊕ ( ∧ ) ⊕ ( ∧ )
Ch(, , ) = ( ∧ ) ⊕ (¬ ∧ ) Message Expansion The pre-processed message makes up words , for 0 ≤ ≤ 15. Remaining words, 16 ≤ ≤ 63, are expanded using = − 16 + 0(− 15) + − 7 + 1(− 2). 1Better performance refers to reduced solving time and improved round solvability. Constants and Initialisation Each hash function part of the SHA-2 family uses diferent H-constants, also known as the initialisation vector (IV). These serve as the initial digest values when starting the compression function. SHA-256 uses fractional parts of square roots from the first 8 primes, whereas SHA-512 uses cube roots. The round constants, also known as K-constants, are derived from fractional parts of cube roots for the first 64 primes (SHA-256) or first 80 primes (SHA-512). These aim to break symmetry in message scheduling during modular addition of the compression function. Compression Function Each H-constant updates one of eight 32-bit registers –ℎ, often referred as the working variables, which are part of the 256-bit starting state. The compression function employs 64 rounds (80 for SHA-512), where for each round, the following are executed: 1 = ℎ + Σ1() + Ch(, , ) + + 2 = Σ0() + Maj (, , ) ℎ = ; = ; = ; = + 1 = ; = ; = ; = 1 + 2
What is often referred to as a round-reduced model, is simply a compression with less iterations, also knowns as steps or simply rounds, than standard. For round-reduced models, a lot of K-constants and expanded messages are irrelevant for obtaining the digest.
Finalisation After processing all blocks, the final digest concatenates the eight registers’ contents. Truncated variants trim the output size. For SHA-256, this produces a 64-character hexadecimal value.
A cryptographic collision occurs when distinct inputs ̸= ′ yield identical digests ( ) = ( ′).
As described in [
Collisions can be divided into three categories based on the IV used: • Free-Start Collisions (FS): Attacker controls both message blocks and IVs. A collision occurs when either the message or IV are unique. demonstrated a weakness in the compression function, showing round structure vulnerabilities. • Semi-Free-Start Collisions (SFS): Attacker chooses a fixed IV for both messages, while controlling the message blocks. A middle-ground between FS and STD, demonstrating significant structural weaknesses. • Classical/Standard Collisions (STD): Attacker controls only the message blocks. The NIST provided IV is used. Completely breaks collision resistance properties, deeming the hash function cryptographically insecure.
Standard collision is always unsatisfiable (UNSAT) for the first 8 rounds. This is likely due to choice of constants, creating infeasible conditions for a collision.
SHA-256 SHA-512
STD FS SFS SFS STD STD FS SFS
A SAT + CAS approach was used in [
A direct attack targetting OpenWRT’s use of SHA-256 was described in [
There have been attempts to make a GPU accelerated SAT solver [
A wider variety of of cryptanalysis tools, including SAT, SMT, MILP and CP were applied to multiple
ciphers, permutations and hash functions in [
No research has previously defined the baseline of what SMT solvers are capable for SHA-2 collisions. It is likely that researchers utilising reasoning tools, like SAT or SMT solvers, were only getting a few rounds, taking this as an implied hard limit without the use of sophisticated encodings. This creates the basis for RQ1 and RQ2, which aims to fill this knowledge gap.
We have written a custom benchmark generator which creates SMT-LIB files modelling a pair of SHA256 or SHA-224 instances running a configurable number of rounds. The initialisation values can be configured for standard, free-start or semi-free start.
All satisfiable instances were verified using our SHA-2 implementation, which is known-good against standard known values.
To investigate RQ1 we aimed to use an exhaustive list of currently available SMT solvers. These
include: Z3 version 4.13.4 [
Only the most promising SMT solver, Bitwuzla, was benchmarked with diferent parameters related to theory of BitVectors, rewriting, solver backends.
Simplifying Compression Functions The non-linear Ch and Maj functions, described in Section 2.1 can be simplified, while preserving the logical output, by replacing XOR operations with OR: Ch(, , ) = ( ∧ ) ∨ (¬ ∧ )
Maj (, , ) = ( ∧ ) ∨ ( ∧ ) ∨ ( ∧ )
Alternative Bitwise Addition Encodings of bvadd in solvers tend to be optimised for propagation
and space [
2) bitadd-2(, ) = 0 ⊕ (ℎ ≪
bitadd-(1, . . . , ) = bitadd-2(⨁︁ ≪ =1 2)) 1)
⋁︁ 1≤ <≤ ( ∧ )) This hierarchical structure, in theory, enables (log ) carry propagation, though practical SMT contraints necessitated sequential left-to-right chaining for multi-operand cases.
Diferential Encoding In order to move to a diferential cryptanalysis reasoning model, diferentials have been defined between corresponding pairs of computation values in the two SHA-2 instances. These encodings include Delta Subtraction (DSub) Δ− = − ′, and Delta Exclusive Or (DXOR) Δ⊕ = ⊕ ′.
Both encodings were systematically applied to message block diferences during expansion, working variables (–ℎ) in the compression function, round specific constants ( ), and final digests. Base assertions on absolute values have been converted to assert on diferential values, but otherwise no additional assertions have been used. All the underlying absolute values were still present and calculated for each variable to ensure compliance with the SHA-2 definition.
All code was written in Rust (rustc version 1.85.1) [
A dedicated X86_64 machine was set up, with a fresh installation of NixOS 25.05 (Warbler), utilising the Linux Realtime 6.6.77-rt50 kernel. For hardware, the machine consisted of an AMD Ryzen 9 5900X processor, paired with 4x32GiB DDR4 memory sticks. The BIOS was configured with CPU Clock 37.00, CPU Clock Control 100.000 MHz, DDR4-3600 18-22-22-52-64-1.35V, CPU VCore 0.818V, CPU VCore Loadline Calibration LOW, CSM Support ENABLED. This runner can be rebuilt at any time, using the NixOS configuration: https://github.com/Supermarcel10/NixOSConfig/ blob/f1d26ec/devices/E01/configuration.nix.
This section presents highlights of our experimental results. Outputs deemed invalid by our known-good SHA-2 implementation, or resulting in an error code, have been excluded from plots. One example of this is Colibi2, which failed to meet SMTLIB constraints. For an exhaustive set of results, please refer to Appendix B. All raw results are available in the codebase, described in Section 3.2.
Two diferent visualisation layouts are used to address the research questions.
Comparison Graph These provide a side-by-side comparison of each solver’s performance as lines on a 2D plot. The rounds are displayed on the X-axis and log 2 time on the Y-axis. Results that time out are set to the maximum possible time. The line that goes the most to the right (more rounds), while staying low (less time) is the best. Additionally, the consistency and linearity of the line provides insight about the reasoning of the problem. This graph is used to answer RQ1 in Subsection 4.1. Baseline Graph The baseline graph was designed to compare between diferent runs of the same solver with parameters and encodings. It is a 2D line graph with the baseline in the middle. Any missing or invalid data is skipped from plotting. Deviation data is then calculated from the baseline based on time diference, and represented as a percentage.
If no plot exists on baseline, but a valid deviation is plotted, +∞ will be used as the deviation value. This can be interpreted as “This was infinitely faster than the nothing achieved (on baseline) within timeout”. If a baseline exists, but no deviation for that round is present, the plot will be skipped.
A rough run-to-run variance is shown with a grey colour near the middle. The green area with − % implies “this took % less time, compared to baseline”. Similarly, the red area with +% implies “this took % more time, compared to baseline”.
The graph scales with the results, and tops out at 100% in both directions. When a result is plotted on the edge of the graph, the deviation is ≥ 100% (i.e. twice as long or half as long). This graph is used to visualise results for RQ2 and RQ3 in Subsection 4.1.
SHA256 STD Solver Comparison
Figure 1 helps answer RQ1 and showcases interesting aspects of SMT solver choice. No solver could ifnd a collision for 5 rounds, although subsequent rounds terminated with their respective outcomes. We believe this could be misleading; the common approach to using automated reasoning tools of “increasing the rounds until you get a timeout” could cause incorrect conclusions.
Bitwuzla was the most consistent SMT solver, being the only one capable of proving non-existence of a collision for 7 and 8 rounds. This could suggests that Bitwuzla may have stronger capabilities for UNSAT formulas as opposed to its competitors.
As most solvers struggled with higher-round collisions, Bitwuzla and MathSAT were capable of pushing through and delivering 18 and 17 rounds respectively. Bitwuzla is the definitive winner, being both more consistent and able to deliver the most rounds within the timeout period. This means Bitwuzla is the baseline SMT solver to beat.
With a 10 hour timeout, no collisions were found for 19 rounds using Bitwuzla.
Bitwuzla SHA256 STD: Rewrite Level Args +100% +80% +60% +40% +20% ) vTeed +(%0% m i -20% -40% -60% -80%
To answer RQ2, we tried an exhaustive list of parameters available on the most promising SMT solver, Bitwuzla. Figures 2 and 3 signified that adjusting Bitwuzla’s parameters can impact performance both positively and negatively. Despite this, collision performance did not improve.
Setting the rewrite level to 0 or disabling variable-subst provided a positive performance uplift for short-running collisions but hindered long-running ones.
The Kissat SAT solver backend outperformed the baseline (CaDiCaL) in short-running rounds, but may perform worse in longer-running collisions, as implied by the upwards trend near the right edge of Figure 4.
Enabling Bitwuzla’s propagation-based local search engine (--bv-solver prop) negated performance gains, highlighting the performance advantage likely stems from an optimized bit-blasting strategy compared to other solvers.
Enabling multithreading via CryptoMiniSat improved overall performance, though increasing threads beyond four (the lowest tested) led to diminishing returns. This is likely caused by practical trade-ofs related to SMT parallelism and SMT solver memory characteristics. Bitwuzla SHA256 STD: Preprocessing Args - no-pp-embedded - no-pp-flatten-and - no-pp-normalize - no-pp-skeleton-preproc - no-pp-variable-subst - no-pp-variable-subst-norm-eq - pp-contr-ands - pp-elim-extracts - pp-variable-subst-norm-bv-ineq - pp-variable-subst-norm-diseq Baseline 16
To answer RQ3, all combinations of diferential cryptanalysis encodings presented in Section 3.1 have been benchmarked. These can be seen in Figure 5 and Figure 6.
While there were no improvements in the last round computable, this data gives a clearer direction for future work.
The delta subtract encoding, did not allow the solver to reason more freely as expected, and performed within margin of error. It did help influence the solvability of round 5, where previously no result was found within the timeout period.
The delta XOR encoding proved more meaningful, especially in short-running collisions. It is unclear if delta XOR provides benefits for long-running collisions, but seems more promising than delta subtract.
As for the alternative bitwise add, it performed worse for solving time. Despite this, improved linearity for some output cases has been observed. Listings 2 and 1 showcases less altered bits, This implies the SMT solver has taken a diferent direction, reasoning more about reducing these diferenes.
Maj and Ch simplification had minor efects, but did not paint a clear enough picutre for a conclusive answer.
In combination with more powerful diferential cryptanalysis encodings, it is possible the presented encodings could be help in other aspects.
The graphs answer RQ1: Bitwuzla [
It is plausible that an alternative set of parameters could improve other solvers’ performance, such as MathSAT, leaving RQ2 partially unanswered. It is conclusive that default parameters for Bitwuzla are the most stable for round solvability and solving time.
In order to answer RQ3, this work analysed basic encodings to provide insights. Diferential cryptanalysis by subtraction simply does not work for SHA-256.
Bitwuzla SHA256 STD: SAT Solver Args 2 4 6
Bitwuzla SHA256 STD: Delta XOR Encoding Comparison 2 4 6
Bitwuzla SHA256 STD: Delta Sub Encoding Comparison
Generating a brute-force approach modelling the SHA-2 standard proved inefective, but performed significantly better than previous literature would imply. By identifying the most promising SMT solver, this work established a recommended SMT solver choice and a baseline claim to beat for future research.
[
Encoding Based Work Encodings described in [
SMT Parameter Exploration Work Further exploration into parameter performance efects could be assessed. Other promising SMT solvers, such as MathSAT, could outperform Bitwuzla with the right choice of parameters.
Hardware Based Work Hardware choice has not been directly benchmarked towards solving
performance. A performance comparison of diferent processors would paint a clearer picture and
recommendation on choice towards better solving performance. For example, an AMD Ryzen 7 9800X3D [
The author(s) have not employed any Generative AI tools. MarcelBarlik,MartinBrain .
X 6 e 5 T 2 a a L h in s 8 F n
o T i U t d c li n a u v f n i h g s ien ha b o t e u la d z d u e w p t a i c s b e n r e e e b v s l a o h n s-- uer o i t t a o ark e:: 943 t n 6 7 e 3 ? ? 7 5 d d fe4 97b lia lia b b V V 3 7 ( ( 9 9 1 9 a a 1 1 4 8 5 5 d d d 4 f f c c 1 9 0 0 0 0 3 d 7 7 e e e 0 6 6 b b 8 6 5 5 5 5 a 8 a a b b c 3 3 3 a a e 4 e e 9 9 6 3 2 2 d d 4 4 7 7 3 3 0 0 5 5 ark e:: 100 f f 5 8 0 0 8 8 2 3 0 0 1 1 2 3 b b 2^8 2^6 2^4 )2^2 i(sTe m 2^0 2^-2 2^-4 2^-6
Expanding on the graphs mentioned in Section 4, an additional graph is used.
Detailed Graph Unlike other graphs, only a single benchmark run is plotted in this graph. It utilises a pair of 2D coordinate systems, where the first line graph relates to time taken in log 2, and the second to memory usage in Mibibytes (MiB). Since SMT solving prefers more locality in memory hierarchy, this graph can help understand if the performance degradation is due to hardware limitations, such as saturating all CPU L3 cache. This graph is used to visualise data in Appendix B.
SHA224 FS Solver Comparison
SHA224 SFS Solver Comparison 2 4 6 8
SHA224 STD Solver Comparison 2^8 2^6 2^4 2^2 )(sTe m i 2^0 2^-2 2^-4 2^-6 2^-8 2^9 2^7 2^5 2^3 i)(se2^1 m T 2^-1 2^-3 2^-5 2^-7
SHA256 FS Solver Comparison 2 4 6 8
SHA256 SFS Solver Comparison 2^9 2^7 2^5 2^3 ()sTe m i 2^1 2^-1 2^-3 2^-5 2^8 2^6 2^4 2^2 ()sTe m i 2^0 2^-2 2^-4 2^-6 2^-8 Com1p0ressionRounds 12 2 4 6 8 14 16 18 20
SHA256 STD Solver Comparison 2^8 2^6 2^4 2^-4 2^-6 2^-8 +100% +0% -20% -40%
Bitwuzla SHA256 STD: Abstraction Args 2 4 6 ) ved +(%0% Te m i -5% -10% 2 4 6 Bitwuzla SHA256 STD: Propagation Args 4 8 CompressionRo1u0nds 14 --no-prop-const-bits --no-prop-ineq-bounds --no-prop-sext Baseline 16
Bitwuzla SHA256 STD: Rewrite Level Args +100% -20% -40% -60% -80%
Bitwuzla SHA256 STD: SAT Solver Args
Bitwuzla SHA256 STD: Solver Engine Args +15% +10% ) ved % ( +Te5% m i 2^11 2^9 2^7 2^5 )(sTe2^3 m i 2^1 2^-1 2^-3 2^-5 2^-7 2 4 6 bitwuzla; Memory & Time vs Rounds 150.0
M i)(ryeo m M
B
Bitwuzla SHA256 STD: Bruteforce Encoding Comparison +100% -20% -40% -60% -80% 2 4 6
Bitwuzla SHA256 STD: Delta XOR Encoding Comparison 2 4 6
Bitwuzla SHA256 STD: Delta Sub Encoding Comparison 12 18