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

cryptosmt #6

Closed siweisun closed 9 years ago

siweisun commented 9 years ago

Hi kste,

Great project ! I am also working on automatic cryptanalysis based on Mixed-integer linear programming (MILP), instead of SAT.

See

  1. http://eprint.iacr.org/2013/676
  2. http://eprint.iacr.org/2014/747

One main drawback of the MILP based method is that it is not suitable for ARX construction (modelling the differential behavior of mod addition introduces too many variables and constraints), and I think the method presented in "Towards Finding Optimal Differential Characteristics for ARX: Application to Salsa20" is very promising for ARX. And I think the framework you implement is very interesting and will be very useful.

I see that you have implemented the examples of SIMON and SPECK. May I know the results you have obtained using this framework? For example, can you use your framework to prove that SPECK is secure against basic differential attack (based on differential characteristic)? What is the longest/best characteristic you've got for SIMON and SPECK?

Best regards, Siwei Sun

E-mail: sunsiwei at iie.ac.cn

kste commented 9 years ago

Hi Siwei Sun,

I've also seen your work on eprint and read it. It looks very interesting and I've already checked and compared the results with my tool. I can confirm your differentials for SIMON48/64 and get a very similar probability with my tool resp. find similar characteristics. For SIMON48 I could also find a 17-round differential with probability >=2^-46.5.

For SPECK the problem instances are harder and it takes a long time to search for characteristics for SPECK48/64 without any additional restrictions (there are a few tricks possible...). For SPECK32 it is feasible to proof resistance against basic attacks using a single differential characteristic.

I'm currently working on a bigger update, which should be done and released by the end of the year. It includes other ARX constructions (Siphash, Chaskey, ...), different attack vectors (linear characteristics, key recovery) and support for a faster solver (boolector).

Thanks for your interest!

siweisun commented 9 years ago

Thanks for you quick response, and look forward your next update!

I see the that boolector uses PicoSAT as its underlying SAT solver. Is PicoSAT faster than Cryptominisat? May you tell me your email address. I'm not quit familiar with Github and do not know how to send you messagese directly. :)

kste commented 9 years ago

The latest boolector version should use Lingeling and it seems to be faster (often by a factor of 3) on many problems I tried to solve with this this tool. I'll send you an e-mail.