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.

Some of the features are:

• Proof properties regarding the differential behavious of a primitive.
• Find the best linear/differential trails.
• Compute probability of a differential.
• Find preimages for hash functions.
• Recover a secret key.

The following primitives are supported by CryptoSMT at the moment:

• Simon[3],
• Speck[3],
• Skinny[4],
• Present[5],
• Midori[6],
• LBlock[7],
• Sparx[8],
• Twine[9],
• Noekeon[10],
• Prince[11],
• Mantis[4],
• Speckey[8],
• Rectangle[12],
• Cham[13],
• CRAFT[21],
• TRIFLE[22]
• SAND[23]

• Keccak[14]

• Salsa[15],
• ChaCha[16]

• Ketje[17],
• Ascon[18]

• Chaskey[19],
• SipHash[20]

Please note that at the moment not all features are available for all ciphers. A detailed description on the application of this tool on the SIMON block ciphers and how a differential/linear model for SIMON can be constructed is given in [1].

You can find some additional information on the project website.

CryptoSMT requires you to have STP and Cryptominisat installed and setup the paths to the binaries in config.py. Further it requires the pyyaml which you can install using

$ pip3 install pyyaml

The easiest way to get all the external tools to run is with the provided Dockerfile. You can build a basic image using:

cd docker/
docker build -t cryptosmt .

This includes building minisat, cryptominisat, STP, boolector and all dependencies. You can then run the image with:

docker run -it cryptosmt

which gives you a ready to use setup of CryptoSMT.

As an example we will look at how CryptoSMT can be used to find the optimal differential characteristics from round 1 to 16 for the block cipher sand-64 under looser pattern model.

Running the command

$ python3 cryptosmt.py --cipher sand_diff_pattern --round 1 --endrounds 16 --mode 1 --wordsize 32

will start the search for the optimal trail and you will see as output

R  1r:
Starting search for characteristic with minimal weight
sand_diff_pattern - Rounds: 1 Wordsize: 32
---
Weight: 0 Time: 0.0s
---

CryptoSMT tries to find a differential trail with a given weight w_i. If no such trail exists w_i is incremented and the search continues. In this case the best trail has a weight of 0 and can be quickly found:

Characteristic for sand_diff_pattern - Rounds 1 - Wordsize 32 - Weight 0 - Time 0.01s
Rounds  x       y       inG0    inG1    xorG    permG   sumw
---------------------------------------------------------------
0       0x00    0x01    0x00    0x00    0x00    0x00    0x0000
1       0x01    0x00    none    none    none    none    none

Weight: 0
Wrote .tex to tmp/sand_diff_pattern-wd32-stp/sand_diff_pattern-wd32-1r-0weight.tex
current round time cost:     0.01 s

CryptoSMT prints out the difference in the two state words x_i, y_i , the probability for the transition between two rounds sumw_i and some other Intermediate variable.

Similarly, the following command can be used to find the optimal linear characteristics from round 1 to 16 for the block cipher sand-64 under active S-box model with detailed LAT.

$ time python3 cryptosmt.py --cipher sand_linear_actsbox --round 1 --endrounds 16 --mode 1 --wordsize 32

Let's say you want to add "NewCipher" to the tool:

1. Make a copy from an example in "./ciphers/" which is similar to the design you want to analyze (for example if you want an ARX, Speck might be a good start) and rename it to "NewCipher.py".
2. Modify the content of "NewCipher.py" to adapt it to your cipher (here it's best to look at some examples, as it depends a lot on design).
3. Update the file "cryptosmt.py": Add "NewCipher" in the import (line 8), and include it in the tool by adding it to the ciphersuite (line 25).
4. Run "python3 cryptosmt.py --cipher NewCipher" to see if it works.

We can describe the process of the CryptoSMT as the following steps:

1. It creates an stp file which contains the SMT model of the differential cryptanaysis of the given cipher in CVC format (this file is placed in "./tmp/" folder)
2. After generation of SMT model in CVC format, it calls an SMT solver to solve the generated model. The STP is used by default as SMT solver. You can also use the Boolector as SMT solver.
3. The SMT model contains some inherent constraints which are used for modeling the differential propagation rules, and some additional constraints which are used to model the outside counditions like the fixed input/output differentials values.
4. One of the additional constraints is the starting weight (of the differential probability) constraint. The first SMT model is generated with the starting weight, and this model is changed repeatedly by increasing the weight by one, and each time, it's satisfiablity is checked by an SMT solver. The goal is to find the minimum weight which makes the model satisfiable.
5. If the SMT model is satisfiable for the first time, the weight (of the differential probability) which is used, is reteurned as the minimum weight (of the differential probability) as one of the output, and the process is stoped.

These processes are almost realted to the mod0, which is used to find the best differential with maximum (minimum) differential probablity (weight).

Special thanks to Ralph Ankele and Hosein Hadipour for their extensive contributions!

[1] Observations on the SIMON block cipher family

[2] Mind the Gap - A Closer Look at the Security of Block Ciphers against Differential Cryptanalysis

[3] The SIMON and SPECK Families of Lightweight Block Ciphers

[4] The SKINNY Family of Block Ciphers and its Low-Latency Variant MANTIS

[5] PRESENT: An Ultra-Lightweight Block Cipher

[6] Midori: A Block Cipher for Low Energy (Extended Version)

[7] LBlock: A Lightweight Block Cipher

[8] Design Strategies for ARX with Provable Bounds: SPARX and LAX (Full Version)

[9] TWINE: A Lightweight Block Cipher for Multiple Platforms

[10] Nessie Proposal: NOEKEON

[11] PRINCE - A Low-latency Block Cipher for Pervasive Computing Applications (Full version)

[12] RECTANGLE: A Bit-slice Lightweight Block Cipher Suitable for Multiple Platforms

[13] CHAM: A Family of Lightweight Block Ciphers for Resource-Constrained Devices

[14] The Keccak reference

[15] The Salsa20 family of stream ciphers

[16] ChaCha, a variant of Salsa20

[17] CAESAR submission: Kђѡїђ v2

[18] Ascon v1.2 Submission to the CAESAR Competition

[19] Chaskey: An Efficient MAC Algorithm for 32-bit Microcontrollers

[20] SipHash: a fast short-input PRF

[21] CRAFT: Lightweight Tweakable Block Cipher with Efficient Protection Against DFA Attacks

[22] TRIFLE

[23] SAND: an AND-RX Feistel lightweight block cipher supporting S-box-based security evaluations

@misc{CryptoSMT-ref,
    author = {{Stefan Kölbl}},
    title = {{CryptoSMT: An easy to use tool for cryptanalysis of symmetric primitives}},
    note = {\url{https://github.com/kste/cryptosmt}},
}