Cryptography Stack Exchange
Cryptography Stack Exchange

Questions tagged [sat]

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

A propositional logic formula, also called Boolean expression, is built from variables, operators AND (conjunction, also denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬), and parentheses. A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables. The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. This decision problem is of central importance in many areas of computer science, including theoretical computer science, complexity theory, algorithmics, cryptography and artificial intelligence

9 questions
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 encryption works. From what I understand the…
Yuon
  • 153
  • 9
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. However it would be nice to evaluate a…
rkiyanchuk
  • 343
  • 2
  • 9
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 need help to understand it. The authors plot the…
juaninf
  • 2,621
  • 2
  • 17
  • 26
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, and then the last 64 bits contain the length of the…
MSJ
  • 61
  • 3
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 i=a*2^4+b*2^3+c*2^2+d*2+e and i is the offset from the least significant bit. The author Page 33/200, chapter 2.3.4 states that in order to find the polynomial for the…
mapjoe
  • 33
  • 3
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 primes and ask people to factorize the product. They…
Timur Timak
  • 145
  • 7
2
votes
1 answer

Partial Known Message Pre-Image Attack on SHA-1

If the last 448 bits of a sha1 block input are known (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 force all $2^{64}$ possibilities? Is this a kind of reduced…
Amin Habibi
  • 21
  • 1
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 of modular addition it would have without said constant…
LightBit
  • 1,392
  • 10
  • 24
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
  • 113
  • 7