Skip to main content

Questions tagged [sat]

For questions involving/related to the Boolean satisfiability problem (SAT).

Filter by
Sorted by
Tagged with
1 vote
1 answer

How to use smt solvers in order to restrict the possible key search where a portion of the private key and a portion of the public key hash is known?

I’m in the following situation : I’ve a portion/first bytes of a private secp256k1 security key such as it would take minutes to fully recover it through Pollard’s Kangaroo if I had the public key. ...
user2284570's user avatar
0 votes
0 answers

How to express the Boolean cardinality constraint to CNF formulas

A Boolean cardinality constraint $$\sum_{j=0}^{n-1}x_j=k,$$ where $x_j$’s are Boolean variables, and $k$ is a non-negative integer. How to express the Boolean cardinality constraint to CNF formulas?
mini minions's user avatar
3 votes
1 answer

Is SAT the mathematical problem behind SHA-2 and SHA-3?

When I'm convincing non-believers that crypto is secure, I have a hard time with hash functions and the associated block ciphers. It is easy to show why RSA is hard to crack: I multiply two small ...
Timur Timak's user avatar
1 vote
1 answer

Alzette ARX round constants

In this paper Alzette "ARX-box" is presented and on page 9 authors claim about XORing round constants: They also break additive patterns that could arise on the left branch due to the chain ...
LightBit's user avatar
  • 1,659
0 votes
1 answer

current state of 3-SAT problem?

In this paper, a quantum algorithm to solve the 3-SAT problem in linear time is presented. Is it true? Did the author make a mistake? What state-of-the-art algorithms exist for this problem?
OneUser's user avatar
  • 133
4 votes
1 answer

Partial known message pre-image attack on SHA-1

If the last $448$ bits of a SHA-1 block input are known and only the first $64$ bits are unknown, is it possible to do a preimage attack using SAT solvers or something else? Or do I have to brute ...
Amin Habibi's user avatar
3 votes
1 answer

How to sequence SHA256 block circuit to obtain hash of a message comprising multiple 512 blocks?

I am trying to obtain a circuit that computes the SHA256 hash for an input message that is greater than 512 bits. I understand how the message is to be padded (we append a 1 and then some zeroes, ...
MSJ's user avatar
  • 61
3 votes
1 answer

Function to polynomial equation in GF(2)

Let F(a,b,c,d,e) be a function that returns the ith bit of 0x3A5C742E, where ...
mapjoe's user avatar
  • 33
8 votes
3 answers

SAT-Based Public Key Cryptosystem

I am researching post quantum cryptography and I've stumbled upon this article which presents a PKC with an np-complete (SAT) trapdoor. I was wondering if someone could help me understand the way the ...
Yuon's user avatar
  • 163
4 votes
1 answer

Plotting Running Times of SAT solver

In the the paper "Efficient Methods for Conversion and Solution of Sparse Systems of Low-Degree Multivariate Polynomials over GF(2) via SAT-Solvers" there is a Figure that I can not understand and I ...
juaninf's user avatar
  • 2,711
5 votes
2 answers

Determine complexity of a SAT problem

Is there a standard way to determine a complexity of the specified SAT problem? I'm researching algebraic cryptanalysis and came to solving multivariate quadratic equation systems using CryptoMiniSat. ...
rkiyanchuk's user avatar