密码学分析-工具——CryptoSMT-526互联

	CryptoSMT是一个易于使用的工具，用于对称原语的密码分析，如分组密码或哈希函数。它基于SMT/SAT求解器，如STP, Boolector，CryptoMiniSat，并提供了一个简单的框架来使用它们进行密码分析技术。
	其中一些特点是: 关于原语微分行为的证明性质。寻找最佳的线性/微分路径。计算微分的概率。查找哈希函数的原图像。 *恢复密钥。
	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]
	请注意，目前并不是所有的功能都适用于所有的密码。[1]详细描述了该工具在SIMON分组密码上的应用，以及如何构造SIMON的微分/线性模型。
	# 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].