search

msoos / grainofsalt

Grain of Salt equation generator
Other
16 stars 5 forks source link

Interpretation of SAT solver Outputs #6

Open notmike-5 opened 10 months ago

notmike-5 commented 10 months ago

Once a stream cipher is properly specified, and the CNFs are generated by GoS and fed into a suitable SAT solver (e.g. CryptoMiniSat), how exactly should the output of the solver be interpreted for satisfiable instances? Is the solver returning the plaintext for that particular instance, the key or some state information, or is it something else?

For example, using Grain as our chosen stream cipher and using the default specification provided with GoS, CryptoMiniSat outputs something on the close order of ~3950 variable assignments. I understand Grain to have an 80-bit key and 64-bit IV, so the output seems too lengthy to be these. To be honest, I'm not really sure how to interpret the output variable assignments.

msoos commented 10 months ago

Hi,

It depends on the specification of the stream cipher. If the key is loaded into the first shift register, and the shift register is 80 bits long, then the fist 80 variables will be the key.

Beware, you need to specify output, IV, etc or the key will be for a solver-picked output, which is of course easy to do.

I hope this helps,

Mate