Algorithms/procedures about cryptosmt HOT 6 CLOSED

The input to cryptoSMT is a set of parameters (cipher, rounds, target probability for differential characteristic, ...) and it constructs a problem instance in the CVC-language which is processable by STP. This is done by setting up the constraints (only allow valid differentials, ...) for the variables in each round.
Additionally, there is a variable weight which is used to sum up all the probabilities and enables the tool to search for differential characteristics with a certain probability by assigning a fixed value to it.

The procedure of finding the best differential characteristic (--mode 0) for the given parameters is the following:

• Construct the problem instance with the tool
• Check if STP finds a solution
  ** If there is a solution, output the variable assignment
  ** else increment weight and call STP again

In this case the SAT solver is called implicitly by STP, as it is a SAT-solver based SMT-solver.

The SAT-solver is used explicitly in the case of computing/estimating the probability of a differential (--mode 4).
STP is used to construct the CNF of the given SMT problem instance and then the SAT solver is called. This is done because for computing the probability of the differential we want to find many solutions to our given problem instance. The advantage of cryptominisat is that it keeps the state (learned clauses...) when searching for more solutions, which speeds up finding any subsequent solutions.

I hope I could clarify a few things. You might also want to read reference [1] given on the project site, which applies a similar approach to Salsa20.

from cryptosmt.

Hi, what is the role of python language in this smt solver?

from cryptosmt.

Hi!
For your information, CryptoSMT is not actually an SMT solver. It is actually a cryptographic tool which uses some SMT solvers such as STP, and Boolector, to solve some kinds of cryptographic problems. In other words, CryptoSMT uses Python language to create an SMT model, and then invokes an SMT solver to solve the obtained SMT model. Therefore, the main role of CryptoSMT is converting a cryptographic problem to an SMT model, and uses Python language to do that.
Good luck!

from cryptosmt.

from cryptosmt.

from cryptosmt.

from cryptosmt.