International Journal of Electrical and Computer Engineering (IJECE) Vol.
No.
June 2025, pp.
ISSN: 2088-8708.
DOI: 10.
11591/ijece.
Application of satisfiability problem solvers for assessing the strength of hash algorithms Kunbolat Algazy.
Kairat Sakan.
Andrey Varennikov.
Nursulu Kapalova Information Security Laboratory.
Institute of Information and Computational Technologies.
Almaty.
Republic of Kazakhstan Article Info
ABSTRACT
Article history:
This article presents a methodology for assessing the strength of cryptographic algorithms and provides experimental data obtained from studying the cryptographic strength of the developed hash function HBC-256 using modern satisfiability problem (SAT) solvers.
Various SAT solvers implementing the conflict-driven clause learning (CDCL) algorithm, based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, were used to conduct the cryptanalysis of the HBC-256 hash function.
The most effective was the parallel SAT solver Parkissat, and thus it was used for more in-depth research.
A series of experiments were conducted to determine how resistant the HBC-256 hashing algorithm is to preimage attacks for one, two, three, and four rounds.
For this purpose, four sets of files were prepared using special propositional encoding tools, each set including 30 files in the standard of center for discrete mathematics and theoretical computer sciences (DIMACS) format.
These files contain Boolean formulas in conjunctive normal form (CNF), used as input for modern SAT solvers.
To obtain more accurate time measurements, the same experiment was repeated multiple times, after which the average time was The results of this study show that SAT solvers encounter significant difficulties when attempting to solve the preimage search problem for the full-round version of the HBC-256 hash function, even when only 30 bits of the original message are unknown.
Received Jun 11, 2024 Revised Dec 17, 2024 Accepted Jan 16, 2025 Keywords:
Boolean formulas Cryptanalysis Hash function Propositional encoding Satisfiability problem This is an open access article under the CC BY-SA license.
Corresponding Author:
Kairat Sakan Information Security Laboratory.
Institute of Information and Computational Technologies 28 Shevchenko.
Almaty, 050010.
Republic of Kazakhstan Email: 19kairat78@gmail.
INTRODUCTION
Ensuring computer security in large open networks such as the internet is one of the most pressing areas of modern informatics.
However, providing security is a challenging task as it involves addressing numerous technical issues to guarantee the highest possible level of reliability to meet the needs of regular These issues necessitate the use of specific protocols to ensure secure data exchange and modern cryptographic methods.
Even when a protocol has a formal proof of security, it can still be compromised if the cryptographic algorithm used for its implementation possesses undesirable algebraic properties.
Thus, one of the essential steps in creating a cryptographic scheme, algorithm, or protocol is conducting an initial cryptanalysis to assess the strength of the proposed scheme.
Modern methods successfully applied to the analysis of cryptographic algorithms, such as linear cryptanalysis or differential cryptanalysis, rely solely on statistical tools.
Another approach for analyzing cryptographic algorithms to obtain more reliable security guarantees is propositional encoding followed by the application of satisfiability (SAT) solvers .
Many practically significant problems related to Journal homepage: http://ijece.
ISSN: 2088-8708
information management and processing in discrete systems can be effectively reduced to the satisfiability problems of Boolean formulas.
This applies to problems of synthesis and verification in microelectronics, some theoretical programming issues, inversion problems of discrete functions, management of communication protocols, and many others.
A Boolean formula of ycu variables is an expression constructed according to specific rules over an alphabet that includes Boolean variables ycu1 , .
, ycuycu , parentheses, and special symbols that are known as Boolean .
Boolean formulas are also referred to as Aupropositional formulasAy or Auformulas of logic algebra.
Ay There are Boolean formulas presented in a special form known as normal forms.
The primary object of further consideration will be Boolean formulas in conjunctive normal form (CNF) .
Let .
, .
ycu be the set of all words of length ycu over the alphabet .
, .
In several sources, the elements of .
, .
ycu are referred to as Boolean vectors.
Any Boolean formula ya of ycu variables define a completely defined Boolean function yceya : .
, .
ycu Ie .
, .
A formula ya is called satisfiable if there exists an assignment yu OO .
, .
ycu of values to the variables in ya such that yceya .
= 1.
Such an assignment is called a satisfying assignment for ya.
If no such assignment exists, ya is called unsatisfiable.
For any Boolean formula ya, a circuit can be constructed from functional elements over an arbitrary complete basis, for example, {O,A}.
From this circuit, using Tseitin transformations, one can construct a CNF ya.
that is satisfiable if and only if ya is satisfiable.
The formula ya.
is generally a formula with more variables than ya.
However, importantly, the transition from ya to ya.
is performed in polynomial time relative to the length of the binary representation of ya.
Given this, everywhere below, the Boolean satisfiability problem will refer to the problem of satisfiability of any CNF: that is, given an arbitrary CNF ya, the question is to determine whether ya is satisfiable.
SAT is a classical NP-complete problem .
Thus, if ycE O ycAycE, then SAT cannot be solved in polynomial time .
elative to the size of the CNF) in the general case.
Nevertheless, the last 20 years have seen significant progress in the development of SAT-solving algorithms, achieving impressive results on extensive classes of so-called industrial benchmarks .
, .
One of the most important classes of logical equations is formed by equations in the form of CNF=1, where 1 denotes the true value.
The problems of finding solutions to this class of equations belong to the so-called SAT problems.
Special software tools called SAT solvers are used to solve SAT problems.
For some cases.
SAT solvers allow finding a satisfying assignment for the CNF, i.
, a set of variable values that evaluates the CNF to Autrue.
Ay From this assignment, the desired secret key can be efficiently obtained.
This approach is called SAT cryptanalysis.
In the field of cryptanalysis.
SAT solvers can be applied to a variety of tasks .
They are used to search for a key using a ciphertext-only attack, or to search for a key using a known-plaintext attack.
Additionally.
SAT solvers are employed to prove that a cipher is faithful, meaning the same ciphertext cannot be generated using different keys, which implies the absence of a universal key capable of decrypting ciphertext encrypted with any other key.
They also demonstrate that a cipher is not closed, which means that for any two keys, there does not exist a third key such that double encryption with the first two keys is equivalent to encryption with the third key.
Furthermore.
SAT solvers can prove that a cipher does not have weak keys, specifically showing that no keys exist for which double encryption is equivalent to sequential encryption and decryption operations.
Lastly.
SAT solvers are used to evaluate the strength of hashing algorithms by searching for collisions, first or second preimages, and other vulnerabilities.
Scientific studies on the application of SAT solvers for analyzing cryptographic hash functions have demonstrated various approaches and their effectiveness.
These works explore both the theoretical aspects and the practical efficiency of applying SAT solvers in this field.
Researchers have shown how SAT solvers can be utilized to identify vulnerabilities in hash functions, such as finding collisions or pre-images.
Moreover, advancements in SAT solver algorithms have significantly improved their performance, making them a powerful tool for evaluating the security of modern cryptographic hash functions.
In the study .
SAT solvers were used to find collisions in the SHA-256 hash function based on socalled Ausemi-free-startAy collisions.
Authors integrated the programmatic SAT CAS paradigm with differential cryptanalysis methods previously employed in collision attacks on SHA-256.
Although these attacks are still far from finding collisions for the full version of SHA-256, they show progress in applying SAT solvers for analyzing the security of hash functions.
Programmable SAT solvers for cryptanalysis allow the customization of the SAT-solving process for specific cryptographic tasks, making them more flexible and effective for analyzing hash functions .
They enable the consideration of cryptographic operations' characteristics and apply them during the propagation and conflict analysis processes.
The authors enhance the propagation and conflict analysis mechanisms of conflict-driven clause learning (CDCL) solvers by incorporating specialized algorithms tailored to the cryptographic primitives under examination.
This method proves to be highly effective, particularly in the differential path analysis and algebraic fault detection of hash functions.
Preliminary Int J Elec & Comp Eng.
Vol.
No.
June 2025: 3191-3201
Int J Elec & Comp Eng
ISSN: 2088-8708
results highlight the potential of this approach, confirming it as a substantial advancement compared to traditional Blackbox SAT-based cryptanalysis techniques.
Lingeling is a highly optimized SAT solver that has been used successfully in various SAT It has been expanded into two parallel variants: Plingeling and Treengeling.
In study .
, two solvers.
Plingeling and Treengeling, are described, both of which support parallel and distributed computing.
Plingeling divides the task among multiple threads on a single processor, while Treengeling distributes the work across several nodes in a distributed system.
While SAT solvers represent a powerful tool for solving certain classes of problems, their application in cryptography is limited due to the complexity, scale, and specificity of cryptographic tasks.
Successful use of SAT solvers in cryptography requires a deep understanding of both the cryptographic primitives themselves and the methods for transforming these problems into a solvable form for SAT solvers.
The main limitations in applying SAT solvers include aspects such as exponential complexity, excessively large and complex Boolean formulas, and the challenging scalability of simplified versions of cryptographic algorithms to full-round versions.
Overcoming these limitations in solving cryptographic tasks with SAT solvers requires a comprehensive approach, including algorithm optimization, the development of new methods, and the application of various strategies.
One way to overcome these limitations is through the use of parallel computing.
The use of parallel or distributed computing in SAT solvers is especially beneficial when dealing with large formulas, as it allows different parts of the task to be processed simultaneously, significantly improving the efficiency of solving problems.
Based on this, the SAT solver experiments in this research were conducted on the HP Enterprise DL380 Gen10/2 Xeon Gold server.
SAT solvers are powerful tools for evaluating the cryptographic strength of hash functions.
With the continuous growth of computational capabilities, research is ongoing to enhance the efficiency of solvers and adapt them for analyzing modern cryptographic hash functions.
The scientific community explores various approaches and SAT solvers to identify vulnerabilities such as collisions, first-preimage, and secondpreimage attacks.
The essence of this research lies in assessing the cryptographic strength of the newly developed hash function HBC-256 using state-of-the-art SAT solvers, as the development of any hash function must be accompanied by a thorough security analysis, including modeling potential attacks with SAT solvers.
To address this issue, the study conducted a practical cryptanalysis of the cryptographic hash function HBC-256.
A series of experiments were carried out to evaluate the resilience of the HBC-256 hashing algorithm against preimage attacks.
This article presents an evaluation of the performance of parallel and sequential SAT solvers in solving preimage search problems for the HBC-256 hashing algorithm.
The contributions of this work are as follows:
Oe A brief overview of existing methods and approaches for checking the satisfiability of a Boolean function represented in CNF and finding its value set is provided.
Oe A comparative analysis of the effectiveness of the SAT solvers Lingeling.
CaDiCaL.
Kissat.
Plingeling.
Treengeling, and Parkissat is conducted using the HBC-256 hash function as an example.
Oe Using Parkissat, which demonstrated the best results in the comparative analysis, the high cryptographic strength of the HBC-256 hash function is proven.
METHOD
The following methods were employed during the research: .
propositional encoding to transform cryptographic algorithms into Boolean formulas and i.
solution search for the satisfiability problem of Boolean formulas using efficient SAT solvers.
The use of SAT solvers in algebraic cryptanalysis provides a powerful tool for solving complex systems of equations, making this approach particularly effective for analyzing cryptographic systems.
The advantage of algebraic cryptanalysis lies in its versatility, as this approach can be applied to any cipher that can be expressed in algebraic form, including symmetric ciphers, asymmetric schemes, elliptic curve-based schemes, and hash functions, whereas differential and linear cryptanalysis are generally limited to symmetric block ciphers and their effectiveness depends on the specifics of the algorithm.
However, the application of SAT solvers to cryptographic problems requires significant computational resources, limiting their practical use in some cases.
Therefore, in terms of performance and efficiency, the main focus will be on selecting the specific SAT solver.
Propositional encoding to transform cryptographic algorithms into Boolean formulas Since manual encoding is impractical, cryptographic algorithms are typically transformed into Boolean formulas using specialized tools.
These tools enable the expression of cryptographic algorithms in high-level programming languages, followed by the conversion of the resulting program into the corresponding Boolean formula in CNF.
The resulting formula is then saved in a file with the standard DIMACS format, making it compatible for use as input data by modern SAT solvers.
Application of satisfiability problem solvers for assessing the strength of A (Kunbolat Algaz.
A ISSN: 2088-8708 For the preparation of experimental data in this paper, the Transalg software suite was employed as such a tool.
Transalg was developed by the Matrosov Institute for system dynamics and control theory of the Siberian Branch of the Russian Academy of Sciences, located in Irkutsk .
This suite facilitates the conversion of arbitrary algorithms into Boolean formulas.
These algorithms compute everywhere-defined discrete functions, i.
, functions of the form yce: .
, .
O Ie .
, .
O , and are expressed using the specially designed programming language TA akin to C .
Searching for solutions to Boolean formula satisfiability problems using efficient SAT solvers Any Boolean satisfiability problem consists of two key subtasks-checking the satisfiability of an arbitrary Boolean function represented in CNF and finding a set of values for which such a CNF is satisfied.
The foundation of most SAT solvers is the Davis-Putnam-Logemann-Loveland (DPLL) algorithm .
, .
which was specifically proposed for determining the satisfiability of Boolean formulas written in CNF, i.
for solving SAT problems.
The DPLL algorithm serves as the basis for most efficient SAT solvers.
The main idea of the DPLL algorithm is to apply depth-first search methods and utilize the unit propagation rule.
The DPLL algorithm divides the set of variables of the CNF formula into two subsets.
A and B, where subset A contains variables with a value of AutrueAy and subset B contains variables with a value of Aufalse.
Ay At each step, an arbitrary variable from the CNF formula is chosen, and it is assigned a value of AutrueAy .
dding the variable to subset A).
Then the original formula is simplified, and the simplified problem is solved.
If the simplified CNF formula is satisfiable, then the variable value chosen is correct.
the chosen variable is assigned a value of Aufalse,Ay and it is moved to subset B.
The problem is then solved again for the chosen AufalseAy variable value.
Thus, either the correct variable value (AutrueAy or AufalseA.
will be found, or it will be proven that the original formula is unsatisfiable .
, .
The foundation of the vast majority of modern complete SAT solvers, effective on broad classes of practical tests, is the conflict-driven clause learning (CDCL) algorithm.
In turn, this algorithm is based on the DPLL algorithm.
The main difference between these two algorithms is that CDCL uses memory to store search history more precisely, and information about dead-end branches of the search tree is recorded in the form of new constraints, called conflict clauses .
Ae.
This allows for significantly deeper backtracking in some cases than in DPLL.
In addition to conventional or sequential SAT solvers, parallel SAT solvers have gained widespread use.
These solvers are divided into three categories: portfolio solvers, divide-andconquer solvers, and solvers based on parallel local search.
Portfolio solvers are built on the use of multiple algorithms or different configurations of the same All solvers in the parallel portfolio work on different processors to solve the same problem.
If one solver program is completed, the portfolio solver reports whether the problem is satisfiable or unsatisfiable according to that solver.
All other solvers stop working.
Diversifying portfolios by including different solvers, each of which performs well on different types of problems, enhances solver efficiency.
Many solvers use random number generators internally.
Diversifying their initial values .
is a simple way to diversify the portfolio.
Other diversification strategies include enabling, disabling, or diversifying certain heuristics in the sequential solver .
, .
Unlike parallel portfolios, parallel divide-and-conquer solvers attempt to divide the search space among individual instances of SAT solvers running in parallel threads.
However, due to the use of methods such as unit propagation, after partitioning the SAT problem into individual subproblems, they may vary significantly in complexity, leading to the challenging problem of load balancing.
One strategy for parallel local search to solve SAT involves using opposite truth values for one or more variables .
lip variable.
in different nodes of the computing system.
These variables are selected using heuristics that attempt to determine how this change can expedite the SAT problem-solving process by reducing the number of unsatisfied clauses.
Another approach is to apply the aforementioned portfolio approach .
, .
Despite the abundance of SAT solvers of various types available today, a universal solution that performs equally well for all tasks has not yet been found.
Each solver may excel at tasks that others struggle with while performing significantly worse on some other tasks.
It is practically impossible to predict in advance which solver should be used in a given situation, so the choice of solver that best suits solving a particular problem is determined experimentally.
Hash function HBC-256 The cryptographic algorithm chosen for testing using modern SAT solvers was the HBC-256 data hashing algorithm, developed in the Information Security Laboratory of the Institute of Information and Computational Technologies of the Ministry of Science and Higher Education of the Republic of Kazakhstan.
The HBC-256 hash function was built using the Merkle-Damgard construction with the widepipe modification, which is one of the most common modifications.
To ensure one-wayness, the DaviesMeyer scheme was employed.
The algorithm HBC-256 consists of 4 rounds, and the length of the resulting Int J Elec & Comp Eng.
Vol.
No.
June 2025: 3191-3201
Int J Elec & Comp Eng
ISSN: 2088-8708
hash value is 256 bits.
The compression function utilized in this algorithm is based on a proprietary block cipher called CF, which was designed with consideration of requirements for encryption algorithms in software and hardware implementations .
The input and output block lengths of the compression function CF, as well as the round key length, are all 128 bits.
To enhance the performance, the structure of the HBC-256 hashing algorithm is designed to allow the adjustment of the number of input blocks hashed simultaneously in parallel streams.
This number is determined by the parameter k, which ranges from 3 to 8.
The value of parameter k is selected based on the volume of data being hashed and the available computational resources of the computer used.
Thus, the parameter k defines the length L of the input block for the HBC-256 hashing algorithm, where L=128yk bits.
The structure of the hashing algorithm is shown in Figure 1.
The HBC-256 algorithm under consideration, known for its high level of security, enhanced performance, and suitability for hardware implementation using parallel computations, is extensively described in .
This paper provides detailed results of conducted research on avalanche effects, strict avalanche effects, and statistical security.
Additionally, works .
, .
present conclusions on the impracticality of using methods such as differential, linear, and algebraic cryptanalysis to find collisions in the HBC-256 function.
In our case, when preparing experimental data, we used the value k=3.
Thus, the length L of the input block of the algorithm is 384 bits.
Figure 1.
The scheme of the HBC-256 hashing algorithm
RESULTS AND DISCUSSION
The Transalg translator takes as input a program that computes a discrete function, written in a specialized procedural programming language (TA languag.
The result of translating a TA program is a system of Boolean equations that encode the computation process of the considered function.
The phases of text analysis of the TA program, constructing a syntax tree, and traversing the resulting tree for interpretation are implemented in a standard manner.
A non-trivial aspect of the translation is the procedure for interpreting the language constructs, as this step is responsible for generating the system of Boolean equations that encode the algorithm's execution process.
At this stage, numerous local problems arise, the resolution of which can significantly affect both the size and structure of the resulting code.
As mentioned above, the Transalg software suite was used to transform this algorithm into a Boolean formula.
Initially, using the specialized programming language TA, which is part of the Transalg software suite, a program code was written to implement all the operations performed by the algorithm.
These operations include byte permutation, bitwise cyclic shift, substitution procedure using four 16-byte S-boxes, byte-wise XOR operation, and addition of elements from selected rows and columns of the matrix.
Application of satisfiability problem solvers for assessing the strength of A (Kunbolat Algaz.
A ISSN: 2088-8708 Then, the text of this program was passed to the parsing module of the Transalg software suite, the result of which is a syntax tree describing the internal representation of this program.
Traversal of the syntax tree and construction of Boolean equations are performed by the transformation module.
When generating the final propositional code, the transition to CNF is carried out using Tseitin transformations .
As a result of the propositional encoding of the HBC-256 hashing algorithm, a Boolean formula in CNF was obtained, containing 196,864 Boolean variables and consisting of 986,480 clauses, each of which represents a disjunction of literals.
The total number of literals, i.
Boolean variables or their negations, included in these clauses, is 3,321,880.
Table 1 shows the number of Boolean variables, literals, and clauses depending on the number of rounds of the HBC-256 hash function.
Table 1.
Number of Boolean variables, literals, and clauses in the Boolean formula describing the HBC-256 hash function Number of rounds Number of variables 47,232 97,024 146,944 196,864 Number of literals 791,464 1,633,912 2,477,896 3,321,880 Number of clauses 235,024 485,168 735,824 986,480 Once the propositional representation of the HBC-256 hashing algorithm is obtained, depending on the problem being solved, it is necessary to assign values to the input variables, each corresponding to a specific bit of the input block of the hashed message, and the output variables, each corresponding to a specific bit of the hash code.
After that, a series of tests are performed using six modern SAT solvers to obtain information about the computation runtime, memory usage, and other experimental data.
Depending on whether input and/or output variable values are specified.
SAT solvers can solve the following 4 tasks:
If neither input variable values nor output variable values are specified, random input variable values .
nput messag.
are generated, and then the corresponding output variable values .
ash cod.
are If input variable values .
nput messag.
and output variable values .
ash cod.
are specified, the task of hash code verification is solved.
If only input variable values .
nput messag.
are specified, the task of computing the values of the corresponding output variables .
ash cod.
is solved.
If only output variable values .
ash cod.
are specified, the task of computing the values of the corresponding input variables .
nput messag.
is solved.
The first three tasks, from the perspective of SAT solvers, are trivial and can be solved in just a few However, the fourth task .
re-image searc.
, which is of the greatest interest in terms of cryptanalysis, cannot be solved in a reasonable amount of time.
This is natural because any hash function must be resistant to pre-image attacks.
One of the commonly used techniques when employing SAT solvers is Guess-and-Determine, which involves fixing the values of certain variables, significantly reducing the overall time required to find a solution to the cryptanalysis task at hand.
Therefore, we will simplify our task by specifying, in addition to the output variable values .
ash cod.
, the values of certain input variables, and then attempt to find the values of the remaining input variables using a SAT solver.
The computations were performed under the condition that the output variable values, representing a 256-bit hash value, were fully known.
Input variable values representing a 384-bit plaintext block were provided, with ycu initial bits missing, where 1 O ycu O 30.
The task is to find the values of the input variables corresponding to the missing bits using SAT solvers and thereby fully recover the original message block.
For experiments aimed at testing the resilience of the HBC-256 algorithm against this type of attack, three sequential SAT solvers were selected: CaDiCaL .
Lingeling .
, and Kissat .
, along with three parallel SAT solvers: Plingeling .
Treengeling .
, and Parkissat .
, .
These solvers have at various times achieved top rankings in the annual SAT competition.
Table 2 shows the time taken to find the missing bits of the original message using the aforementioned SAT solvers.
As can be seen from this table, it is preferable to use parallel SAT solvers to solve our problem.
Among the parallel SAT solvers .
or our proble.
, the most efficient one was the Parkissat SAT solver, so it will be used in further experiments.
Empty cells in the table indicate that the execution time exceeded the established limit.
Now, we will conduct a series of experiments to determine the resistance of the HBC-256 hashing algorithm to preimage attacks using one, two, three, and four rounds of the hashing function.
Table 3 presents the solution search time using the Parkissat SAT solver, and Figure 2 shows the dynamics of this time depending on the number of unknown variables for four rounds.
Int J Elec & Comp Eng.
Vol.
No.
June 2025: 3191-3201
Int J Elec & Comp Eng
ISSN: 2088-8708
Table 2.
Time to find the specified number of plaintext bits .
n second.
Number of unknown bits .
CaDiCaL SAT Solvers Sequential Lingeling Kissat Parkissat Parallel Plingeling Treengeling Table 3.
Solution search time using the Parkissat SAT solver .
n second.
Number of unknown bits .
1 round 1,632.
2,489.
4,997.
19,304.
52,062.
Solution search time 2 rounds 3 rounds 1,257.
1,329.
1,100.
3,848.
2,038.
6,278.
4,269.
20,488.
9,984.
76,047.
27,842.
87,101.
63,398.
35 174,276.
4 rounds Application of satisfiability problem solvers for assessing the strength of A (Kunbolat Algaz.
A ISSN: 2088-8708 It is necessary to note the following nuance.
When running the same SAT solver multiple times with the same input and output data, we obtain different times each time.
This is because, at each step of the algorithm for solving the Boolean equation, the selection of the next variable for subsequent assignment of the value AutrueAy or AufalseAy is made using a random number generator.
If the variable is AuluckilyAy chosen, meaning the value chosen for it is part of the solution, this positively affects the search time.
Otherwise, it will be necessary to return to this variable and assign it the opposite value, and then repeat the solution search procedure .
backtracking mechanis.
For example, searching for the values of 25 unknown variables using the Parkissat SAT solver can take from 49 minutes to 15 hours, where they are shown in Table 4.
To obtain a realistic assessment of time, it is necessary to repeat the same experiment multiple times, for example, 10 times, and then find the average time spent.
In our case, the average time to find a solution was 23,361.
06 seconds, or 6 hours, 29 minutes, and 21.
06 seconds.
As evident from Table 3 and the graph in Figure 2, with an increase in the number of unknown bits .
tarting from 25 and abov.
, the time required to solve the problem sharply increases.
It took over 87 hours using a computer with two 56-core processors to find the preimage of the message, assuming that 30 unknown bits were present while the values of the remaining 354 bits were fixed.
The experiments were conducted on a computer with two 56-core AMD EPYC 7663 processors running at 2.
0 GHz each .
otal of 112 core.
and 128 GB of RAM, operating on the Linux Ubuntu 22.
3 LTS operating system.
Figure 2.
Dynamics of solution search time using the Parkissat SAT solver Table 4.
Search time for values of 25 unknown Boolean variables Attempt number Attempt #1 Attempt #2 Attempt #3 Attempt #4 Attempt #5 Attempt #6 Attempt #7 Attempt #8 Attempt #9 Attempt #10 Search time .
, m, .
2 h 52 m 21.
5 h 22 m 00.
2 h 35 m 51.
7 h 39 m 49.
49 m 30.
1 h 56 m 12.
15 h 08 m 07.
13 h 52 m 30.
3 h 25 m 15.
11 h 11 m 50.
10,341.
19,320.
9,351.
27,589.
2,970.
6,972.
54,487.
49,950.
12,315.
40,310.
CONCLUSION
The study undertook a practical cryptanalysis of the cryptographic hash function HBC-256.
The 4-round compression function was described in the form of an equation in CNF=1 format using 986,480 clauses, each of which represents a conjunction of literals and 196,864 Boolean variables.
The solution to this equation was obtained using the SAT solver Parkissat.
The results of the experimental studies show that for the full HBC-256 hash function consisting of 4 rounds, the SAT solver struggles to solve the problem even when only 30 bits of the original message are Since finding the preimage requires determining all 384 bits of the original message block, this task is practically infeasible within a reasonable time frame.
Therefore, it can be concluded that the HBC-256 algorithm is resistant to preimage attacks using this method.
Int J Elec & Comp Eng.
Vol.
No.
June 2025: 3191-3201
Int J Elec & Comp Eng
ISSN: 2088-8708
A limitation of SAT solvers is their brute-force nature, and the problem of reducing the search space is fundamental to these methods.
A solution might not be found within an acceptable time frame, making it practically impossible to provide a theoretical estimate of the possibility of finding a preimage.
Therefore, as a future research direction, it should be noted that other types of cryptanalyses and their combinations, including the combination of differential and algebraic cryptanalysis, will be explored to obtain a theoretical estimate of the strength of the considered hash function.
FUNDING INFORMATION
The research work was funded by the Ministry of Science and Higher Education of Kazakhstan and carried out within the framework of the project BR24993052 AuDevelopment and study of cryptographic algorithms for information protection in resource-constrained systems and evaluation of their strengthAy at the Institute of Information and Computational Technologies.
AUTHOR CONTRIBUTIONS STATEMENT
This journal uses the Contributor Roles Taxonomy (CRediT) to recognize individual author contributions, reduce authorship disputes, and facilitate collaboration.
Name of Author Kunbolat Algazy Kairat Sakan Andrey Varennikov Nursulu Kapalova C : Conceptualization M : Methodology So : Software Va : Validation Fo : Formal analysis ue ue ue ue ue ue ue ue ue ue ue I : Investigation R : Resources D : Data Curation O : Writing - Original Draft E : Writing - Review & Editing ue ue ue ue ue ue ue ue ue ue ue Vi : Visualization Su : Supervision P : Project administration Fu : Funding acquisition CONFLICT OF INTEREST STATEMENT Authors state no conflict of interest.
DATA AVAILABILITY
Oe The data that support the findings of this study are available on request from the corresponding author.
KS.
Oe Derived data supporting the findings of this study are available from the corresponding author.
KS, on Oe The data that support the findings of this study are available from the corresponding author.
KS, upon reasonable request.
REFERENCES