A study of the applicability of the SMT/SAT-based theorem proves for Keccak hash functions cryptanalysis

Authors

  • Е.Г. Качко
  • Д.К. Телевный

Keywords:

SMT, SAT, theorem, cryptanalysis, Keccak, CNF

Abstract

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.

References

Nieuwenhuis, R., Oliveras, A., Tinelli, C. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) // Journal of the ACM. – 2006. – Т. 53, № 6. – P. 937 – 977.

Guido Bertoni, Joan Daemen, Michaël Peeters Gilles Van Assche. The Keccak sponge function family [Электронный ресурс]. – Режим доступа: http://keccak.noekeon.org/ – 21.04.2017. – Загл. с экрана.

Hassan Eldib, Chao Wang, and Patrick Schaumont SMT-Based Verification of Software Countermeasures against Side-Channel Attacks [Электронный ресурс]. – Режим доступа: http://www.faculty.ece.vt.edu/chaowang/pubDOC/Eldib14maskVerif.pdf – 21.02.2011. – Загл. с экрана.

Брюс Шнайер. Прикладная криптография. Протоколы, алгоритмы, исходные тексты на языке С. – Москва : Триумф, 2002.

Clark Barrett, Aaron Stump, Cesare Tinelli. The SMT-LIB Standard Version 2.0 [Электронный ресурс]. – Режим доступа: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf – 21.11.2011. – Загл. с экрана.

SMT-LIB The satisfiability modulo theories library [Элек-тронный ресурс]. – Режим доступа: http://smtlib.cs.uiowa.edu/logics.shtml – 21.03.2017. – Загл. с экрана.

Levent Erk ok Theorem declarations in Cryptol [Электронный ресурс]. – Режим доступа: http://community.galois.com/pipermail/cryptol-users/attachments/20110316/f66e99b2/attachment-0003.pdf – 02.10.2008. – Загл. с экрана.

How to Cite

Качко, Е., & Телевный, Д. (2017). A study of the applicability of the SMT/SAT-based theorem proves for Keccak hash functions cryptanalysis. Radiotekhnika, 2(189), 75–80. Retrieved from http://rt.nure.ua/article/view/183315

Issue

Section

Articles