OKlibrary  0.2.1.6
6.hpp File Reference

On investigations into the 6-round Data Encryption Standard key discovery. More...

Go to the source code of this file.


Detailed Description

On investigations into the 6-round Data Encryption Standard key discovery.

Todo:
Overview
Todo:
Using the 1-base translation for the S-boxes (6-to-4)
  • Translating the DES Sboxes, as 6-to-4 bit boolean functions, using 1-bases.
  • Generating the 1-bases:
    maxima> for i : 1 thru 8 do output_dessbox_fullcnf_stdname(i)$
    shell> gen_seed[1]=7;gen_seed[2]=71;gen_seed[3]=185;gen_seed[4]=346;gen_seed[5]=67;gen_seed[6]=327;gen_seed[7]=148;gen_seed[8]=167;
    shell> base_seed[1]=1;base_seed[2]=1;base_seed[3]=2;base_seed[4]=4;base_seed[5]=2;base_seed[6]=1;base_seed[7]=2;base_seed[8]=1;
    shell> for i in $(seq 1 8); do
      QuineMcCluskey-n16-O3-DNDEBUG DES_Sbox_${i}_fullCNF.cnf > DES_Sbox_${i}_pi.cnf;
      RandomShuffleDimacs-O3-DNDEBUG ${gen_seed[$i]} < DES_Sbox_${i}_pi.cnf | SortByClauseLength-O3-DNDEBUG > DES_Sbox_${i}_sortedpi.cnf;
      RUcpGen-O3-DNDEBUG DES_Sbox_${i}_sortedpi.cnf > DES_Sbox_${i}_gen.cnf;
      RandomShuffleDimacs-O3-DNDEBUG ${base_seed[$i]}  < DES_Sbox_${i}_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > DES_Sbox_${i}_1base.cnf;
    done
       
  • The numbers of clauses in the 1-bases are 124, 129, 138, 128, 134, 136, 123, 152 respectively.
  • All the 1-bases used have clauses of sizes 5 and 6, except Sbox 4 which has clauses of size 5 and 6 as well as 2 of size 7.
  • Generating the 20 instances with random plaintext-ciphertext-pairs:
    rounds : 6$
    sbox_fcl_l : create_list(read_fcl_f(sconcat("DES_Sbox_",i,"_1base.cnf")), i, 1, 8)$
    for seed : 1 thru 20 do block(
      print(sconcat("Generating ", rounds, "-round DES with seed ", seed)),
      set_random(make_random_state(seed)),
      P_hex : lpad(int2hex(random(2**64)),"0",16),
      K_hex : lpad(int2hex(random(2**64)),"0",16),
      C_hex : des_encryption_hex_gen(rounds, P_hex,K_hex),
      P : des_plain2fcl_gen(hexstr2binv(P_hex),rounds),
      C : des_cipher2fcl_gen(hexstr2binv(C_hex),rounds),
      F : des2fcl_gen(sbox_fcl_l,rounds),
      Fs : standardise_fcl([F[1],append(F[2],P[2],C[2])]),
      output_fcl_v(
      sconcat(rounds, "-round DES instantiated with plaintext and ciphertext generated from seed ", seed, "; translated using the 1-base translation for the S-boxes (6-to-4)."),
        Fs[1],
        sconcat("des_6t4_1base_r",rounds,"_s",seed,".cnf"),
        Fs[2]))$
    print("DONE!");
       
  • Statistics for all instances:
    shell> cat des_6t4_1base_r6_s1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
        800    8432    792    800    8432    40550     NA     NA    8432    40550   801
     length   count
          1     128
          3    1920
          5    3648
          6    2730
          7       6
       
  • S-box statistics (1-base translations):
    for F in sbox_fcl_l do print(ncl_list_fcl(F));
    [[5,84],[6,39],[7,1]]
    [[5,75],[6,54]]
    [[5,76],[6,62]]
    [[5,69],[6,59]]
    [[5,78],[6,56]]
    [[5,83],[6,53]]
    [[5,75],[6,48]]
    [[5,68],[6,84]]
       
  • We have the following number of clauses of the following sizes:
    • 128 unit-clauses (setting plaintext + ciphertext);
    • 1920 ternary clauses (80 * 6 = 480 binary additions);
    • 3648 clauses of length 5 (8 * 5 = 48 S-boxes);
    • 2730 clauses of length 6 (8 * 6 = 48 S-boxes);
    • 6 clauses of length seven (1 * 6 = 6 S-boxes).
  • Running minisat-2.2.0 on these instances:
    shell> r=6;
    shell> RunMinisat des_6t4_1base_r${r}_s1.cnf;
       
    This is still running after 8 days XXX.
Todo:
Using the "minimum" translation for the S-boxes (6-to-4)
  • Translating the DES Sboxes, as 6-to-4 bit boolean functions, using the "minimum" (inf-based) representations.
  • Generating the "minimum" CNFs for the Sboxes:
    maxima> for i : 1 thru 8 do output_dessbox_fullcnf_stdname(i)$
    shell> for i in $(seq 1 8); do
      QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG DES_Sbox_${i}_fullCNF.cnf > DES_Sbox_${i}_shg.cnf;
      cat DES_Sbox_${i}_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > DES_Sbox_${i}_shg.wcnf;
    done
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 67 -solve 1 -seed 2444475534 -i DES_Sbox_1_shg.wcnf -r model DES_Sbox_1.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 67 -solve 1 -seed 2521057446 -i DES_Sbox_2_shg.wcnf -r model DES_Sbox_2.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 68 -solve 1 -seed 3544367510 -i DES_Sbox_3_shg.wcnf -r model DES_Sbox_3.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 69 -solve 1 -seed 3808694681 -i DES_Sbox_4_shg.wcnf -r model DES_Sbox_4.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 67 -solve 1 -seed 1876503362 -i DES_Sbox_5_shg.wcnf -r model DES_Sbox_5.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 66 -solve 1 -seed 68018538 -i DES_Sbox_6_shg.wcnf -r model DES_Sbox_6.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 67 -solve 1 -seed 1856244582 -i DES_Sbox_7_shg.wcnf -r model DES_Sbox_7.ass;
    shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 400000 -wtarget 69 -solve 1 -seed 4223500633 -i DES_Sbox_8_shg.wcnf -r model DES_Sbox_8.ass;
    shell> for i in $(seq 1 8); do
      cat DES_Sbox_${i}_fullCNF.cnf_primes | FilterDimacs DES_Sbox_${i}.ass > DES_Sbox_${i}_min.cnf;
    done
       
  • The numbers of clauses in the CNFs are 67, 67, 68, 69, 67, 66, 67, and 69 respectively.
  • Generating the instance for 20 random plaintext-ciphertext-pairs:
    rounds : 6$
    sbox_fcl_l : create_list(read_fcl_f(sconcat("DES_Sbox_",i,"_min.cnf")), i, 1, 8)$
    for seed : 1 thru 20 do block(
      print(sconcat("Generating ", rounds, "-round DES with seed ", seed)),
      set_random(make_random_state(seed)),
      P_hex : lpad(int2hex(random(2**64)),"0",16),
      K_hex : lpad(int2hex(random(2**64)),"0",16),
      C_hex : des_encryption_hex_gen(rounds, P_hex,K_hex),
      P : des_plain2fcl_gen(hexstr2binv(P_hex),rounds),
      C : des_cipher2fcl_gen(hexstr2binv(C_hex),rounds),
      F : des2fcl_gen(sbox_fcl_l,rounds),
      Fs : standardise_fcl([F[1],append(F[2],P[2],C[2])]),
      output_fcl_v(
      sconcat(rounds, "-round DES instantiated with plaintext and ciphertext generated from seed ", seed, "; translated using the 1-base translation for the S-boxes (6-to-4)."),
        Fs[1],
        sconcat("des_6t4_min_r",rounds,"_s",seed,".cnf"),
        Fs[2]))$
    print("DONE!");
       
  • Statistics:
    shell> cat des_6t4_min_r6_s1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
        800    5288    792    800    5288    24008     NA     NA    5288    24008   801
     length   count
          1     128
          3    1920
          5    1392
          6    1776
          7      72
       
  • S-box statistics ("minimum" translation):
    for F in sbox_fcl_l do print(ncl_list_fcl(F));
    
    [[5,30],[6,35],[7,2]]
    [[5,33],[6,33],[7,1]]
    [[5,28],[6,38],[7,2]]
    [[5,29],[6,38],[7,2]]
    [[5,29],[6,36],[7,2]]
    [[5,28],[6,38]]
    [[5,29],[6,37],[7,1]]
    [[5,26],[6,41],[7,2]]
      
  • We have the following number of clauses of the following sizes:
    • 128 unit-clauses (setting plaintext + ciphertext);
    • 1920 ternary clauses (80 * 6 = 480 binary additions);
    • 1392 clauses of length 5 (8 * 6 = 48 S-boxes);
    • 1776 clauses of length 6 (8 * 5 = 48 S-boxes);
    • 72 clauses of length seven (7 * 6 = 42 S-boxes).
  • Running minisat-2.2.0 on these instances:
    shell> r=6;
    shell> RunMinisat des_6t4_min_r${r}_s1.cnf;
       
    This is still running after 8 days XXX.
Todo:
Using the canonical translation for the S-boxes (6-to-4)
  • Translating the DES Sboxes, as 6x4 boolean functions, using the canonical representation. That is, each Sbox is represented with the canonical representation given by dualts_fcl in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac.
  • Generating the instance:
    rounds : 6$
    sbox_fcl_l : create_list(dualts_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
    for seed : 1 thru 20 do block(
      print(sconcat("Generating ", rounds, "-round DES with seed ", seed)),
      set_random(make_random_state(seed)),
      P_hex : lpad(int2hex(random(2**64)),"0",16),
      K_hex : lpad(int2hex(random(2**64)),"0",16),
      C_hex : des_encryption_hex_gen(rounds, P_hex,K_hex),
      P : des_plain2fcl_gen(hexstr2binv(P_hex),rounds),
      C : des_cipher2fcl_gen(hexstr2binv(C_hex),rounds),
      F : des2fcl_gen(sbox_fcl_l,rounds),
      Fs : standardise_fcl([F[1],append(F[2],P[2],C[2])]),
      output_fcl_v(
      sconcat(rounds, "-round DES instantiated with plaintext and ciphertext generated from seed ", seed, "; translated using the 1-base translation for the S-boxes (6-to-4)."),
        Fs[1],
        sconcat("des_6t4_canon_r",rounds,"_s",seed,".cnf"),
        Fs[2]))$
    print("DONE!");
       
  • Statistics:
    shell> cat des_6t4_canon_r6_s1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG nz
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
       3872   35888   3864   3872   35888   104192     NA     NA   35888   104192  3873
     length   count
          1     128
          2   30720
          3    1920
         11    3072
         64      48
       
  • S-box statistics (canonical translation):
    ncl_list_fcl(dualts_fcl([listify(setn(10)), des_sbox_fulldnf_cl(1)]));
    [[2,640],[11,64],[64,1]]
       
  • We have the following number of clauses of the following sizes:
    • 128 unit-clauses (setting plaintext + ciphertext);
    • 30720 binary clauses (8 * 6 = 48 S-boxes);
    • 1920 ternary clauses (80 * 6 = 480 binary additions);
    • 3072 clauses of length eleven (8 * 6 = 48 S-boxes);
    • 48 clauses of length 64 (8 * 6 = 48 S-boxes).
  • Running minisat-2.2.0 on these instances:
    shell> r=6;
    shell> RunMinisat des_6t4_canon_r${r}_s1.cnf;
       
    This is still running after 8 days XXX.

Definition in file 6.hpp.