OKlibrary  0.2.1.6
14_13.hpp File Reference

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

Go to the source code of this file.


Detailed Description

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

Todo:
Problem specification
Todo:
Using the canonical box translation
  • Translation of aes(14,2,1,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 small scale AES for 14 + 1/3 rounds:
    rounds : 14$
    num_rows : 2$
    num_columns : 1$
    exp : 8$
    final_round_b : false$
    box_tran : aes_ts_box$
    seed : 1$
    mc_tran : aes_mc_bidirectional$
    output_ss_fcl_std(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
    
    shell> cat ssaes_r14_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    45072 734616 2160112 0 2160112 45073 1
     length count
    1 112
    2 688128
    3 3200
    17 43008
    256 168
       
  • In this translation, we have:
    • 14 full rounds (Key Addition, SubBytes, and MixColumns operation).
    • 56 Sboxes:
      • 28 from SubBytes = 2 byte * 14 rounds;
      • 28 from key schedule = 2 row * 1 byte * 14 rounds.
    • 56 multiplications by 02: 2 rows * 1 multiplication * 1 columns * 14 rounds * 2 directions (forward + inverse).
    • 56 multiplications by 03: 2 rows * 1 multiplication * 1 columns * 14 rounds * 2 directions (forward + inverse).
    • 800 additions of arity 2:
      • 224 from key additions = 16 bits * 14 rounds;
      • 16 from final key addition = 16 bits;
      • 112 from the key schedule = 1 rows * 8 bits * 14 rounds.
      • 224 from forward MixColumns = 2 rows * 1 column * 8 bits * 14 rounds;
      • 224 from inverse MixColumns = 2 rows * 1 column * 8 bits * 14 rounds.
    • 112 bits for the constant in the key schedule = 8 bits * 14 rounds.
  • Note that as this variant has only one column, the key schedule applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and K_j are key words from the previous round key.
  • The Sboxes and multiplications use the canonical translation, which has the following number of clauses of each length:
    maxima> ncl_list_full_dualts(16,256);
    [[2,4096],[17,256],[256,1]]
       
  • This instances has 168 boxes = 56 S-boxes + 112 multiplications.
  • This instance has the following number of clauses of length:
    • 1 : 112 = key schedule constant * 1;
    • 2 : 688128 = 168 boxes * 4096;
    • 3 : 320 = 448 additions (arity 2) * 4;
    • 4 : 640 = 40 multiplications by 04 * 16;
    • 6 : 5720 = 40 S-boxes * 143;
    • 7 : 5080 = 40 S-boxes * 127;
    • 8 : 960 = 40 S-boxes * 24.
  • The number of clauses of each length in the translation are:
    • 112 unit-clauses (key schedule constant).
    • 688128 binary clauses (56 Sboxes; 56 multiplications * 2).
    • 3200 ternary clauses (800 arity two additions).
    • 43008 clauses of length seventeen (56 Sboxes; 56 multiplications * 2).
    • 168 clauses of length 256 (56 Sboxes; 56 multiplications * 2).
  • Generate random assignments for the plaintext and ciphertext, leaving the key unknown:
    maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
       
    Merge the assignments with the translations:
    shell> AppendDimacs-O3-DNDEBUG ssaes_r14_c1_rw2_e4_f0.cnf ssaes_pkpair_r14_c1_rw2_e4_f0_s1.cnf > r14_keyfind.cnf; done
       
  • All solvers solve in < 20 minutes:
    • precosat236
      shell> precosat236 r14_keyfind.cnf
      c 56022 conflicts, 304526 decisions, 163 random
      c 0 iterations, 172 restarts, 0 skipped
      c 181.9 seconds, 148 MB max, 10 MB recycled
           
    • cryptominisat:
      shell> cryptominisat r14_keyfind.cnf
      c restarts                 : 168
      c conflicts                : 43829       (239.90    / sec)
      c decisions                : 67335       (1.98      % random)
      c CPU time                 : 182.70      s
           
    • minisat-2.2.0:
      shell> minisat-2.2.0 r14_keyfind.cnf
      restarts              : 253
      conflicts             : 82374          (368 /sec)
      decisions             : 324814         (0.00 % random) (1452 /sec)
      propagations          : 1071399042     (4790302 /sec)
      CPU time              : 223.66 s
           
    • precosat-570.1:
      shell> precosat-570.1 r14_keyfind.cnf
      c 90715 conflicts, 351716 decisions, 176 random
      c 0 iterations, 1931 restarts, 0 skipped
      c 570.7 seconds, 75 MB max, 27 MB recycled
           
    • glucose:
      shell> glucose r14_keyfind.cnf
      <snip>
      c restarts              : 693
      c conflicts             : 404866         (478 /sec)
      c decisions             : 2156003        (1.81 % random) (2545 /sec)
      c propagations          : 1254906184     (1481240 /sec)
      c CPU time              : 847.2 s
           
  • We can check we get the right result with:
    shell> OKsolver_2002-O3-DNDEBUG -O r14_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 1 2 8 0 && echo "VALID"
    VALID
       
Todo:
Using the "minimum" box translation
  • Translation of aes(14,2,1,8):
  • The CNFs for the Sbox and multiplications:
    /* Multiplication by 02: */
    maxima> FieldMul2CNF : [{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16},{{-9,2},{-2,9},{-10,3},{-3,10},{-11,4},{-4,11},{-12,-5,-1},{-12,1,5},{-5,1,12},{-1,5,12},{-13,-6,-1},{-1,6,13},{-14,7},{-7,14},{-15,1,8},{-8,1,15},{-16,-15,-8},{-16,8,15},{-13,6,16},{-6,13,16}}]$
    set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
    /* Multiplication by 03: */
    maxima> FieldMul3CNF :
     [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
      [{-9,-2,-1},{-2,1,9},{-10,2,3},{-10,-9,-3,1},{-10,-3,-1,9},{-3,2,10},{-9,1,3,10},{-1,3,9,10},{-11,-4,-3},{-11,3,4},{-4,3,11},{-3,4,11},{-12,-5,-4,1},{-12,-4,-1,5},{-5,1,4,12},{-1,4,5,12},{-13,-5,-1,6},{-13,1,5,6},{-13,-12,-6,4},{-13,-6,-4,12},{-6,-5,-1,13},{-6,1,5,13},
       {-12,4,6,13},{-4,6,12,13},{-14,-7,-6},{-14,6,7},{-7,6,14},{-6,7,14},{-16,-8,-1},{-16,1,8},{-16,-15,-7},{-16,7,15},{-8,1,16},{-1,8,16},{-15,7,16},{-7,15,16}]]$
    set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
    /* Sbox: */
    maxima> output_rijnsbox_fullcnf_stdname();
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
    shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 40000000 -wtarget 294 -solve 1 -seed 3213901809 -i AES_Sbox_shg.wcnf -r model AES_Sbox_s294.ass;
    shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
    maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
    maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
       
  • Generating small scale AES for 14 + 1/3 rounds:
    rounds : 14$
    num_rows : 2$
    num_columns : 1$
    exp : 8$
    final_round_b : false$
    box_tran : aes_small_box$
    seed : 1$
    mc_tran : aes_mc_bidirectional$
    output_ss_fcl_std(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
    
    shell> cat ssaes_r14_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    2064 22912 128152 0 128152 2065 1
     length count
    1 112
    2 448
    3 4992
    4 896
    6 8008
    7 7112
    8 1344
       
  • In this translation, we have:
    • 14 full rounds (Key Addition, SubBytes, and MixColumns operation).
    • 56 Sboxes:
      • 28 from SubBytes = 2 byte * 14 rounds;
      • 28 from key schedule = 2 row * 1 byte * 14 rounds.
    • 56 multiplications by 02: 2 rows * 1 multiplication * 1 columns * 14 rounds * 2 directions (forward + inverse).
    • 56 multiplications by 03: 2 rows * 1 multiplication * 1 columns * 14 rounds * 2 directions (forward + inverse).
    • 800 additions of arity 2:
      • 224 from key additions = 16 bits * 14 rounds;
      • 16 from final key addition = 16 bits;
      • 112 from the key schedule = 1 rows * 8 bits * 14 rounds.
      • 224 from forward MixColumns = 2 rows * 1 column * 8 bits * 14 rounds;
      • 224 from inverse MixColumns = 2 rows * 1 column * 8 bits * 14 rounds.
    • 112 bits for the constant in the key schedule = 8 bits * 14 rounds.
  • Note that as this variant has only one column, the key schedule applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and K_j are key words from the previous round key.
  • The Sboxes and multiplications use the "minimum" translations, which have the following number of clauses of each length:
    maxima> ncl_list_fcs(ev_hm(ss_sbox_cnfs,8));
    [[6,143],[7,127],[8,24]]
    maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,2]))
    [[2,8],[3,12]]
    maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,3]))
    [[3,20],[4,16]]
       
  • This instance has the following number of clauses of length:
    • 1 : 112 = key schedule constant * 1;
    • 2 : 448 = 56 multiplications by 02 * 8;
    • 3 : 4992 = 56 multiplications by 02 * 12 + 56 multiplications by 03 20 + 800 additions (arity 2) * 4;
    • 4 : 896 = 56 multiplications by 04 * 16;
    • 6 : 8008 = 56 S-boxes * 143;
    • 7 : 7112 = 56 S-boxes * 127;
    • 8 : 1344 = 56 S-boxes * 24.
  • Generate random assignments for the plaintext and ciphertext, leaving the key unknown:
    maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
       
    Merge the assignments with the translations:
    shell> AppendDimacs-O3-DNDEBUG ssaes_r14_c1_rw2_e4_f0.cnf ssaes_pkpair_r14_c1_rw2_e4_f0_s1.cnf > r14_keyfind.cnf; done
       
  • Solver runs:
    • cryptominisat:
      shell> cryptominisat r14_keyfind.cnf
      <snip>
      c restarts                 : 9433
      c conflicts                : 2030565     (4696.47   / sec)
      c decisions                : 4350327     (1.04      % random)
      c CPU time                 : 432.36      s
           
    • glucose:
      shell> glucose r14_keyfind.cnf
      <snip>
      c restarts              : 918
      c conflicts             : 2226769        (2807 /sec)
      c decisions             : 2781657        (1.75 % random) (3507 /sec)
      c propagations          : 136974745      (172675 /sec)
      c CPU time              : 793.25 s
           
  • We can check we get the right result with:
    shell> OKsolver_2002-O3-DNDEBUG -O r14_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 1 2 8 0 && echo "VALID"
    VALID
       

Definition in file 14_13.hpp.