This tool generates SMT programs for ciphers RC4 and Spritz and runs SMT solvers on these programs.
Input to this tool is a file with RC4 or Spritz states, generated by generate.py with switch --smt. For each state, the tool generates SMT program for either recovering cipher state from keystram or generating keystream from state, using one of two SMT logics. The amount of keystream (rounds of cipher) used in SMT program and the set of forbidden states (in case of recovering state, it forces SMT solver to find state other than stated in forbidden states) can be set. In case we don't want to test each state for uniqueness (as it can take much longer than just solving the problem), it can be turned off. The cipher Spritz is able to use only with logic abv
The tool runs SMT solver on generated programs and outputs statistics about each experiment. Any SMT solver that is able to read format SMT-Lib v2 from stdin can be used.
All tool options are printed out with switch -h.
Tento nástroj slúži na generovanie SMT programov pre šifry RC4 a Spritz a na spúšťanie SMT solverov na týchto programoch.
Vstup nástroja je súbor so stavmi šifry RC4 alebo Spritz vygenerovaný skriptom generate.py s prepínačom --smt. Pre každý stav nástroj vygeneruje SMT program buď na extrakciu stavu šifry z bežiaceho kľúča alebo na vypočítanie bežiaceho kľúča zo stavu v jednej z dvoch SMT logík. Dĺžka bežiaceho kľúča a množina zakázaných stavov (v prípade extrakcie stavu, zakázané stavy nútia SMT solver nájsť riešenie programu iné ako dané stavy) sa dajú nastaviť. V prípade, že necheme testovať programy na jednoznačnosť stavu (keďže to môže trvať dosť dlho), táto funckia sa dá vypnúť. Šifra Spritz sa dá modelovať iba logikou abv.
Nástroj pre každý vygenerovaný program spustí SMT solver a vypíše informácie o experimente. Použiť sa dá ľubovoľný SMT solver podporujúci formát SMT-Lib v2 a čítanie zo štandardného vstupu.
Všetky možnosti nástroja sa vypíšu prepínačom -h.