Propositional satisfiability (SAT) is at the nucleus of state-of-the-art approaches to a variety computationally hard problems, one which cryptanalysis. Moreover, number practical applications SAT can only be tackled efficiently by identifying and exploiting subset formula's variables called backdoor set (or simply backdoors). This paper proposes new class sets for used in context cryptographic attacks, namely guess-and-determine attacks. The idea identify best subject statistically...

Many industrial verification problems are solved via reduction to CircuitSAT. It is often the case that resulting SAT instances very hard and require use of parallel computing be in reasonable time. The particularly relevant problem this context how best plan resources, because solvers' runtime well known predict. In present paper we propose two methods employ knowledge about a circuit's structure partition CircuitSAT instance into specific number simpler subproblems. A distinctive feature...

In this paper we propose the technology for constructing propositional encodings of discrete functions. It is aimed at solving inversion problems considered functions using state-of-the-art SAT solvers. We implemented in form software system called Transalg, and used it to construct a number cryptanalysis problems. By applying solvers these managed invert several cryptographic particular, produced by Transalg family two-block MD5 collisions which first 10 bytes are zeros. Also encoding...

In this paper, we propose an approach for modeling and analysis of a number phenomena collective behavior. By collectives mean multi-agent systems that transition from one state to another at discrete moments time. The behavior member (agent) is called conforming if the opinion agent current time moment conforms some other agents previous moment. We presume each every makes decision by choosing set {0,1} (where 1-decision corresponds action 0-decision inaction). our model with synchronous...

In this paper we considered the problem of finding pairs mutually orthogonal diagonal Latin squares order 10. First reduced it to Boolean satisfiability problem. The obtained instance is very hard, therefore decomposed into a family subproblems. To solve latter used volunteer computing project SAT@home. course 10-month long computational experiment managed find 29 described kind, that are different from already known pairs. Also search for triples 10 satisfy weakened orthogonality condition....

Abstract In this research, the study concerns around several features of diagonal Latin squares (DLSs) small order. Authors suggest an algorithm for computing minimal and maximal numbers transversals DLSs. According to algorithm, all DLSs a particular order are generated, each square its constructed. The was implemented applied at most 7 on personal computer. experiment 8 performed in volunteer project Gerasim@home. addition, problem finding pairs orthogonal 10 considered reduced Boolean...

Solving hard instances of the Boolean satisfiability problem (SAT) in practice is an interestingly nontrivial area. The heuristic nature SAT solvers makes it impossible to know advance how long will take solve any particular instance. One way coping with this disadvantage Divide-and-Conquer approach when original instance decomposed into a set simpler subproblems. However, plays crucial role resulting effectiveness solving. In present study, we reduce choosing proper decomposition stochastic...

Abstract The A5/1 keystream generator is a part of Global System for Mobile Communications (GSM) protocol, employed in cellular networks all over the world. Its cryptographic resistance was extensively analyzed dozens papers. However, almost corresponding methods either employ specific hardware or require an extensive preprocessing stage and significant amounts memory. In present study, bitslice variant Anderson’s Attack on implemented. It requires very little computer memory no...

In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language.Translation of such is based on propositional encoding methods formal computing models and concept symbolic execution.We used system make number cryptographic functions.

In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced SAT such way that it should be perceived as natural by cryptographic community. In~the theoretical part paper justify main principles general reduction from class containing majority employed cryptography. Then, Transalg software tool developed based on these...

In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced SAT such way that it should be perceived as natural by cryptographic community. In~the theoretical part paper justify main principles general reduction from class containing majority employed cryptography. Then, Transalg software tool developed based on these...

In this paper we present the computational study of one class discrete models collective behavior. context these a set agents, that form collective, is represented by network. Each agent assigned special weight function. The behavior in time moments specified with vector function, coordinates which are defined values agents functions at corresponding moments. We phenomena concerning so-called conforming behavior: when an some moment decides to act or not depending on similar decisions, made...

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to Boolean Satisfiability Problem (SAT). We call set variables B ρ-backdoor, if for fraction at least ρ possible assignments from B, assigning their values in formula Conjunctive Normal Form (CNF) results polynomially solvable formulas. Clearly, ρ-backdoor with ρ=1 is an SBS. For given it efficiently construct (ε, δ)-approximation parameter using Monte Carlo method. Thus, we define...

Solving hard instances of the Boolean satisfiability problem (SAT) in practice is an interestingly nontrivial area. In particular, heuristic nature state-of-the-art SAT solvers makes it impossible to know advance how long will take solve any particular instance. One way coping with this disadvantage divide-and-conquer approach when original instance decomposed into several simpler subproblems. However, plays a crucial role resulting effectiveness solving. present study, we reduce...