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:
The following primitives are supported by CryptoSMT at the moment:
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].
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 pyyamlThe 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 cryptosmtwhich 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 for the block cipher Simon.
Running the command
$ python3 cryptosmt.py --cipher simon --rounds 8 --wordsize 16will start the search for the optimal trail and you will see as output
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 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 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: 18CryptoSMT prints out the difference in the two state words x_i, y_i
and the probability for the transition between two rounds w_i.
Let's say you want to add "NewCipher" to the tool:
We can describe the process of the CryptoSMT as the following steps:
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
[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
@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}},
}