OKlibrary  0.2.1.6
4_13.hpp File Reference

Investigations into small-scale AES key discovery for 4 + 1/3 round AES with a 2x2 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 4 + 1/3 round AES with a 2x2 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
Todo:
Using the canonical box translation
  • Translation of aes(4,2,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 (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 4 + 1/3 rounds:
    rounds : 4$
    num_rows : 2$
    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(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
    
    shell> cat ssaes_r4_c2_rw2_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    2016 13928 40208 0 40208 2017 1
     length count
    1 16
    2 11264
    3 1024
    4 128
    9 1408
    16 88
       
  • In this translation, we have:
    • 4 full rounds (Key Addition, SubBytes, and MixColumns operation).
    • 24 Sboxes:
      • 16 from SubBytes = 4 byte * 4 rounds;
      • 8 from key schedule = 2 row * 1 word * 4 rounds.
    • 32 multiplications by 02: 2 rows * 1 multiplication * 2 columns 4 rounds * 2 directions (forward + inverse).
    • 32 multiplications by 03: 2 rows * 1 multiplication * 2 columns 4 rounds * 2 directions (forward + inverse).
    • 144 additions:
      • 256 additions of arity 2:
        • 64 from key additions = 16 bits * 4 rounds;
        • 16 from final key addition = 16 bits;
        • 48 from the key schedule = (16 bits - 4 bits) * 4 rounds.
        • 64 from forward MixColumns = 2 rows * 2 column * 4 bits * 4 rounds;
        • 64 from inverse MixColumns = 2 rows * 2 column * 4 bits * 4 round.
      • 16 additions of arity 3:
        • 16 from the key schedule = 4 bits * 4 round.
    • 16 bits for the constant in the key schedule = 4 bits * 4 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 instances has 88 boxes = 24 S-boxes + 64 multiplications.
  • This instance has the following number of clauses of length:
    • 1 : 16 = key schedule constant * 1;
    • 2 : 11264 = 88 boxes * 128;
    • 3 : 1024 = 256 additions (arity 2) * 4;
    • 4 : 128 = 16 additions (arity 3) * 8;
    • 9 : 1408 = 88 boxes * 16;
    • 16 : 88 = 88 boxes * 1.
  • Then we can generate random assignments with the plaintext and ciphertext, leaving the key unknown:
    maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
       
    and the merging the assignments with the translations:
    shell> AppendDimacs-O3-DNDEBUG ssaes_r4_c2_rw2_e4_f0.cnf ssaes_pkpair_r4_c2_rw2_e4_f0_s1.cnf > r4_keyfind.cnf
       
  • OKsolver solves this with very few decisions:
    shell> OKsolver_2002-O3-DNDEBUG r4_keyfind.cnf
    s SATISFIABLE
    c sat_status                            1
    c initial_maximal_clause_length         16
    c initial_number_of_variables           2016
    c initial_number_of_clauses             13960
    c initial_number_of_literal_occurrences 40240
    c number_of_initial_unit-eliminations   48
    c reddiff_maximal_clause_length         0
    c reddiff_number_of_variables           48
    c reddiff_number_of_clauses             176
    c reddiff_number_of_literal_occurrences 624
    c number_of_2-clauses_after_reduction   11328
    c running_time(sec)                     20.9
    c number_of_nodes                       1246
    c number_of_single_nodes                0
    c number_of_quasi_single_nodes          0
    c number_of_2-reductions                44291
    c number_of_pure_literals               0
    c number_of_autarkies                   0
    c number_of_missed_single_nodes         0
    c max_tree_depth                        17
    c number_of_table_enlargements          0
    c number_of_1-autarkies                 0
    c number_of_new_2-clauses               0
    c maximal_number_of_added_2-clauses     0
    c file_name                             r4_keyfind.cnf
       
  • However, minisat2 and glucose need to branch a lot more:
    shell> minisat2 r4_keyfind.cnf
    <snip>
    Verified 13576 original clauses.
    Verified 976 eliminated clauses.
    restarts              : 12
    conflicts             : 18318          (1104 /sec)
    decisions             : 20892          (1.78 % random) (1259 /sec)
    propagations          : 14693302       (885672 /sec)
    conflict literals     : 514079         (63.22 % deleted)
    Memory used           : 18.46 MB
    CPU time              : 16.59 s
    shell> minisat-2.2.0 r4_keyfind.cnf
    <snip>
    restarts              : 127
    conflicts             : 40470          (7125 /sec)
    decisions             : 45214          (0.00 % random) (7960 /sec)
    propagations          : 36303086       (6391388 /sec)
    conflict literals     : 1250043        (71.04 % deleted)
    Memory used           : 20.00 MB
    CPU time              : 5.68 s
    shell> glucose r4_keyfind.cnf
    <snip>
    c restarts              : 2
    c nb ReduceDB           : 1
    c nb learnts DL2        : 55
    c nb learnts size 2     : 1
    c nb learnts size 1     : 0
    c conflicts             : 6731           (8742 /sec)
    c decisions             : 7756           (1.77 % random) (10073 /sec)
    c propagations          : 2519893        (3272588 /sec)
    c conflict literals     : 286835         (44.78 % deleted)
    c Memory used           : 3.98 MB
    c CPU time              : 0.77 s
       
  • The number of decision nodes used by the OKsolver has jumped drastically here! What has changed?
  • Also note that minisat-2.2.0 does a lot better here than minisat2.
  • We can check we get the right result with:
    shell> OKsolver_2002-O3-DNDEBUG -O r4_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 4 2 2 4 0 && echo "VALID"
    VALID
       

Definition in file 4_13.hpp.