OKlibrary  0.2.1.6
2_13.hpp File Reference

Investigations into small-scale AES key discovery for 2+1/3 round AES with 1 row and 16 columns. More...

Go to the source code of this file.


Detailed Description

Investigations into small-scale AES key discovery for 2+1/3 round AES with 1 row and 16 columns.

Todo:
Problem specification
Todo:
Using the canonical box translation <ul Translation of aes(2,1,16,8):
  • We treat S-boxes and additions as boxes.
  • The S-box is considered as a 16-bit to 1-bit boolean functions, translated using the canonical translation; see dualts_fcl in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac.
  • Additions of arity k are considered bit-wise as (k+1)-bit to 1-bit boolean functions; translated using their prime implicates.

Generating AES for 2 + 1/3 round:

num_rounds : 2$
num_rows : 1$
num_columns : 16$
exp : 8$
final_round_b : false$
box_tran : aes_ts_box$
seed : 1$
mc_tran : aes_mc_bidirectional$
output_ss_fcl_std(num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$

shell> cat ssaes_r2_c16_rw1_e8_f0.cnf | ExtendedDimacsFullStatistics n
 n non_taut_c red_l taut_c orig_l comment_count finished_bool
10144 151666 445264 0 445264 10145 1
 length count
1 16
2 140288
3 2496
4 128
17 8704
256 34
   

In this translation, we have:

  • 2 full rounds (Key Addition, SubBytes, and MixColumns operation).
  • 34 S-boxes:
    • 32 from SubBytes = 16 bytes * 2 rounds;
    • 2 from key schedule = 1 row * 1 word * 2 rounds.
  • 1156 additions:
    • 512 additions of arity 1:
      • 512 from MixColumns = 128 bits * 2 round * 2 directions;
    • 624 additions of arity 2:
      • 256 from key additions = 128 bits * 2 round;
      • 128 from final key addition = 128 bits;
      • 240 from the key schedule = (128 bits - 8 bits) * 2 round.
    • 16 additions of arity 3:
      • 16 from the key schedule = 8 bits * 2 rounds.
  • 16 bits for the constant in the key schedule = 8 bits * 2 rounds.

The number of clauses of each length in the translation, computed by:

maxima> ncl_list_full_dualts(8,16);
[[2,4096],[17,256],[256,1]]
   

This instance has 60 boxes = 34 S-boxes. This instance has the following number of clauses of length:

  • 1 : 16 = key schedule constant * 1;
  • 2 : 140288 = 34 boxes * 4096 + 512 additions (arity 1) * 2;
  • 3 : 2496 = 624 additions (arity 2) * 4;
  • 4 : 128 = 16 additions (arity 3) * 8;
  • 17 : 8704 = 34 boxes * 256;
  • 256 : 34 = 34 boxes * 1.

Then we can generate a random assignment with the plaintext and ciphertext, leaving the key unknown:

maxima> output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
   

and the merging the assignment with the translation:

shell> AppendDimacs-O3-DNDEBUG ssaes_r2_c16_rw1_e8_f0.cnf ssaes_pkpair_r2_c16_rw1_e8_f0_s1.cnf > experiment_r2_k1.cnf_minisat22
   

minisat-2.2.0 solves it in 40s:

shell> minisat-2.2.0 experiment_r2_k1.cnf
<snip>
restarts              : 127
conflicts             : 40088          (1009 /sec)
decisions             : 143275         (0.00 % random) (3606 /sec)
propagations          : 135629939      (3413792 /sec)
CPU time              : 39.73 s
   

Definition in file 2_13.hpp.