Ročníkový projekt

Názov projektu: Použitie SMT/SAT solverov pre automatickú kryptoanalýzu

Meno študenta: Marian Rajnoha (rajnoha7@uniba.sk)

Meno školiteľa: doc. RNDr. Martin Stanek, PhD. (stanek@dcs.fmph.uniba.sk)

Špecifikácia projektu:

Cieľom práce je ukázať na vybranej kryptografickej konštrukcii, napr. na symetrickej šifre alebo hašovacej funkcii, možnosti a limity SMT/SAT solverov pri jej kryptoanalýze. Práca by mala popísať spôsob reprezentácie vybraného algoritmu, formulácie útoku. Očakáva sa porovnanie výsledkov viacerých solverov z hľadiska úspechu analýzy, spotrebovaného času a pamäťovej náročnosti.

Doterajší priebeh projektu:

• oboznámenie sa s SMT solvermi Z3 a CVC5 a kryptografickou hešovacou funkciou u-Quark
• implementácia útoku na (niekoľkobajtový) vzor cez solver v zjednodušenej verzii u-Quarku
• implementácia vyhľadávania kolízie cez solver v zjednodušenej verzii u-Quarku
• meranie času výpočtu pre rôzne konfigurácie vstupu
• sledovanie využitia CPU a operačnej pamäte počas vykonávania týchto algoritmov

Výsledok projektu po prvom semestri: link

GitHub repozitár: link

Literatúra:

• Performance of various SMT Solvers in Cryptanalysis (DOI: 10.1109/ICCCIS51004.2021.9397110)
• Extending SAT Solvers to Cryptographic Problems (DOI: 10.1007/978-3-642-02777-2_24)
• Logical Cryptanalysis as a SAT Problem (DOI: 10.1023/A:1006326723002)