DES as a SAT problem

• Use encoding of DES into SAT

• Each bit of C, P, K, is propositional variable

• Operation of f is transformed into boolean form

  • CAD tools used separately to optimise this

• Formulae corresponding to each step of DES

• This would be huge and unwieldy, so

  • “clever optimisations” inc. some operations precomputed

• Result is a SAT formula (P,K,C)

  • remember bits are variable, so this encodes the algorithm
    • not a specific plain text

• set some bits (e.g. bits of C) for specific problem