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 4x2 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 4x2 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
Todo:
Using the canonical box translation
  • Translation of aes(1,4,2,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.
    • 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 : 4$
    num_columns : 2$
    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_c2_rw4_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    1396 10128 31316 0 31316 1397 1
     length count
    1 4
    2 7680
    3 368
    4 32
    5 1024
    9 960
    16 60
       
  • In this translation, we have:
    • 1 full round (Key Addition, SubBytes, and MixColumns operation).
    • 12 S-boxes:
      • 8 from SubBytes = 8 byte * 1 rounds;
      • 4 from key schedule = 4 row * 1 word * 1 rounds.
    • 8 multiplications by 02 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 direction (forward).
    • 8 multiplications by 03 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (forward).
    • 8 multiplications by 09 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
    • 8 multiplications by 11 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
    • 8 multiplications by 13 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
    • 8 multiplications by 14 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
    • 160 additions:
      • 92 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.
      • 4 additions of arity 3:
        • 4 from the key schedule = 4 bits * 1 rounds.
      • 64 additions of arity 4:
        • 32 from forward MixColumns = 4 rows * 2 column * 4 bits * 1 rounds;
        • 32 from inverse MixColumns = 4 rows * 2 column * 4 bits * 1 rounds.
    • 4 bits for the constant in the key schedule = 4 bits * 1 rounds.
  • The number of clauses of each length in the translation, computed by:
    maxima> ncl_list_full_dualts(8,16);
    [[2,128],[9,16],[16,1]]
       
  • This instance has 60 boxes = 12 S-boxes + 48 multiplications.
  • This instance has the following number of clauses of length:
    • 1 : 4 = key schedule constant * 1;
    • 2 : 7680 = 60 boxes * 128;
    • 3 : 368 = 92 additions (arity 2) * 4;
    • 4 : 32 = 4 additions (arity 3) * 8;
    • 5 : 1024 = 64 additions (arity 4) * 16;
    • 9 : 960 = 60 boxes * 16;
    • 16 : 60 = 60 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_c2_rw4_e4_f0.cnf ssaes_pkpair_r1_c2_rw4_e4_f0_s1.cnf > r1_keyfind.cnf
       
  • OKsolver_2002:
    shell> OKsolver_2002-O3-DNDEBUG r1_keyfind.cnf
    c running_time(sec)                     42.8
    c number_of_nodes                       2915
    c number_of_2-reductions                25478
       
  • minisat-2.2.0 and glucose:
    shell> minisat-2.2.0 r1_keyfind.cnf
    restarts              : 126
    conflicts             : 38174          (11967 /sec)
    decisions             : 41318          (0.00 % random) (12952 /sec)
    propagations          : 15523483       (4866296 /sec)
    CPU time              : 3.19 s
    
    shell> minisat2 r1_keyfind.cnf
    <snip>
    restarts              : 14
    conflicts             : 43604          (1401 /sec)
    decisions             : 47364          (1.34 % random) (1522 /sec)
    propagations          : 17037471       (547477 /sec)
    CPU time              : 31.12 s
    shell> glucose r1_keyfind.cnf
    <snip>
    c restarts              : 8
    c conflicts             : 16554          (13035 /sec)
    c decisions             : 21834          (1.56 % random) (17192 /sec)
    c propagations          : 3407020        (2682693 /sec)
    c CPU time              : 1.27 s
       
  • We can check we get the right result with:
    shell> OKsolver_2002-O3-DNDEBUG -O r1_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 2 4 4 0 && echo "VALID"
    VALID
       

Definition in file 1_13.hpp.