mhgharieb/cryptosmt

An easy to use tool for cryptanalysis of symmetric primitives based on SMT/SAT solvers.

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.

Some of the features are:

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

Supported Primitives

The following primitives are supported by CryptoSMT at the moment:

Block Ciphers

• Simon[2],
• Speck[2],
• Skinny[3],
• Present[4],
• Midori[5],
• LBlock[6],
• Sparx[7],
• Twine[8],
• Noekeon[9],
• Prince[10],
• Mantis[3],
• Speckey[7],
• Rectangle[11],
• Cham[12]

Hash Functions

• Keccak[13]

Stream Ciphers

• Salsa[14],
• ChaCha[15]

Authenticated Encryption Ciphers

• Ketje[16],
• Ascon[17]

Message Authentication Codes

• Chaskey[18],
• SipHash[19]

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

Installation & Tutorial

For information on how to install CryptoSMT and a tutorial on how to use it see the project website.

References

• [1] Observations on the SIMON block cipher family
• [2] The SIMON and SPECK Families of Lightweight Block Ciphers
• [3] The SKINNY Family of Block Ciphers and its Low-Latency Variant MANTIS
• [4] PRESENT: An Ultra-Lightweight Block Cipher
• [5] Midori: A Block Cipher for Low Energy (Extended Version)
• [6] LBlock: A Lightweight Block Cipher
• [7] Design Strategies for ARX with Provable Bounds: SPARX and LAX (Full Version)
• [8] TWINE: A Lightweight Block Cipher for Multiple Platforms
• [9] Nessie Proposal: NOEKEON
• [10] PRINCE - A Low-latency Block Cipher for Pervasive Computing Applications (Full version)
• [11] RECTANGLE: A Bit-slice Lightweight Block Cipher Suitable for Multiple Platforms
• [12] CHAM: A Family of Lightweight Block Ciphers for Resource-Constrained Devices
• [13] The Keccak reference
• [14] The Salsa20 family of stream ciphers
• [15] ChaCha, a variant of Salsa20
• [16] CAESAR submission: Kђѡїђ v2
• [17] Ascon v1.2 Submission to the CAESAR Competition
• [18] Chaskey: An Efficient MAC Algorithm for 32-bit Microcontrollers
• [19] SipHash: a fast short-input PRF

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

BibTex

@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}},
}