CryptoSMT is an easy to use tool for cryptanalysis of symmetric primitives likes block ciphers or hash functions. It is based on SMT/SAT solvers like STP, Boolector, CryptoMiniSat and provides a simple framework to use them for cryptanalytic techniques. The project is hosted on GitHub.
CryptoSMT allows to formulate various cryptanalytic problems in a simple way and solve them with SMT/SAT solvers.
- Proof properties regarding the differential behavious of a primitive.
- Find the best linear/differential characteristics.
- Compute probability of a differential.
- Find preimages/collisions for hash functions.
- Recover a secret key.
CryptoSMT invokes the SMT solver STP and the SAT solver CryptoMiniSat, which are required to run the tool. To have the latest version of the solvers it is recommended to build them yourself:
To enable the
--boolector flag, Boolector should be installed. While
this is optionally we observed that it can outperform other solvers on the problem
instances we are interested.
Additionally it might be necessary to install the python YAML library
$ pip3 install pyyaml
$ sudo apt-get install python3-yaml
which is used as format for the input files.
After installing the solvers, CryptoSMT needs to know the paths to the binaries, which
can be added into
# Paths to the STP and cryptominisat executable PATH_STP = "../stp/stp" PATH_CRYPTOMINISAT = "../cryptominisat/cryptominisat" PATH_BOOLECTOR = "../boolector/boolector"
A short explanation of the parameters which can be used. It also
possible to get a list of them using
$ python cryptosmt.py --help.
||Specifies the cipher to use.|
||The number of rounds used of the cipher|
||The size of the statewords in bits.|
||Determines the mode of operation. See table below for a description.|
||The weight of the differential characteristic for the search to start.|
||Only search for iterative characteristics.|
||Use the parameters from an inputfile.|
Currently the following modes are supported
|0||Finds the characteristic with minimal weight for the given parameters.|
|1||Finds the characteristic with minimal weight for an increasing number of rounds.|
|2||Outputs all valid characteristics for the given parameters.|
|4||Counts all characteristic for the given parameters, for instance to determine the probability of a differential.|
Finding optimal characteristic
In the first example we want to find the best differential characteristic for the SIMON block cipher. We can specify parameters and start CryptoSMT:
$ python3 cryptosmt.py --cipher simon --rounds 8 --wordsize 16
If no mode is specified CryptoSMT uses mode 0 and tries to find the best characteristic.
simon - Rounds: 8 Wordsize: 16 --- Weight: 0 Time: 0.0s Weight: 1 Time: 0.08s Weight: 2 Time: 0.16s Weight: 3 Time: 0.44s Weight: 4 Time: 0.74s Weight: 5 Time: 0.89s ...
CryptoSMT tries to find a differential characteristic with a given weight \(w_i\). If no such characteristic exists \(w_i\) is incremented and the search continues. In this case the best characteristic has a weight of 18 and can be quickly found:
Characteristic for simon - Rounds 8 - Wordsize 16 - Weight 18 - Time 13.15s Rounds x y w ------------------------------- 0 0x0040 0x0191 -2 1 0x0011 0x0040 -4 2 0x0004 0x0011 -2 3 0x0001 0x0004 -2 4 0x0000 0x0001 -0 5 0x0001 0x0000 -2 6 0x0004 0x0001 -2 7 0x0011 0x0004 -4 8 0x0040 0x0011 none Weight: 18
The tool prints out the difference in the two state words \(x_i\), \(y_i\) and the probability for the transition between two rounds \(w_i\).
Using Input files
For more complex scenarios CryptoSMT specifies a YAML based input file format. The tool
can process them with the
--inputfile x parameter. Lets have a look at an
--- cipher: simon sweight: 18 rounds: 8 wordsize: 16 mode: 4 fixedVariables: - x0: "0x0040" - y0: "0x0191" - x8: "0x0040" - y8: "0x0011" ...
We can directly specify the parameters and also fix certain variables of the state.