CryptoSMT - an easy to use tool for cryptanalysis of symmetric primitives likes block ciphers or hash functions. 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. The following primitives are supported by CryptoSMT at the moment: Simon, Speck, Keccak, Ketje, Chaskey, SipHash, Salsa, ChaCha, Ascon. 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 .
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Chen, Shiyao; Fan, Yanhong; Sun, Ling; Fu, Yong; Zhou, Haibo; Li, Yongqing; Wang, Meiqin; Wang, Weijia; Guo, Chun: SAND: an AND-RX Feistel lightweight block cipher supporting S-box-based security evaluations (2022)
- Sadeghi, Sadegh; Rijmen, Vincent; Bagheri, Nasour: Proposing an MILP-based method for the experimental verification of difference-based trails: application to SPECK, SIMECK (2021)
- Kölbl, Stefan; Tischhauser, Elmar; Derbez, Patrick; Bogdanov, Andrey: Troika: a ternary cryptographic hash function (2020)
- Sun, Siwei; Hu, Lei; Qiao, Kexin; Ma, Xiaoshuang; Shan, Jinyong; Song, Ling: Improvement on the method for automatic differential analysis and its application to two lightweight block ciphers DESL and LBlock-s (2015)