activity
20112022
most citedEncoding Cryptographic Functions to SAT Using Transalg System

21 citations · 67 across the 10 of their papers we have counts for

collaborators

10 papers

cs.CR2022★ 5 cited

Inverting Cryptographic Hash Functions via Cube-and-Conquer

Oleg Zaikin

MD4 and MD5 are fundamental cryptographic hash functions proposed in the early 1990s. MD4 consists of 48 steps and produces a 128-bit hash given a message of arbitrary finite size.…

physics.soc-ph2020★ 10 cited

Spontaneous symmetry breaking of active phase in coevolving nonlinear voter model

Arkadiusz Jędrzejewski, Joanna Toruniewska, Krzysztof Suchecki +2

We study an adaptive network model driven by a nonlinear voter dynamics. Each node in the network represents a voter and can be in one of two states that correspond to different op…

cs.LO2018★ 6 cited

Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

Alexander Semenov, Ilya Otpuschennikov, Irina Gribanova +2

In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic c…

cs.AI2018★ 6 cited

On Cryptographic Attacks Using Backdoors for SAT

Alexander Semenov, Oleg Zaikin, Ilya Otpuschennikov +2

Propositional satisfiability (SAT) is at the nucleus of state-of-the-art approaches to a variety of computationally hard problems, one of which is cryptanalysis. Moreover, a number…

math.CO2017★ 1 cited

Fast Algorithm for Enumerating Diagonal Latin Squares of Small Order

Stepan Kochemazov, Eduard Vatutin, Oleg Zaikin

In this paper we propose an algorithm for enumerating diagonal Latin squares of small order. It relies on specific properties of diagonal Latin squares to employ symmetry breaking…

cs.AI2016★ 21 cited

Encoding Cryptographic Functions to SAT Using Transalg System

Ilya Otpuschennikov, Alexander Semenov, Irina Gribanova +2

In this paper we propose the technology for constructing propositional encodings of discrete functions. It is aimed at solving inversion problems of considered functions using stat…

cs.AI2015★ 10 cited

Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem

Alexander Semenov, Oleg Zaikin

In this paper we propose the approach for constructing partitionings of hard variants of the Boolean satisfiability problem (SAT). Such partitionings can be used for solving corres…

cs.DC2014

Using Volunteer Computing for Mounting SAT-based Cryptographic Attacks

Alexander Semenov, Oleg Zaikin, Ilya Otpuschennikov

In this paper we describe the volunteer computing project SAT@home, developed and maintained by us. This project is aimed at solving hard instances of the Boolean satisfiability pr…

cs.AI2013★ 4 cited

On estimating total time to solve SAT in distributed computing environments: Application to the SAT@home project

Alexander Semenov, Oleg Zaikin

This paper proposes a method to estimate the total time required to solve SAT in distributed environments via partitioning approach. It is based on the observation that for some si…

cs.DC2011★ 4 cited

Parallel algorithms for SAT in application to inversion problems of some discrete functions

Alexander Semenov, Oleg Zaikin, Dmitry Bespalov +1

In this article we consider the inversion problem for polynomially computable discrete functions. These functions describe behavior of many discrete systems and are used in model c…