text: In the present paper we describe the technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis instances are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. Therefore, in the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Based on these principles we describe the Transalg software system, developed with SAT-based cryptanalysis specifics in mind. We show the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We also compare the functional capabilities of the proposed system with that of other software systems that can be used to reduce cryptanalysis instances to SAT, and also with the CBMC system widely employed in symbolic verification. In the paper we also present vast experimental data, obtained using the SAT-solvers that took first places at the SAT-competitions in the recent several years.
  @cite_61: In logical cryptanalysis a problem of search of a secret key of a cryptographic system is formulated as a SAT problem, i.e. a problem of search of a satisfying assignment for some CNF. In this paper we consider some natural strategies for parallelization of these SAT problems. We apply coarse-grained approach which makes it possible to use distributed computing environments with slow interconnect. The main practical result of this paper is successful logical cryptanalysis of keystream generator A5 1 in BNB-Grid system.
  @cite_14: In this paper, we propose an algorithm for constructing guess-and-determine attacks on keystream generators and apply it to the cryptanalysis of the alternating step generator (ASG) and two its modifications (MASG and MASG0). In a guess-and-determine attack, we first “guess” some part of an initial state and then apply some procedure to determine, if the guess was correct and we can use the guessed information to solve the problem, thus performing an exhaustive search over all possible assignments of bits forming a chosen part of an initial state. We propose to use in the “determine” part the algorithms for solving Boolean satisfiability problem (SAT). It allows us to consider sets of bits with nontrivial structure. For each such set it is possible to estimate the runtime of a corresponding guess-and-determine attack via the Monte-Carlo method, so we can search for a set of bits yielding the best attack via a black-box optimization algorithm augmented with several SAT-specific features. We constructed and implemented such attacks on ASG, MASG, and MASG0 to prove that the constructed runtime estimations are reliable. We show, that the constructed attacks are better than the trivial ones, which imply exhaustive search over all possible states of the control register, and present the results of experiments on cryptanalysis of ASG and MASG MASG0 with total registers length of 72 and 96, which have not been previously published in the literature.
  @cite_92: In this paper we propose an approach for constructing partitionings of hard variants of the Boolean satisfiability problem (SAT). Such partitionings can be used for solving corresponding SAT instances in parallel. For the same SAT instance one can construct different partitionings, each of them is a set of simplified versions of the original SAT instance. The effectiveness of an arbitrary partitioning is determined by the total time of solving of all SAT instances from it. We suggest the approach, based on the Monte Carlo method, for estimating time of processing of an arbitrary partitioning. With each partitioning we associate a point in the special finite search space. The estimation of effectiveness of the particular partitioning is the value of predictive function in the corresponding point of this space. The problem of search for an effective partitioning can be formulated as a problem of optimization of the predictive function. We use metaheuristic algorithms (simulated annealing and tabu search) to move from point to point in the search space. In our computational experiments we found partitionings for SAT instances encoding problems of inversion of some cryptographic functions. Several of these SAT instances with realistic predicted solving time were successfully solved on a computing cluster and in the volunteer computing project SAT@home. The solving time agrees well with estimations obtained by the proposed method.
  @cite_29: 
  @cite_96: Bivium is a reduced version of the stream cipher Trivium. In this paper we investigate how fast a key recovery attack on Bivium using Grobner bases is. First we explain the attack scenario and the cryptographic background. Then we identify the factors that have impact on the computation time and show how to optimise them. As a side effect these experiments benchmark several Grobner basis implementations. The optimised version of the Grobner attack has an expected running time of 239.12 s, beating the attack time of our previous SAT solver attack by a factor of more than 330. Furthermore this approach is faster than an attack based on BDDs, an exhaustive key search, a generic time-memory trade-off attack and a guess-and-determine strategy.
  @cite_89: In this paper we present experimental results of an application of SAT solvers in current cryptography. Trivium is a very promising stream cipher candidate in the final phase of the eSTREAM project. We use the fastest industrial SAT solvers to attack a reduced version of Trivium - called Bivium. Our experimental attack time using the SAT solver is the best attack time that we are aware of, it is faster than the following attacks: exhaustive search, a BDD based attack, a graph theoretic approach and an attack based on Grobner bases. The attack recovers the internal state of the cipher by first setting up an equation system describing the internal state, then transforming it into CNF and then solving it. When one implements this attack, several questions have to be answered and several parameters have to be optimised.
  @cite_24: Cryptography ensures the confidentiality and authenticity of information but often relies on unproven assumptions. SAT solvers are a powerful tool to test the hardness of certain problems and have successfully been used to test hardness assumptions. This paper extends a SAT solver to efficiently work on cryptographic problems. The paper further illustrates how SAT solvers process cryptographic functions using automatically generated visualizations, introduces techniques for simplifying the solving process by modifying cipher representations, and demonstrates the feasibility of the approach by solving three stream ciphers. To optimize a SAT solver for cryptographic problems, we extended the solver's input language to support the XOR operation that is common in cryptography. To better understand the inner workings of the adapted solver and to identify bottlenecks, we visualize its execution. Finally, to improve the solving time significantly, we remove these bottlenecks by altering the function representation and by pre-parsing the resulting system of equations. The main contribution of this paper is a new approach to solving cryptographic problems by adapting both the problem description and the solver synchronously instead of tweaking just one of them. Using these techniques, we were able to solve a well-researched stream cipher 26 times faster than was previously possible.
  @cite_23: In this paper, we propose a new stream cipher construction based on block cipher design principles. The main idea is to replace the building blocks used in block ciphers by equivalent stream cipher components. In order to illustrate this approach, we construct a very simple synchronous stream cipher which provides a lot of flexibility for hardware implementations, and seems to have a number of desirable cryptographic properties.
  @cite_124: Cryptanalysis of ciphers usually involves massive computations. The security parameters of cryptographic algorithms are commonly chosen so that attacks are infeasible with available computing resources. Thus, in the absence of mathematical breakthroughs to a cryptanalytical problem, a promising way for tackling the computations involved is to build special-purpose hardware exhibiting a (much) better performance-cost ratio than off-the-shelf computers. This contribution presents a variety of cryptanalytical applications utilizing the cost-optimized parallel code breaker (COPACOBANA) machine, which is a high-performance low-cost cluster consisting of 120 field-programmable gate arrays (FPGAs). COPACOBANA appears to be the only such reconfigurable parallel FPGA machine optimized for code breaking tasks reported in the open literature. Depending on the actual algorithm, the parallel hardware architecture can outperform conventional computers by several orders of magnitude. In this work, we focus on novel implementations of cryptanalytical algorithms, utilizing the impressive computational power of COPACOBANA. We describe various exhaustive key search attacks on symmetric ciphers and demonstrate an attack on a security mechanism employed in the electronic passport (e-passport). Furthermore, we describe time-memory trade-off techniques that can, e.g., be used for attacking the popular A5 1 algorithm used in GSM voice encryption. In addition, we introduce efficient implementations of more complex cryptanalysis on asymmetric cryptosystems, e.g., elliptic curve cryptosystems (ECCs) and number cofactorization for RSA. Even though breaking RSA or elliptic curves with parameter lengths used in most practical applications is out of reach with COPACOBANA, our attacks on algorithms with artificially short bit lengths allow us to extrapolate more reliable security estimates for real-world bit lengths. This is particularly useful for deriving estimates about the longevity of asymmetric key lengths.
  @cite_10: Many practically important combinatorial problems can be efficiently reduced to a problem of Boolean satisfiability (SAT). Therefore, the implementation of distributed algorithms for solving SAT problems is of great importance. In this article we describe a technology for organizing desktop grid, which is meant for solving SAT problems. This technology was implemented in the form of a volunteer computing project SAT@home based on a popular BOINC platform.
  @cite_66: 
  @cite_12: 
summary: As we mentioned above, SAT-based cryptanalysis is still actively developing. The cryptographic attacks that employ SAT-solvers show very good results for a number of keystream generators: Geffe, Wolfram (present paper), Crypto-1, Hitag2 (see @cite_24 ). In @cite_61 there was described a successful SAT-based attack on the widely known A5 1 cryptographic keystream generator, which has been used in GSM networks to cipher traffic. Later several dozen cryptanalysis instances for this cipher were solved in the SAT@home volunteer computing project @cite_10 . This result together with other attacks on A5 1 (see @cite_66 @cite_124 @cite_12 ) provides an exhaustive argument towards not using A5 1 any more. The Bivium keystream cipher @cite_23 is a popular object of algebraic and SAT-based cryptanalysis @cite_29 @cite_89 @cite_24 @cite_96 . In @cite_92 there was constructed a SAT-based guess-and-determine attack on Bivium the estimated runtime of which is realistic for modern distributed computing systems. In @cite_14 there were described SAT-based guess-and-determine attacks on several variants of the alternating step generator.