Tag Archives: sat

Summer School on Tools :: Mykonos, Greece :: 28.5 – 1.6.

Slightly redacted announcement for the 2012 Summer School on Tools below.

Following the success of the ECRYPT Workshop on Tools for Cryptanalysis 2010,the ECRYPT II Symmetric Techniques Virtual Lab (SymLab) is pleased to announce the 2012 Summer School on Tools. Covering selected topics in both symmetric and asymmetric cryptography, this summer school will provide a thorough overview of some of the most important cryptographic tools that emerged in recent years. While the summer school is aimed primarily at postgraduate students, attendance is open to all. Continue reading

Slides: Introduction to Algebraic Techniques in Block Cipher Cryptanalysis

This morning I delivered my talk titled “Algebraic Techniques in Cryptanlysis (of block ciphers with a bias towards Gröbner bases)” at the ECrypt PhD Summerschool here in Albena, Bulgaria. I covered:

  1. Why bother
  2. Setting up equation systems
  3. Solving (GBs, SAT solvers, MIP, Cube Testers)
  4. “Advanced” Techniques

Well, here are the slides, which perhaps spend too much time explaining F4.

PS: This is as good as any opportunity to point to the paper “Algebraic Techniques in Differential Cryptanalysis Revisited” by Meiqin Wang, Yue Sun, Nicky Mouha and Bart Preneel accepted at ACISP 2011. I don’t agree with every statement in the paper – which revisits techniques Carlos and I proposed in 2009 – but our FSE 2009 paper does deserve a good whipping, i.e., we were way too optimistic about our attack.

CryptoMiniSat 2.5 won the SATRace 2010

Mate Soos’ CryptoMiniSat won the SATRace 2010. Congratulations Mate! For those who don’t know CryptoMiniSat, it is a fork of MiniSat which supports XOR clauses (Gaussian elimination!) among other things. This makes it particularly suitable for cryptographic problems.  I’ll try to make an optional Sage Package for CryptoMiniSat soon-ish.

SAT Solving Pointers

This is just a quick note to point out two SAT-solving sources relevant for cryptography.

Have fun.

Algebraic Attacks and CNF

Since the seminal papers [1] and [2] by Bard, Courtois and Jefferson it seems accepted wisdom that the right thing to do for constructing a CNF representation of a block cipher is to construct an algebraic system of equations first (cf. [3]). This system of equations is then converted to CNF using some ANF to CNF converted (e.g. [4]) which deals with the negative impact of the XORs just introduced via the ANF. On the other hand, it is straight forward to compute some CNF for a given S-Box directly by considering its truth table. Sage now contains code which does this for you:

sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True)
sage: S = sr.sbox()
sage: print S.cnf()

[(1, 2, 3, 4, -5), (1, 2, 3, 4, 6), (1, 2, 3, 4, 7), (1, 2, 3, 4, -8), (1, 2, 3, -4, 5), (1, 2, 3, -4, -6), (1, 2, 3, -4, 7), (1, 2, 3, -4, 8), (1, 2, -3, 4, -5), (1, 2, -3, 4, 6), (1, 2, -3, 4, -7),(1, 2, -3, 4, 8), (1, 2, -3, -4, -5), (1, 2, -3, -4, 6), (1, 2, -3, -4, -7), (1, 2, -3, -4, -8), (1, -2, 3, 4, -5), (1, -2, 3, 4, -6), (1, -2, 3, 4, 7), (1, -2, 3, 4, -8), (1, -2, 3, -4, 5), (1, -2, 3, -4, 6), (1, -2, 3, -4, 7), (1, -2, 3, -4, -8), (1, -2, -3, 4, -5), (1, -2, -3, 4, 6), (1, -2, -3,4, 7), (1, -2, -3, 4, 8), (1, -2, -3, -4, 5), (1, -2, -3, -4, -6), (1, -2, -3, -4, 7), (1, -2, -3, -4, -8), (-1, 2, 3, 4, 5), (-1, 2, 3, 4, -6), (-1, 2, 3, 4, -7), (-1, 2, 3, 4, 8), (-1, 2, 3, -4, 5), (-1, 2, 3, -4, 6), (-1, 2, 3, -4, -7), (-1, 2, 3, -4, 8), (-1, 2, -3, 4, 5), (-1, 2, -3, 4, 6), (-1, 2, -3, 4, 7), (-1, 2, -3, 4, 8), (-1, 2, -3, -4, 5), (-1, 2, -3, -4, 6), (-1, 2, -3, -4, -7), (-1, 2, -3, -4, -8), (-1, -2, 3, 4, -5), (-1, -2, 3, 4, -6), (-1, -2, 3, 4, 7), (-1, -2, 3, 4, 8), (-1,-2, 3, -4, -5), (-1, -2, 3, -4, -6), (-1, -2, 3, -4, -7), (-1, -2, 3, -4, 8), (-1, -2, -3, 4, -5), (-1, -2, -3, 4, -6), (-1, -2, -3, 4, -7), (-1, -2, -3, 4, -8), (-1, -2, -3, -4, 5), (-1, -2, -3, -4,-6), (-1, -2, -3, -4, -7), (-1, -2, -3, -4, -8)]

I am not claiming that this naive approach produces an optimal representation, it seems more compact than what ANF to CNF converters produce, though.