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.

Zimný semester:

• 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)
• Quark: a lightweight hash (DOI: 10.1007/s00145-012-9125-6)

Letný semester:

• oboznámenie sa s blokovými šiframi RAZOR a LLLWBC
• implementácia overovania diferencií pre ľubovoľný počet kôl LLLWBC prostredníctvom SMT solvera Z3
• implementácia hľadania minimálneho počtu aktívnych kolových funkcií v LLLWBC prostredníctvom Z3

Výsledok projektu po druhom semestri: link

GitHub repozitár: link

Literatúra:

• LLLWBC: A New Low-Latency Light-Weight Block Cipher (DOI: 10.1007/978-3-031-26553-2_2)