kste
commented
9 years ago 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.
git2109
hadipourh
Dear Author, May I know how the tool was developed. What are different algorithms used. Can you explain what are the steps involved.What is the input for SMT, from there what is the output to STP/cryptominisat