A study of the applicability of the SMT/SAT-based theorem proves for Keccak hash functions cryptanalysis - Качко, Е.Г.; Телевный, Д.К. (Radiotekhnika, 2017)
The study is devoted to the problem of using the SMT proves for Keccak-p cryptanalysis in different steps. The article describes the possibilities to use the SMT/SAT exemplified with the search for pre-images of hash-function, SMT approaches to formal verifications in modeling, descriptions of existing tools and libraries.