search

kste / cryptosmt

An easy to use tool for cryptanalysis of symmetric primitives based on SMT/SAT solvers.
MIT License
89 stars 36 forks source link

Mode 4 issue #17

Open nivi1501 opened 2 years ago

nivi1501 commented 2 years ago

Hi, I executed the following command and obtained the results given below. I have a few queries regarding the output:

  1. Current probability is greater than 1. What does the 'current probability' depict here?
  2. Can you please direct me towards the documentation to highlight the significance of the words 'trails' and 'weights'

python3 cryptosmt.py --cipher present --rounds 1 --wordsize 64 --mode 4 --boolector Finding all trails of weight 0 Solutions: 0 Finding all trails of weight 1 Solutions: 0 Finding all trails of weight 2 Solutions: 384 Trails found: 384 Current Probability: 6.584962500721156 Time: 7.89s Finding all trails of weight 3 Solutions: 1152 Trails found: 1536 Current Probability: 7.906890595608519 Time: 18.62s Finding all trails of weight 4 Solutions: 69120 Trails found: 70656 Current Probability: 12.154818109052105 Time: 611.57s Finding all trails of weight 5 Solutions: 38478 Trails found: 109134 Current Probability: 12.49246348266757 Time: 1012.54s

kste commented 2 years ago

The current probability here shows the sum of the probability of all trails which you found. This might not be very meaningful depending on how the model/search is setup (and the tool does not provide any guidance unfortunately). In general how you would use this is to fix the input/output difference, and then find all trails which have the same input/output difference. If you don't restrict the differences, then the tool will just sum up all trails.

Trail refers to what in the literature is called differential characteristic/path/trail. See for instance https://eprint.iacr.org/2018/689.pdf for some better definitions.