OKlibrary  0.2.1.6
1_13.hpp File Reference

Investigations into small-scale AES key discovery for 1+1/3 round AES with a 2x4 plaintext matrix and 4-bit field elements. More...

Go to the source code of this file.


Detailed Description

Investigations into small-scale AES key discovery for 1+1/3 round AES with a 2x4 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
Todo:
Using the canonical box translation
  • Translation of aes(1,2,4,4):
    • 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 8x1 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 small-scale AES for 1 + 1/3 round:
    num_rounds : 1$
    num_rows : 2$
    num_columns : 4$
    exp : 4$
    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_r1_c4_rw2_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    1036 6750 19476 0 19476 1037 1
     length count
    1 4
    2 5376
    3 624
    4 32
    9 672
    16 42
       
  • In this translation, we have:
    • 1 full round (Key Addition, SubBytes, and MixColumns operation).
    • 10 Sboxes:
      • 8 from SubBytes = 8 byte * 1 rounds;
      • 2 from key schedule = 2 row * 1 word * 1 rounds.
    • 16 multiplications by 02: 2 rows * 1 multiplication * 4 columns * 1 round * 2 directions (forward + inverse).
    • 16 multiplications by 03: 2 rows * 1 multiplication * 4 columns * 1 round * 2 directions (forward + inverse).
    • 160 additions:
      • 156 additions of arity 2:
        • 32 from key additions = 32 bits * 1 round;
        • 32 from final key addition = 32 bits;
        • 28 from the key schedule = (32 bits - 4 bits) * 1 round.
        • 32 from forward MixColumns = 2 rows * 4 column * 4 bits * 1 round;
        • 32 from inverse MixColumns = 2 rows * 4 column * 4 bits * 1 round.
      • 4 additions of arity 3:
        • 4 from the key schedule = 4 bits * 1 round.
    • 4 bits for the constant in the key schedule = 4 bits * 1 rounds.
  • The number of clauses of each length in the canonical translation:
    maxima> ncl_list_full_dualts(8,16);
    [[2,128],[9,16],[16,1]]
       
  • This instance has 42 boxes = 10 S-boxes + 32 multiplications.
  • This instance has the following number of clauses of length:
    • 1 : 4 = key schedule constant * 1;
    • 2 : 5376 = 42 boxes * 128;
    • 3 : 624 = 156 additions (arity 2) * 4;
    • 4 : 32 = 4 additions (arity 3) * 8;
    • 9 : 672 = 42 boxes * 16;
    • 16 : 42 = 42 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_rw2_e4_f0.cnf ssaes_pkpair_r1_c4_rw2_e4_f0_s1.cnf > r1_keyfind.cnf
       
  • minisat-2.2.0 solves it in 0.03s:
    restarts              : 11
    conflicts             : 1654           (55133 /sec)
    decisions             : 2581           (0.00 % random) (86033 /sec)
    propagations          : 211137         (7037900 /sec)
    conflict literals     : 36509          (24.97 % deleted)
    Memory used           : 19.00 MB
    CPU time              : 0.03 s
       
  • cryptominisat solves it in 0.03s:
    c restarts                 : 3
    c conflicts                : 362         (12066.67  / sec)
    c decisions                : 581         (0.00      % random)
    c CPU time                 : 0.03        s
       
    ??? what does "Verified 1017 clauses." mean here ???
  • OKsolver solves it in 0.9s:
    c running_time(sec)                     0.9
    c number_of_nodes                       103
    c number_of_2-reductions                3705
       

Definition in file 1_13.hpp.