OKlibrary  0.2.1.6
1_13.hpp File Reference

Investigations into small-scale AES key discovery with 1 row, 1 column and 4-bit field elements for 1 round AES (1+1/3) More...

Go to the source code of this file.


Detailed Description

Investigations into small-scale AES key discovery with 1 row, 1 column and 4-bit field elements for 1 round AES (1+1/3)

Todo:
Overview
Todo:
Using the canonical box translation
  • Translation of aes(1,1,1,4):
  • Generating simplest small-scale AES for 1 round
    num_rounds : 1$
    num_rows : 1$
    num_columns : 1$
    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_c1_rw1_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    68 358 1012 0 1012 69 1
     length count
    1 4
    2 272
    3 48
    9 32
    16 2
       
  • In this translation, we have:
    • 1 full round (Key Addition, SubBytes, and MixColumns operation).
    • 2 Sboxes:
      • 1 from SubBytes = 1 byte * 1 round;
      • 1 from key schedule = 1 row * 1 byte * 1 round.
    • 20 additions:
      • 8 additions of arity 1:
        • 4 from forward MixColumns = 4 bits * 1 round;
        • 4 from inverse MixColumns = 4 bits * 1 rounds.
      • 12 additions of arity 2:
        • 4 from key additions = 4 bits * 1 round;
        • 4 from final key addition = 4 bits;
        • 4 from the key schedule = 4 bits * 1 rounds.
    • 4 bits for the constant in the key schedule.
  • The additions are translated by their prime implicates, containing 2^a clauses where a is the arity of the addition constraint.
  • The Sbox is translated by the canonical-translation:
    > ncl_list_fcl(dualts_fcl(ss_sbox_fulldnf_fcl(2,4,ss_polynomial_2_4)));
    [[2,128],[9,16],[16,1]]
       
  • This instance has the following number of clauses of length:
    • 1 : 4 = key schedule constant * 1;
    • 2 : 272 = 2 S-boxes * 128 + 8 "additions" (arity 1) * 2;
    • 3 : 48 = 12 additions (arity 2) * 4;
    • 9 : 32 = 2 S-boxes * 16;
    • 16 : 2 = 2 S-boxes * 1.
  • 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_c1_rw1_e4_f0.cnf ssaes_pcpair_r1_c1_rw1_e4_f0_s1.cnf > r1_keyfind.cnf
       
  • OKsolver solves this with no decisions:
    shell> OKsolver_2002-O3-DNDEBUG r1_keyfind.cnf
    c running_time(sec)                     0.0
    c number_of_nodes                       1
    c number_of_2-reductions                19
    c number_of_autarkies                   1
    c file_name                             r1_keyfind.cnf
       
  • However, minisat-2.2.0 and glucose need to branch:
    shell> minisat-2.2.0 r1_keyfind.cnf
    <snip>
    restarts              : 1
    conflicts             : 7              (inf /sec)
    decisions             : 14             (0.00 % random) (inf /sec)
    propagations          : 198            (inf /sec)
    CPU time              : 0 s
    shell> minisat2 r1_keyfind.cnf
    <snip>
    restarts              : 1
    conflicts             : 13             (inf /sec)
    decisions             : 21             (0.00 % random) (inf /sec)
    propagations          : 286            (inf /sec)
    CPU time              : 0 s
    shell> glucose r1_keyfind.cnf
    <snip>
    c restarts              : 1
    c conflicts             : 12             (inf /sec)
    c decisions             : 32             (0.00 % random) (inf /sec)
    c propagations          : 215            (inf /sec)
    c CPU time              : 0 s
       
  • It seems OKsolver is propagating purely by r_2. Perhaps the OKsolver is able to take advantage of the r_1-basedness of the canonical translation due to its use of r_2 reductions?
  • 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 1 1 4 0 && echo "VALID"
    VALID
       

Definition in file 1_13.hpp.