CryptoSMT

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.

Applications

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.

Setup

Prerequisites

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

or

$ sudo apt-get install python3-yaml

which is used as format for the input files.

Configuration

After installing the solvers, CryptoSMT needs to know the paths to the binaries, which can be added into ./config.py.

# Paths to the STP and cryptominisat executable
PATH_STP = "../stp/stp"
PATH_CRYPTOMINISAT = "../cryptominisat/cryptominisat"
PATH_BOOLECTOR = "../boolector/boolector"

Parameters

A short explanation of the parameters which can be used. It also possible to get a list of them using $ python cryptosmt.py --help.

Overview of parameters
Parameter Description
--cipher x Specifies the cipher to use.
--rounds x The number of rounds used of the cipher
--wordsize x The size of the statewords in bits.
--mode x Determines the mode of operation. See table below for a description.
--sweight x The weight of the differential characteristic for the search to start.
--iterative Only search for iterative characteristics.
--inputfile x Use the parameters from an inputfile.

Currently the following modes are supported

Modes supported
Mode Description
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.

Examples

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 example file:

---
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.

One application of this is to find all differential characteristics contributing to a differential.