OKlibrary  0.2.1.6
1_13.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 20.5.2011 (Swansea)
00002 /* Copyright 2011, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00308 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}}]$
00309 set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
00310 /* Multiplication by 03: */
00311 maxima> FieldMul3CNF :
00312  [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00313   [{-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},
00314    {-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}]]$
00315 set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
00316 /* Sbox: */
00317 maxima> output_rijnsbox_fullcnf_stdname();
00318 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00319 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00320 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;
00321 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00322 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00323 maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
00324    \endverbatim
00325    </li>
00326    <li> Generating small-scale AES for 1 + 1/3 rounds:
00327    \verbatim
00328 shell> mkdir aes_1_1_8/canon
00329 shell> cd aes_1_1_8/canon
00330 shell> oklib --maxima
00331 oklib_load_all()$
00332 num_rounds : 1$
00333 num_rows : 2$
00334 num_columns : 1$
00335 exp : 8$
00336 final_round_b : false$
00337 box_tran : aes_small_box$
00338 oklib_monitor : true$
00339 mc_tran : aes_mc_bidirectional$
00340 output_ss_fcl_std(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
00341 
00342 shell> cat ssaes_r1_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00343  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00344 3264 52532 154472 0 154472 3265 1
00345  length count
00346  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00347 192 1696 9332 0 9332 193 1
00348  length count
00349 1 8
00350 2 32
00351 3 416
00352 4 64
00353 6 572
00354 7 508
00355 8 96
00356    \endverbatim
00357    </li>
00358    <li> In this translation, we have:
00359     <ul>
00360      <li> 1 full round (Key Addition, SubBytes, and MixColumns operation).
00361      </li>
00362      <li> 4 Sboxes:
00363       <ul>
00364        <li> 2 from SubBytes = 2 byte * 1 round; </li>
00365        <li> 2 from key schedule = 2 row * 1 byte * 1 round. </li>
00366       </ul>
00367      </li>
00368      <li> 4 multiplications by 02: 2 rows * 1 multiplication * 1 columns
00369      * 1 round * 2 directions (forward + inverse). </li>
00370      <li> 4 multiplications by 03: 2 rows * 1 multiplication * 1 columns
00371      * 1 round * 2 directions (forward + inverse). </li>
00372      <li> 72 additions:
00373       <ul>
00374        <li> 16 from key additions = 16 bits * 1 round; </li>
00375        <li> 16 from final key addition = 16 bits; </li>
00376        <li> 8 from the key schedule = 1 rows * 8 bits * 1 round. </li>
00377        <li> 16 from forward MixColumns = 2 rows * 1 column * 8 bits *
00378        1 round; </li>
00379        <li> 16 from inverse MixColumns = 2 rows * 1 column * 8 bits * 1
00380        round. </li>
00381       </ul>
00382      </li>
00383      <li> 8 bits for the constant in the key schedule. </li>
00384     </ul>
00385    </li>
00386    <li> Note that as this variant has only one column, the key schedule
00387    applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and
00388    K_j are key words from the previous round key. </li>
00389    <li> The Sboxes and multiplications use the "minimum" translations,
00390    which have the following number of clauses of each length:
00391    \verbatim
00392 maxima> ncl_list_fcs(ev_hm(ss_sbox_cnfs,8));
00393 [[6,143],[7,127],[8,24]]
00394 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,2]))
00395 [[2,8],[3,12]]
00396 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,3]))
00397 [[3,20],[4,16]]
00398    \endverbatim
00399    </li>
00400    <li> This instance has the following number of clauses of length:
00401     <ul>
00402      <li> 1 : 8 = key schedule constant * 1; </li>
00403      <li> 2 : 32 = 4 multiplications by 02 * 8; </li>
00404      <li> 3 : 416 = 4 multiplications by 02 * 12 + 4 multiplications by 03 * 20
00405      +  72 additions (arity 2) * 4; </li>
00406      <li> 4 : 64 = 4 multiplications by 03 * 16; </li>
00407      <li> 6 : 572 = 4 S-boxes * 143; </li>
00408      <li> 7 : 508 = 4 S-boxes * 127; </li>
00409      <li> 8 : 96 = 4 S-boxes * 24. </li>
00410     </ul>
00411    </li>
00412    <li> Generate random assignments for the plaintext and ciphertext, leaving
00413    the key unknown with a single plaintext-ciphertext-pair:
00414     <ul>
00415      <li> Generate random assignments for the plaintext and ciphertext, leaving
00416      the key unknown:
00417      \verbatim
00418 maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
00419      \endverbatim
00420      Merge the assignments with the translations:
00421      \verbatim
00422 shell> AppendDimacs-O3-DNDEBUG ssaes_r1_c1_rw2_e4_f0.cnf ssaes_pkpair_r1_c1_rw2_e4_f0_s1.cnf > r1_keyfind.cnf; done
00423      \endverbatim
00424      </li>
00425      <li> All solvers solve in <1s:
00426       <ul>
00427        <li> precosat236
00428        \verbatim
00429 shell> precosat236 r1_keyfind.cnf
00430 c 2084 conflicts, 2673 decisions, 1 random
00431 c 0 iterations, 3 restarts, 10 skipped
00432 c prps: 29841 propagations, 0.99 megaprops
00433 c 0.0 seconds, 0 MB max, 0 MB recycled
00434        \endverbatim
00435        </li>
00436        <li> precosat-570.1:
00437        \verbatim
00438 shell> precosat-570.1 r1_keyfind.cnf
00439 c 2899 conflicts, 3880 decisions, 0 random
00440 c 1 iterations, 28 restarts, 43 skipped
00441 c 0.0 seconds, 0 MB max, 0 MB recycled
00442        \endverbatim
00443        </li>
00444        <li> minisat-2.2.0:
00445        \verbatim
00446 shell> minisat-2.2.0 r1_keyfind.cnf
00447 restarts              : 11
00448 conflicts             : 1684           (168400 /sec)
00449 decisions             : 1938           (0.00 % random) (193800 /sec)
00450 propagations          : 23607          (2360700 /sec)
00451 CPU time              : 0.01 s
00452        \endverbatim
00453        </li>
00454        <li> cryptominisat:
00455        \verbatim
00456 shell> cryptominisat r1_keyfind.cnf
00457 c restarts                 : 6
00458 c conflicts                : 1827        (60900.00  / sec)
00459 c decisions                : 2367        (0.00      % random)
00460 c CPU time                 : 0.03        s
00461        \endverbatim
00462        </li>
00463        <li> glucose:
00464        \verbatim
00465 shell> glucose r1_keyfind.cnf
00466 <snip>
00467 c restarts              : 1
00468 c conflicts             : 5583           (62033 /sec)
00469 c decisions             : 5897           (1.56 % random) (65522 /sec)
00470 c propagations          : 114998         (1277756 /sec)
00471 c CPU time              : 0.09 s
00472        \endverbatim
00473        </li>
00474        <li> OKsolver_2002:
00475        \verbatim
00476 shell> OKsolver_2002-O3-DNDEBUG r1_keyfind.cnf
00477 c running_time(sec)                     2.2
00478 c number_of_nodes                       21651
00479 c number_of_single_nodes                4
00480 c number_of_2-reductions                39101
00481 c number_of_missed_single_nodes         4
00482        \endverbatim
00483        </li>
00484       </ul>
00485      </li>
00486      <li> We can check we get the right result with:
00487      \verbatim
00488 shell> OKsolver_2002-O3-DNDEBUG -O r1_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 1 2 8 0 && echo "VALID"
00489 VALID
00490      \endverbatim
00491      </li>
00492     </ul>
00493    </li>
00494    <li> Generating 20 random plaintext-ciphertext-pairs and running
00495    solvers instances instantiated with these pairs to find the key:
00496     <ul>
00497      <li> Computing the random plaintext-ciphertext-pairs:
00498      \verbatim
00499 for seed : 1 thru 20 do output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
00500      \endverbatim
00501      </li>
00502      <li> Running minisat-2.2.0:
00503      \verbatim
00504 shell> col=1; row=2; e=8; r=1; for s in $(seq 1 5); do
00505   for k in $(seq 1 20); do
00506     echo "Seed ${s}; Key ${k} Round ${r}";
00507     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c${col}_rw${row}_e${e}_f0.cnf ssaes_pcpair_r${r}_c${col}_rw${row}_e${e}_f0_s${k}.cnf | RandomShuffleDimacs-O3-DNDEBUG $s > r${r}_k${k}_s${s}.cnf;
00508     minisat-2.2.0 r${r}_k${k}_s${s}.cnf > minisat_r${r}_k${k}_s${s}.result 2>&1;
00509   done;
00510 done;
00511 shell> echo "n  c  t  sat  cfs dec rts r1 mem ptime stime cfl r k s" > minisat_results; for s in $(seq 1 5); do
00512   for k in $(seq 1 20); do
00513     cat minisat_r${r}_k${k}_s${s}.result | awk -f $OKlib/Experimentation/ExperimentSystem/SolverMonitoring/ExtractMinisat.awk | awk " { print \$0 \"  $r  $k $s\" }";
00514   done;
00515 done >> minisat_results;
00516      \endverbatim
00517      yields:
00518      \verbatim
00519 shell> oklib --R
00520 E = read.table("minisat_results", header=TRUE)
00521 EM = aggregate(E, by=list(r=E$r), FUN=mean)
00522 EM
00523   r   n       c      t sat     cfs     dec  rts       r1 mem ptime stime
00524 1 1 192 1646.96 0.0096   1 1578.48 1836.57 9.69 22142.69  19     0 5e-04
00525        cfl r    k s
00526 1 15286.49 1 10.5 3
00527      \endverbatim
00528      </li>
00529      <li> Running OKsolver_2002:
00530      \verbatim
00531 shell> col=1; row=2; e=8; r=1; for s in $(seq 1 5); do
00532   for k in $(seq 1 20); do
00533     echo "Seed ${s}; Key ${k} Round ${r}";
00534     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c${col}_rw${row}_e${e}_f0.cnf ssaes_pcpair_r${r}_c${col}_rw${row}_e${e}_f0_s${k}.cnf | RandomShuffleDimacs-O3-DNDEBUG $s > r${r}_k${k}_s${s}.cnf;
00535     OKsolver_2002-O3-DNDEBUG r${r}_k${k}_s${s}.cnf > oksolver_r${r}_k${k}_s${s}.result 2>&1;
00536   done;
00537 done;
00538 shell> echo "n  c  l  t  sat  nds  r1  r2  pls  ats h file n2cr  dmcl dn  dc  dl snds qnds mnds  tel  oats  n2cs  m2cs r k s" > oksolver_results; for s in $(seq 1 5); do
00539   for k in $(seq 1 20); do
00540     cat oksolver_r${r}_k${k}_s${s}.result | awk -f $OKlib/Experimentation/ExperimentSystem/SolverMonitoring/ExtractOKsolver.awk | awk " { print \$0 \"  $r  $k $s\" }";
00541   done;
00542 done >> oksolver_results;
00543      \endverbatim
00544      yields:
00545      \verbatim
00546 shell> oklib --R
00547 E = read.table("oksolver_results", header=TRUE)
00548 EM = aggregate(E, by=list(r=E$r), FUN=mean)
00549 EM
00550   r   n    c    l     t sat      nds r1       r2 pls ats    h file n2cr dmcl dn
00551 1 1 192 1728 9364 1.448   1 12638.98 40 23778.04   0   0 16.3   NA  112    0 40
00552    dc  dl snds qnds mnds tel oats n2cs m2cs r    k s
00553 1 120 360 2.93    0 2.01   0    0    0    0 1 10.5 3
00554      \endverbatim
00555      </li>
00556     </ul>
00557    </li>
00558   </ul>
00559 
00560 
00561   \todo Using the 1-base box translation
00562   <ul>
00563    <li> Translation of aes(1,2,1,8):
00564     <ul>
00565      <li> The MixColumns operation is decomposed into its field
00566      multiplications (02 and 03) and addition operations. </li>
00567      <li> The MixColumns operation is translated by translating both
00568      the MixColumns operation and its inverse (it is self-inverse). </li>
00569      <li> We treat S-boxes, field multiplications and additions as boxes.
00570      </li>
00571      <li> The S-box and field multiplications are considered as a 16x1
00572      boolean function, translated using 1-bases;
00573      see ss_sbox_rbase_cnfs in
00574      ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SmallScaleSboxCNF.mac
00575      and ss_field_rbase_cnfs in
00576      ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SmallScaleFieldMulCNF.mac.
00577      </li>
00578      <li> Additions of arity k are considered bit-wise as (k+1)-bit to 1-bit
00579      boolean functions; translated using their prime implicates. </li>
00580     </ul>
00581    </li>
00582    <li> Generating a 1-base for the S-box from
00583    Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp. :
00584    \verbatim
00585 maxima> output_rijnsbox_fullcnf_stdname();
00586 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_pi.cnf
00587 shell> RandomShuffleDimacs-O3-DNDEBUG 103 < AES_Sbox_pi.cnf | SortByClauseLength-O3-DNDEBUG > AES_Sbox_sortedpi.cnf
00588 shell> RUcpGen-O3-DNDEBUG AES_Sbox_sortedpi.cnf > AES_Sbox_gen.cnf
00589 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_Sbox_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_Sbox_base.cnf
00590 shell> cat AES_Sbox_base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00591  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00592 16 4398 30108 0 30108 0 1
00593  length count
00594 5 1
00595 6 1187
00596 7 2703
00597 8 503
00598 9 4
00599    \endverbatim
00600    </li>
00601    <li> Generating a 1-base for the multiplication by 02 and 03 from
00602    Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp. :
00603    \verbatim
00604 maxima> output_rijn_mult_fullcnf_stdname(2);
00605 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_2.cnf > AES_byte_field_mul_2_pi.cnf
00606 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_byte_field_mul_2_pi.cnf | SortByClauseLength-O3-DNDEBUG > AES_byte_field_mul_2_sortedpi.cnf
00607 shell> RUcpGen-O3-DNDEBUG AES_byte_field_mul_2_sortedpi.cnf > AES_byte_field_mul_2_gen.cnf
00608 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_byte_field_mul_2_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_byte_field_mul_2_base.cnf
00609 shell> cat AES_byte_field_mul_2_base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00610  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00611 16 22 56 0 56 0 1
00612  length count
00613 2 10
00614 3 12
00615 maxima> output_rijn_mult_fullcnf_stdname(3);
00616 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_byte_field_mul_full_3.cnf > AES_byte_field_mul_3_pi.cnf
00617 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_byte_field_mul_3_pi.cnf | SortByClauseLength-O3-DNDEBUG > AES_byte_field_mul_3_sortedpi.cnf
00618 shell> RUcpGen-O3-DNDEBUG AES_byte_field_mul_3_sortedpi.cnf > AES_byte_field_mul_3_gen.cnf
00619 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_byte_field_mul_3_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_byte_field_mul_3_base.cnf
00620 shell> cat AES_byte_field_mul_3_base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00621  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00622 16 80 328 0 328 0 1
00623  length count
00624 3 24
00625 4 24
00626 5 32
00627    \endverbatim
00628    </li>
00629    <li> Translating the AES cipher treating Sboxes and field multiplications
00630    as whole boxes and translating these boxes using 1-bases.
00631    </li>
00632    <li> Generating small-scale AES for 1 + 1/3 rounds:
00633    \verbatim
00634 shell> mkdir aes_1_1_8/canon
00635 shell> cd aes_1_1_8/canon
00636 shell> oklib --maxima
00637 oklib_load_all()$
00638 num_rounds : 1$
00639 num_rows : 2$
00640 num_columns : 1$
00641 exp : 8$
00642 final_round_b : false$
00643 box_tran : aes_rbase_box$
00644 oklib_monitor : true$
00645 mc_tran : aes_mc_bidirectional$
00646 set_hm(ss_sbox_rbase_cnfs,8,read_fcl_f("AES_Sbox_base.cnf"))$
00647 set_hm(ss_field_rbase_cnfs,[8,2],read_fcl_f("AES_byte_field_mul_2_base.cnf"))$
00648 set_hm(ss_field_rbase_cnfs,[8,3],read_fcl_f("AES_byte_field_mul_3_base.cnf"))$
00649 output_ss_fcl_std(num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
00650 
00651 shell> cat ssaes_r1_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00652  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00653 192 18296 122840 0 122840 193 1
00654  length count
00655 1 8
00656 2 40
00657 3 432
00658 4 96
00659 5 132
00660 6 4748
00661 7 10812
00662 8 2012
00663 9 16
00664    \endverbatim
00665    </li>
00666    <li> In this translation, we have:
00667     <ul>
00668      <li> 1 full round (Key Addition, SubBytes, and MixColumns operation).
00669      </li>
00670      <li> 4 Sboxes:
00671       <ul>
00672        <li> 2 from SubBytes = 2 byte * 1 round; </li>
00673        <li> 2 from key schedule = 2 row * 1 byte * 1 round. </li>
00674       </ul>
00675      </li>
00676      <li> 4 multiplications by 02: 2 rows * 1 multiplication * 1 columns
00677      * 1 round * 2 directions (forward + inverse). </li>
00678      <li> 4 multiplications by 03: 2 rows * 1 multiplication * 1 columns
00679      * 1 round * 2 directions (forward + inverse). </li>
00680      <li> 72 additions:
00681       <ul>
00682        <li> 32 additions of arity 3:
00683         <ul>
00684          <li> 16 from forward MixColumns = 2 rows * 1 column * 8 bits *
00685          1 round; </li>
00686          <li> 16 from inverse MixColumns = 2 rows * 1 column * 8 bits * 1
00687          round. </li>
00688         </ul>
00689        </li>
00690        <li> 40 additions of arity 2:
00691         <ul>
00692          <li> 16 from key additions = 16 bits * 1 round; </li>
00693          <li> 16 from final key addition = 16 bits; </li>
00694          <li> 8 from the key schedule = 1 rows * 8 bits * 1 round. </li>
00695         </ul>
00696        </li>
00697       </ul>
00698      </li>
00699      <li> 8 bits for the constant in the key schedule. </li>
00700     </ul>
00701    </li>
00702    <li> Note that as this variant has only one column, the key schedule
00703    applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and
00704    K_j are key words from the previous round key. </li>
00705    <li> The Sboxes and multiplications use 1-base translations,
00706    which have the following number of clauses of each length:
00707    \verbatim
00708 maxima> ncl_list_fcs(ev_hm(ss_sbox_rbase_cnfs,8));
00709 [[5,1],[6,1187],[7,2703],[8,503],[9,4]]
00710 maxima> ncl_list_fcs(ev_hm(ss_field_rbase_cnfs,[8,2]))
00711 [[2,10],[3,12]]
00712 maxima> ncl_list_fcs(ev_hm(ss_field_rbase_cnfs,[8,3]))
00713 [[3,24],[4,24],[5,32]]
00714    \endverbatim
00715    </li>
00716    <li> This instance has the following number of clauses of length:
00717     <ul>
00718      <li> 1 : 8 = key schedule constant * 1; </li>
00719      <li> 2 : 40 = 4 multiplications by 02 * 10; </li>
00720      <li> 3 : 432 = 4 multiplications by 02 * 12 + 4 multiplications by 03 * 24
00721      + 72 additions (arity 2) * 4; </li>
00722      <li> 4 : 96 = 4 multiplications by 03 * 24; </li>
00723      <li> 5 : 132 = 4 S-boxes * 1 + 4 multiplications by 03 * 32; </li>
00724      <li> 6 : 4748 = 4 S-boxes * 1187; </li>
00725      <li> 7 : 10812 = 4 S-boxes * 2703; </li>
00726      <li> 8 : 2012 = 4 S-boxes * 503; </li>
00727      <li> 9 : 16 = 4 S-boxes * 4. </li>
00728     </ul>
00729    </li>
00730    <li> Generating 20 random plaintext-ciphertext-pairs and running
00731    solvers instances instantiated with these pairs to find the key:
00732     <ul>
00733      <li> Computing the random plaintext-ciphertext-pairs:
00734      \verbatim
00735 for seed : 1 thru 20 do output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
00736      \endverbatim
00737      </li>
00738      <li> Running minisat-2.2.0:
00739      \verbatim
00740 shell> col=1; row=2; e=8; r=1; for s in $(seq 1 5); do
00741   for k in $(seq 1 20); do
00742     echo "Seed ${s}; Key ${k} Round ${r}";
00743     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c${col}_rw${row}_e${e}_f0.cnf ssaes_pcpair_r${r}_c${col}_rw${row}_e${e}_f0_s${k}.cnf | RandomShuffleDimacs-O3-DNDEBUG $s > r${r}_k${k}_s${s}.cnf;
00744     minisat-2.2.0 r${r}_k${k}_s${s}.cnf > minisat_r${r}_k${k}_s${s}.result 2>&1;
00745   done;
00746 done;
00747 shell> echo "n  c  t  sat  cfs dec rts r1 mem ptime stime cfl r k s" > minisat_results; for s in $(seq 1 5); do
00748   for k in $(seq 1 20); do
00749     cat minisat_r${r}_k${k}_s${s}.result | awk -f $OKlib/Experimentation/ExperimentSystem/SolverMonitoring/ExtractMinisat.awk | awk " { print \$0 \"  $r  $k $s\" }";
00750   done;
00751 done >> minisat_results;
00752      \endverbatim
00753      yields:
00754      \verbatim
00755 shell> oklib --R
00756 E = read.table("minisat_results", header=TRUE)
00757 EM = aggregate(E, by=list(r=E$r), FUN=mean)
00758 EM
00759   r   n        c      t sat    cfs    dec  rts       r1 mem  ptime stime
00760 1 1 192 18248.62 0.5836   1 335.81 363.35 3.33 14769.97  20 0.0066 0.551
00761       cfl r    k s
00762 1 2638.52 1 10.5 3
00763      \endverbatim
00764      </li>
00765      <li> Running OKsolver_2002:
00766      \verbatim
00767 shell> col=1; row=2; e=8; r=1; for s in $(seq 1 5); do
00768   for k in $(seq 1 20); do
00769     echo "Seed ${s}; Key ${k} Round ${r}";
00770     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c${col}_rw${row}_e${e}_f0.cnf ssaes_pcpair_r${r}_c${col}_rw${row}_e${e}_f0_s${k}.cnf | RandomShuffleDimacs-O3-DNDEBUG $s > r${r}_k${k}_s${s}.cnf;
00771     OKsolver_2002-O3-DNDEBUG r${r}_k${k}_s${s}.cnf > oksolver_r${r}_k${k}_s${s}.result 2>&1;
00772   done;
00773 done;
00774 shell> echo "n  c  l  t  sat  nds  r1  r2  pls  ats h file n2cr  dmcl dn  dc  dl snds qnds mnds  tel  oats  n2cs  m2cs r k s" > oksolver_results; for s in $(seq 1 5); do
00775   for k in $(seq 1 20); do
00776     cat oksolver_r${r}_k${k}_s${s}.result | awk -f $OKlib/Experimentation/ExperimentSystem/SolverMonitoring/ExtractOKsolver.awk | awk " { print \$0 \"  $r  $k $s\" }";
00777   done;
00778 done >> oksolver_results;
00779      \endverbatim
00780      yields:
00781      \verbatim
00782 shell> oklib --R
00783 E = read.table("oksolver_results", header=TRUE)
00784 EM = aggregate(E, by=list(r=E$r), FUN=mean)
00785 EM
00786   r   n     c      l     t sat    nds r1     r2 pls ats    h file n2cr dmcl dn
00787 1 1 192 18328 122872 2.572   1 620.29 40 913.57   0 0.3 11.8   NA  120    0 40
00788    dc  dl snds qnds mnds tel oats n2cs m2cs r    k s
00789 1 120 360 0.26    0 0.26   0    0    0    0 1 10.5 3
00790      \endverbatim
00791      </li>
00792     </ul>
00793    </li>
00794   </ul>
00795 
00796 */