OKlibrary  0.2.1.6
general.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 28.11.2011 (Swansea)
00002 /* Copyright 2011 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 
00112 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}}]$
00113 set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
00114 /* Multiplication by 03: */
00115 maxima> FieldMul3CNF :
00116  [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00117   [{-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},
00118    {-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}]]$
00119 set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
00120 /* Sbox: */
00121 maxima> output_rijnsbox_fullcnf_stdname();
00122 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00123 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00124 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;
00125 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00126 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00127 maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
00128        \endverbatim
00129        </li>
00130        <li> Please see "Computing a minimum CNF represention" in
00131        AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp. </li>
00132        <li> Generating the instances:
00133        \verbatim
00134 shell> mkdir ssaes_r1-20_c3_rw1_e8_f0_k1-1_aes_min_box_aes_mc_bidirectional
00135 shell> cd ssaes_r1-20_c3_rw1_e8_f0_k1-1_aes_min_box_aes_mc_bidirectional
00136 shell> oklib --maxima
00137 num_rows : 1$
00138 num_columns : 3$
00139 exp : 8$
00140 final_round_b : false$
00141 box_tran : aes_small_box$
00142 seed : 1$
00143 mc_tran : aes_mc_bidirectional$
00144 for num_rounds : 1 thru 20 do (
00145   output_ss_fcl_std(
00146     num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran),
00147   for seed : 1 thru 20 do (
00148     output_ss_random_pc_pair(
00149       seed,num_rounds,num_columns,num_rows,exp,final_round_b)))$
00150 exit();
00151 shell> for r in $(seq 1 20); do
00152   for s in $(seq 1 20) do
00153     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c3_rw1_e8_f0.cnf ssaes_pcpair_r${r}_c3_rw1_e4_f0_s${s}.cnf > r${r}_k${s}.cnf;
00154   done
00155 done
00156        \endverbatim
00157        </li>
00158       </ul>
00159      </li>
00160      <li> The 1-base box translation:
00161       <ul>
00162        <li> Generating a 1-base for the S-box from
00163    Cryptography/AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp. :
00164    \verbatim
00165 maxima> output_rijnsbox_fullcnf_stdname();
00166 shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_pi.cnf
00167 shell> RandomShuffleDimacs-O3-DNDEBUG 103 < AES_Sbox_pi.cnf | SortByClauseLength-O3-DNDEBUG > AES_Sbox_sortedpi.cnf
00168 shell> RUcpGen-O3-DNDEBUG AES_Sbox_sortedpi.cnf > AES_Sbox_gen.cnf
00169 shell> RandomShuffleDimacs-O3-DNDEBUG 1 < AES_Sbox_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > AES_Sbox_base.cnf
00170 shell> cat AES_Sbox_base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00171  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00172 16 4398 30108 0 30108 0 1
00173  length count
00174 5 1
00175 6 1187
00176 7 2703
00177 8 503
00178 9 4
00179        \endverbatim
00180        </li>
00181        <li> Please see "r_1-bases" in
00182        AdvancedEncryptionStandard/plans/Representations/Sbox_8.hpp. </li>
00183        <li> Generating the instances:
00184        \verbatim
00185 shell> mkdir ssaes_r1-20_c3_rw1_e8_f0_k1-1_aes_1base_box_aes_mc_bidirectional
00186 shell> cd ssaes_r1-20_c3_rw1_e8_f0_k1-1_aes_1base_box_aes_mc_bidirectional
00187 shell> oklib --maxima
00188 num_rows : 1$
00189 num_columns : 3$
00190 exp : 8$
00191 final_round_b : false$
00192 box_tran : aes_rbase_box$
00193 seed : 1$
00194 mc_tran : aes_mc_bidirectional$
00195 for num_rounds : 1 thru 20 do (
00196   output_ss_fcl_std(
00197     num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran),
00198   for seed : 1 thru 20 do (
00199     output_ss_random_pc_pair(
00200       seed,num_rounds,num_columns,num_rows,exp,final_round_b)))$
00201 exit();
00202 shell> for r in $(seq 1 20); do
00203   for s in $(seq 1 20) do
00204     AppendDimacs-O3-DNDEBUG ssaes_r${r}_c3_rw1_e8_f0.cnf ssaes_pcpair_r${r}_c3_rw1_e4_f0_s${s}.cnf > r${r}_k${s}.cnf;
00205   done
00206 done
00207        \endverbatim
00208        </li>
00209       </ul>
00210      </li>
00211     </ul>
00212    </li>
00213   </ul>
00214 
00215 
00216   \todo Minisat-2.2.0
00217   <ul>
00218    <li> Solving the key discovery problem over rounds 1 to 20. </li>
00219    <li> The canonical box translation:
00220     <ul>
00221      <li> The data:
00222      \verbatim
00223 shell> for r in $(seq 1 20); do for s in $(seq 1 20); do RunMinisat r${r}_k${s}.cnf; done; done
00224 shell> (ExtractMinisat header-only |  awk " { print \$0 \" r s\"}"; for r in $(seq 1 4); do for s in $(seq 1 20); do
00225     cat ExperimentMinisat_r${r}_k${s}cnf_*/Statistics | tail -n 1 | awk " { print \$0 \" ${r} ${s}\"}";
00226   done;
00227 done) > MinisatStatistics
00228 shell> oklib --R
00229 R> E = read.table("MinisatStatistics", header=TRUE)
00230 R> aggregate(E, by=list(r=E$r), FUN=mean)
00231 r   rn    rc            t  sat         cfs         dec      rts           r1    mem  ptime stime          cfl
00232 1 1208 17796 4.749215e-02 1.00      286.95     2730.85     3.05      60556.7   9.00 0.0095  0.02      51757.4
00233 2 2344 35496 1.779539e+01 1.00    69910.15   244117.35   198.00   32444019.8  58.15 0.0120  0.04   14567690.3
00234 3 3480 53196 4.800013e+01 1.00   148693.60   597392.90   387.55   67025301.9 114.40 0.0200  0.06   29870635.6
00235 4 4616 70896 1.121947e+04 1.05 15353353.90 54250682.65 22731.75 5516558000.2 924.35 0.0265  0.08 5309395310.2
00236 R> aggregate_statistics(E[c("r","t","cfs","r1")], by=list("r"))
00237   r       t.mean         t.sd    t.min       t.max    cfs.mean       cfs.sd cfs.min  cfs.max      r1.mean        r1.sd   r1.min      r1.max
00238 1 1 4.749215e-02 1.464625e-02 0.027995 7.39880e-02      286.95     223.0127      14      698      60556.7 4.613163e+04     3393      142167
00239 2 2 1.779539e+01 1.879794e+01 0.057991 5.25750e+01    69910.15   65680.2979      23   213489   32444019.8 3.006823e+07    17318   100808694
00240 3 3 4.800013e+01 4.436927e+01 7.603840 1.87271e+02   148693.60  102529.6673   44744   455063   67025301.9 5.386161e+07 12725413   228186522
00241 4 4 1.121947e+04 8.334966e+03 0.000000 2.81446e+04 15353353.90 9778328.8799       0 35989537 5516558000.2 3.567265e+09        0 13009604735
00242      \endverbatim
00243      Note here that key with seed 4 returned and error, and hence we have
00244      "1.05" for "sat". This experiment must be run again (it errored after
00245      527 minutes). </li>
00246     </ul>
00247    </li>
00248    <li> The "minimum" box translation:
00249     <ul>
00250      <li> The data:
00251      \verbatim
00252 shell> for r in $(seq 1 20); do for s in $(seq 1 20); do RunMinisat r${r}_k${s}.cnf; done; done
00253 shell> (ExtractMinisat header-only |  awk " { print \$0 \" r s\"}"; for r in $(seq 1 4); do for s in $(seq 1 20); do
00254     cat ExperimentMinisat_r${r}_k${s}cnf_*/Statistics | tail -n 1 | awk " { print \$0 \" ${r} ${s}\"}";
00255   done;
00256 done) > MinisatStatistics
00257 shell> oklib --R
00258 R> E = read.table("MinisatStatistics", header=TRUE)
00259 R> aggregate(E, by=list(r=E$r), FUN=mean)
00260 r  rn   rc            t         cfs        dec      rts           r1   mem ptime  stime          cfl
00261 1 184 1560 2.424565e-02     2236.85     2662.7    12.95 2.588565e+04  8.00 0.000 0.0090     21949.85
00262 2 296 3024 4.044634e+00   298957.00   344442.8   695.70 5.702301e+06  8.00 0.000 0.0100   4162284.00
00263 3 408 4488 6.966964e+01  3505260.35  4099517.2  5931.15 9.290159e+07 12.90 0.000 0.0135  60130846.75
00264 4 520 5952 1.281556e+03 26518153.95 30264840.0 36318.30 1.251430e+09 34.55 0.002 0.0200 545569858.95
00265 R> aggregate_statistics(E[c("r","t","cfs","r1")], by=list("r"))
00266 r       t.mean         t.sd    t.min       t.max    cfs.mean       cfs.sd cfs.min  cfs.max      r1.mean        r1.sd  r1.min     r1.max
00267 1 2.424565e-02 1.205448e-02 0.007998    0.048992     2236.85     1653.853     139     5744 2.588565e+04 1.920905e+04    1752      67017
00268 2 4.044634e+00 3.772671e+00 0.038994   13.204000   298957.00   237780.895    3059   822904 5.702301e+06 5.106003e+06   45300   17958522
00269 3 6.966964e+01 8.429120e+01 2.242660  403.495000  3505260.35  3446073.443  187972 16727967 9.290159e+07 1.023211e+08 3601114  492327148
00270 4 1.281556e+03 1.300257e+03 6.483010 4401.220000 26518153.95 23545349.385  385027 79797406 1.251430e+09 1.189224e+09 9342287 3970533106
00271      \endverbatim
00272      </li>
00273     </ul>
00274    </li>
00275    <li> The 1-base box translation:
00276     <ul>
00277      <li> The data:
00278      \verbatim
00279 shell> for r in $(seq 1 20); do for s in $(seq 1 20); do RunMinisat r${r}_k${s}.cnf; done; done
00280 shell> (ExtractMinisat header-only |  awk " { print \$0 \" r s\"}"; for r in $(seq 1 4); do for s in $(seq 1 20); do
00281     cat ExperimentMinisat_r${r}_k${s}cnf_*/Statistics | tail -n 1 | awk " { print \$0 \" ${r} ${s}\"}";
00282   done;
00283 done) > MinisatStatistics
00284 shell> oklib --R
00285 R> E = read.table("MinisatStatistics", header=TRUE)
00286 R> aggregate(E, by=list(r=E$r), FUN=mean)
00287 r  rn    rc            t        cfs        dec      rts           r1    mem  ptime  stime          cfl
00288 1 184 17976    0.5649137      189.9      209.5     2.20      5976.95  10.00 0.0110 0.5300      1329.15
00289 2 296 35856    6.6444390    26194.4    27582.7    92.20   1757050.00  12.35 0.0195 1.1900    392016.80
00290 3 408 53736   68.3752300   432840.7   484224.7   941.70  18866602.75  29.60 0.0295 1.7290   7417296.55
00291 4 520 71616 7500.9050500 16254372.2 17373478.6 22877.95 959566525.75 109.05 0.0395 2.3035 349172967.80
00292 R> aggregate_statistics(E[c("r","t","cfs","r1")], by=list("r"))
00293 r       t.mean         t.sd      t.min       t.max   cfs.mean       cfs.sd cfs.min  cfs.max      r1.mean        r1.sd   r1.min     r1.max
00294 1    0.5649137 1.314491e-02   0.544917     0.59091      189.9 1.200254e+02      12      392      5976.95 3.731548e+03      551      12763
00295 2    6.6444390 4.469542e+00   1.457780    18.09520    26194.4 1.985138e+04    1409    76465   1757050.00 1.357439e+06    90491    5231210
00296 3   68.3752300 6.246889e+01  13.360000   245.36900   432840.7 4.018269e+05   88015  1658292  18866602.75 1.755783e+07  3562554   69228347
00297 4 7500.9050500 1.211908e+04 188.654000 45321.30000 16254372.2 2.536459e+07  733692 97761567 959566525.75 1.507831e+09 43611219 5837203969
00298      \endverbatim
00299      </li>
00300     </ul>
00301    </li>
00302   </ul>
00303 
00304 */