OKlibrary  0.2.1.6
1.hpp File Reference

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

Go to the source code of this file.


Detailed Description

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

Todo:
Overview
Todo:
Using the canonical translation for the S-box (6-to-4)
  • Translating the one round DES key discovery problem using the canonical translation for the DES Sboxes, as 6-to-4 bit boolean functions.
  • Generating the instance:
    rounds : 1$
    sbox_fcl_l : create_list(dualts_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
    P_hex : "038E596D4841D03B"$
    K_hex : "15FBC08D31B0D521"$
    C_hex : des_encryption_hex_gen(rounds, "038E596D4841D03B","15FBC08D31B0D521")$
    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("DES over ",rounds," rounds; translated using the canonical translation for the S-boxes (6-to-4)."),
      Fs[1],
      sconcat("des_canon_r",rounds,".cnf"),
      Fs[2])$
    print("DONE!");
       
  • Statistics:
    shell> cat des_canon_r1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    752 6088 17472 0 17472 753 1
     length count
    1 128
    2 5120
    3 320
    11 512
    64 8
       
  • 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);
    • 5120 binary clauses (8 S-boxes);
    • 320 ternary clauses (80 binary additions);
    • 512 clauses of length eleven (8 S-boxes);
    • 8 clauses of length 64 (8 S-boxes).
  • Most solvers solve without any conflicts/backtracks (cryptominisat, precosat236, precosat-570.1, minisat-2.2.0, minisat2, glucose, satz215, sat-grasp).
  • Some solvers do take some conflicts/nodes (picosat:9).
  • march_pl yields:
    shell> march_pl des_canon_r1.cnf
    c main():: nodeCount: 25
    c main():: dead ends in main: 0
       
    Does "dead ends" mean number of backtracks?
  • OKsolver_2002 also solves without any decisions:
    shell> OKsolver_2002-O3-DNDEBUG des_canon_r1.cnf
    c number_of_initial_unit-eliminations   608
    c running_time(sec)                     0.0
    c number_of_nodes                       1
    c number_of_2-reductions                7
    c number_of_autarkies                   8
       
  • Are we just lucky that some solvers happen to pick the right variables?
Todo:
Using the 1-base translation for the S-boxes (6-to-4)
  • Translating the one round DES key discovery problem using the 1-bases to translate the DES Sboxes, as 6-to-4 bit boolean functions.
  • 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 instance:
    rounds : 1$
    sbox_fcl_l : create_list(read_fcl_f(sconcat("DES_Sbox_",i,"_1base.cnf")), i, 1, 8)$
    P_hex : "038E596D4841D03B"$
    K_hex : "15FBC08D31B0D521"$
    C_hex : des_encryption_hex_gen(rounds, "038E596D4841D03B","15FBC08D31B0D521")$
    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("DES over ",rounds," rounds; translated using the 1-base translation for the S-boxes (6-to-4)."),
      Fs[1],
      sconcat("des_1base_r",rounds,".cnf"),
      Fs[2])$
    print("DONE!");
       
  • Statistics:
    shell> cat des_1base_r1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    240 1512 6865 0 6865 241 1
     length count
    1 128
    3 320
    5 608
    6 455
    7 1
       
  • S-box statistics (1-base translation):
    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);
    • 320 ternary clauses (80 binary additions);
    • 608 clauses of length five (8 S-boxes);
    • 455 clauses of length six (8 S-boxes);
    • 1 clauses of length seven (1 S-box).
  • Most solvers solve without any conflicts/backtracks (cryptominisat, precosat236, precosat-570.1, minisat-2.2.0, minisat2, satz215, sat-grasp).
  • Some solvers do take some conflicts/nodes (picosat:3, glucose:2).
  • march_pl yields:
    shell> march_pl des_1base_r1.cnf
    c main():: nodeCount: 17
    c main():: dead ends in main: 0
       
    Does "dead ends" mean number of backtracks?
  • OKsolver_2002 now needs some decisions to solve:
    shell> OKsolver_2002-O3-DNDEBUG des_1base_r1.cnf
    c running_time(sec)                     0.0
    c number_of_nodes                       7
    c number_of_quasi_single_nodes          1
    c number_of_2-reductions                3
    c number_of_autarkies                   8
    c number_of_1-autarkies                 24
       
  • Are we just lucky that some solvers happen to pick the right variables?
Todo:
Using the canonical+ translation for the S-boxes (6-to-4)
  • Translating the one round DES key discovery problem using the canonical+ translation for the DES Sboxes, as 6-to-4 bit boolean functions.
  • Generating the instance:
    rounds : 1$
    sbox_fcl_l : create_list(dualtsplus_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
    P_hex : "038E596D4841D03B"$
    K_hex : "15FBC08D31B0D521"$
    C_hex : des_encryption_hex_gen(rounds, "038E596D4841D03B","15FBC08D31B0D521")$
    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("DES over ",rounds," rounds; translated using the canonical+ translation for the S-boxes (6-to-4)."),
      Fs[1],
      sconcat("des_canonp_r",rounds,".cnf"),
      Fs[2])$
    print("DONE!");
       
  • Statistics:
    shell> cat des_canonp_r1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    752 6248 22752 0 22752 753 1
     length count
    1 128
    2 5120
    3 320
    11 512
    33 160
    64 8
       
  • S-box statistics (canonical+ translation):
    ncl_list_fcl(dualtsplus_fcl([listify(setn(10)), des_sbox_fulldnf_cl(1)]));
    [[2,640],[11,64],[33,20],[64,1]]
       
  • We have the following number of clauses of the following sizes:
    • 128 unit-clauses (setting plaintext + ciphertext);
    • 5120 binary clauses (8 S-boxes);
    • 320 ternary clauses (80 binary additions);
    • 512 clauses of length eleven (8 S-boxes);
    • 160 clauses of length 33 (8 S-boxes);
    • 8 clauses of length 64 (8 S-boxes).
  • Most solvers solve without any conflicts/backtracks (cryptominisat, precosat236, precosat-570.1, minisat-2.2.0, minisat2, glucose, satz215, sat-grasp, glucose, picosat).
  • march_pl yields:
    shell> march_pl des_canonp_r1.cnf
    c main():: nodeCount: 17
    c main():: dead ends in main: 0
       
    Does "dead ends" mean number of backtracks?
  • OKsolver_2002 also solves without any decisions:
    shell> OKsolver_2002-O3-DNDEBUG des_canonp_r1.cnf
    c number_of_initial_unit-eliminations   622
    c running_time(sec)                     0.0
    c number_of_nodes                       1
    c number_of_autarkies                   8
       
    In this case, everything follows completely by UCP.
Todo:
Using the canonical CNF translation for the S-boxes (6-to-4)
  • Translating the DES Sboxes, as 6-to-4 bit boolean functions, using the canonical CNFs. That is, each Sbox is represented with a CNF where all clauses are of length 10.
  • Generating the instance:
    rounds : 1$
    sbox_fcl_l : create_list(fcs2fcl(des_sbox_fullcnf_fcs(i)), i, 1, 8)$
    P_hex : "038E596D4841D03B"$
    K_hex : "15FBC08D31B0D521"$
    C_hex : des_encryption_hex_gen(rounds, "038E596D4841D03B","15FBC08D31B0D521")$
    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("DES over ",rounds," rounds; translated using the canonical CNF for S-boxes (6-to-4)."),
      Fs[1],
      sconcat("des_full_r",rounds,".cnf"),
      Fs[2])$
    print("DONE!");
       
  • Statistics:
    shell> cat des_full_r1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    240 8128 77888 0 77888 241 1
     length count
    1 128
    3 320
    10 7680
       
  • S-box statistics (canonical CNF translation):
    ncl_list_fcl(des_sbox_fullcnf_fcs(1));
    [[10,960]]
      
  • We have the following number of clauses of the following sizes:
    • 128 unit-clauses (setting plaintext + ciphertext);
    • 320 ternary clauses (80 binary additions);
    • 7680 clauses of length ten (8 S-boxes);
  • Solvers (t:time,cfs:conflicts,nds:nodes): precosat-570.1 (t:0s,cfs:0) precosat236 (t:0s,cfs:0), minisat-2.2.0 (t:0.18s,cfs:2), cryptominisat (t:0.01s,cfs:9), glucose (t:0.01s,cfs:31), OKsolver_2002 (t:0.0,nds:34).
Todo:
Using the "minimum" translation for the S-boxes (6-to-4)
  • Translating the one round DES key discovery problem using the "minimum" translations for the DES Sboxes, as 6-to-4 bit boolean functions.
  • 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:
    rounds : 1$
    sbox_fcl_l : create_list(read_fcl_f(sconcat("DES_Sbox_",i,"_min.cnf")), i, 1, 8)$
    P_hex : "038E596D4841D03B"$
    K_hex : "15FBC08D31B0D521"$
    C_hex : des_encryption_hex_gen(rounds, "038E596D4841D03B","15FBC08D31B0D521")$
    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("DES over ",rounds," rounds; translated using the minimum translation for the S-boxes (6-to-4)."),
      Fs[1],
      sconcat("des_min_r",rounds,".cnf"),
      Fs[2])$
    print("DONE!");
       
  • Statistics:
    shell> cat des_min_r1.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    240 988 4108 0 4108 241 1
     length count
    1 128
    3 320
    5 232
    6 296
    7 12
       
  • 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);
    • 320 ternary clauses (80 binary additions);
    • 232 clauses of length five (8 S-boxes);
    • 296 clauses of length six (8 S-boxes);
    • 12 clauses of length seven (7 S-boxes).
  • Some solvers solve without any conflicts/backtracks (precosat236, precosat-570.1, minisat-2.2.0, minisat2, sat-grasp).
  • Some solvers do take some conflicts/nodes (cryptominisat:1, picosat:3, glucose:2, satz215:1).
  • march_pl yields:
    shell> march_pl des_min_r1.cnf
    c main():: nodeCount: 17
    c main():: dead ends in main: 0
       
    Does "dead ends" mean number of backtracks?
  • OKsolver_2002 now needs some decisions to solve:
    shell> OKsolver_2002-O3-DNDEBUG des_min_r1.cnf
    c running_time(sec)                     0.0
    c number_of_nodes                       9
    c number_of_quasi_single_nodes          1
    c number_of_2-reductions                5
    c number_of_autarkies                   8
    c max_tree_depth                        7
    c number_of_1-autarkies                 22
       
  • Are we just lucky that some solvers happen to pick the right variables?

Definition in file 1.hpp.