The source codes and results are used to help verify the results in our paper. All experiments are conducted on a server with Intel(R) Xeon(R) CPU E5-4650 v3 @ 2.10GHz 12 Core, 65G RAM, and Ubuntu 18.04.5.
- SageMath version 10.3
- Python 3.11.9
- cryptominisat 5.8.0
- Bosphorus 3.0
code files:
-
Keccak code: the code to describe model initialization and generate the final SAT model in indirect encoding way for verifing differential trails of Keccak. result: output all ANF and CNF files of each verified trails as well as print the final feasible solution (i.e. a right message pair) and run time.
-
ascon code: the code to describe model initialization and generate the final SAT model in indirect encoding way for verifing differential trails of Ascon. result: output all ANF and CNF files of each verified trails as well as print the final feasible solution (i.e. a right message pair) and run time.
-
compare_keccak_sat code: the code to describe model initialization and generate the final SAT model in direct encoding way for verifing differential trails of Keccak. result: output all CNF files of each verified trails as well as print the final feasible solution (i.e. a right message pair) and run time.
-
gimli code: the code to describe model initialization and generate the final SAT model in indirect encoding way for verifing differential trails of Gimli. result: output all ANF and CNF files of each verified trails as well as print the final feasible solution (i.e. a right message pair) and run time.
Note: A brief user's guide with instructions on how to use Algsat is available in "USER_GUIDE.md" file.