密码学分析-工具——CryptoSMT

CryptoSMT目前支持以下原语:

###### Block Ciphers
* 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]

###### Hash Functions
* Keccak[14]

###### Stream Ciphers
* Salsa[15],
* ChaCha[16]

###### Authenticated Encryption Ciphers 认证加密密码
* Ketje[17],
* Ascon[18]

###### Message Authentication Codes  消息认证码

* Chaskey[19],
* SipHash[20]

# 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 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:

###### Block Ciphers
* 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]

###### Hash Functions
* Keccak[14]

###### Stream Ciphers
* Salsa[15],
* ChaCha[16]

###### Authenticated Encryption Ciphers
* Ketje[17],
* Ascon[18]

###### Message Authentication Codes
* 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].