OKlibrary  0.2.1.6
1_13.hpp File Reference

Investigations into AES key discovery for 1 round AES (1+1/3) More...

Go to the source code of this file.


Detailed Description

Investigations into AES key discovery for 1 round AES (1+1/3)

Todo:
Problem specification
Todo:
Using the canonical box translation
  • Translation of aes(1,4,4,8):
    • The MixColumns operation is decomposed into its field multiplications (02 and 03) and addition operations.
    • The MixColumns operation is translated by translating both the MixColumns operation and its inverse (it is self-inverse).
    • We treat S-boxes, field multiplications and additions as boxes.
    • The S-box and field multiplications are considered as a 16x1 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 1 + 1/3 round:
    num_rounds : 1$
    num_rows : 4$
    num_columns : 4$
    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)$
    
    ???
    Maxima encountered a Lisp error:
    
     Memory limit reached. Please jump to an outer pointer, quit program and enlarge the
    memory limits before executing the program again.
    ???
    
    shell> cat ssaes_r1_c4_rw4_e8_f0.cnf | ExtendedDimacsFullStatistics n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    31400 510620 1510056 0 1510056 31401 1
     length count
    1 8
    2 475136
    3 1504
    4 64
    5 4096
    17 29696
    256 116
       
  • In this translation, we have:
    • 1 full round (Key addition, SubBytes and MixColumns).
    • 20 Sboxes:
      • 16 from SubBytes = 16 bytes * 1 round.
      • 4 from key schedule = 1 column * 4 bytes * 1 round.
    • 640 additions:
      1. 376 arity two additions:
        • 128 from key additions = 128 bits * 1 round.
        • 128 from final key addition = 128 bits.
        • 120 from key schedule = (128 - 8) bits * 1 round.
      2. 8 arity three additions: 8 from key schedule = 8 bits * 1 round.
      3. 256 arity four additions: 256 from summation in MixColumns matrix multiplication = 4 additions * 4 columns * 16 bits * 1 round.
    • 16 multiplications by 02: 4 rows * 1 multiplication * 4 columns 1 round.
    • 16 multiplications by 03: 4 rows * 1 multiplication * 4 columns 1 round.
    • 16 multiplications by 09: 4 rows * 1 multiplication * 4 columns 1 round.
    • 16 multiplications by 11: 4 rows * 1 multiplication * 4 columns 1 round.
    • 16 multiplications by 13: 4 rows * 1 multiplication * 4 columns 1 round.
    • 16 multiplications by 14: 4 rows * 1 multiplication * 4 columns 1 round.
    • 8 bits set for the constant in the key schedule.
  • The number of clauses of each length in the canonical box translations:
    maxima> ncl_list_full_dualts(16,256);
    [[2,4096],[17,256],[256,1]]
       
  • The instance has 20 S-boxes + 16 * 6 multiplications = 116 boxes (excluding additions).
  • The instance has the following number of clauses of the following size:
    • 1 : 8 = key schedule constant * 1;
    • 2 : 475136 = 116 boxes * 4096;
    • 3 : 1504 = 376 additions (arity 2) * 4;
    • 4 : 64 = 8 additions (arity 3) * 8;
    • 5 : 4096 = 256 additions (arity 4) * 16;
    • 16 : 29696 = 116 boxes * 256 clauses;
    • 256 : 116 = 116 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_r1_c4_rw4_e8_f0.cnf ssaes_pkpair_r1_c4_rw4_e8_f0_s1.cnf > ssaes_r1_c4_rw4_e8_f0_keyfind.cnf
       
  • MG is running experiments with various solvers, but all are ongoing (after a day).
  • The next thing to try is replacing the boxes with the r_1 bases we have.

Definition in file 1_13.hpp.