OKlibrary  0.2.1.6
Sbox_6.hpp File Reference

On investigations into Sbox six of the Data Encryption Standard. More...

Go to the source code of this file.


Detailed Description

On investigations into Sbox six of the Data Encryption Standard.

Todo:
Basic data
  • Generating the full CNF representation:
    1. The CNF-file "DES_Sbox_6_fullCNF.cnf" is created by the Maxima-function output_dessbox_fullcnf_stdname(6) in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/DataEncryptionStandard/Sboxes.mac, which is a full clause-set with 10 variables and 2^10 - 2^6 = 960 clauses:
      > cat DES_Sbox_6_fullCNF.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
       n non_taut_c red_l taut_c orig_l comment_count finished_bool
      10 960 9600 0 9600 1 1
       length count
      10 960
           
    2. This clause-set is also computed by bf2relation_fullcnf_fcs(des_sbox_bf(6),6).
  • The minimum CNF representation has at most 66 clauses. See "Using weighted MaxSAT to compute small CNFs".
Todo:
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 66)
  • Computing the weighted MaxSAT problem:
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG DES_Sbox_6_fullCNF.cnf > DES_Sbox_6_shg.cnf
    shell> cat DES_Sbox_6_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > DES_Sbox_6_shg.wcnf
       
  • Running then:
    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_s66.ass;
    shell> cat DES_Sbox_6_fullCNF.cnf_primes | FilterDimacs DES_Sbox_6_s66.ass > DES_Sbox_6_s66.cnf
    shell> cat DES_Sbox_6_s66.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 66 368 0 368 1 1
     length count
    5 28
    6 38
       
  • The hardness of this "minimum" representation is 3:
    • See "Hardness of boolean function representations" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp for a description of the notion of hardness, and method of computation.
    • Computing the hardness:
      maxima> Sbox_min_F : read_fcl_f("DES_Sbox_6_s66.cnf")$
      maxima> Sbox_primes_F : read_fcl_f("DES_Sbox_6_fullCNF.cnf_primes")$
      maxima> hardness_wpi_cs(setify(Sbox_min_F[2]), setify(Sbox_primes_F[2]));
      3
           
Todo:
1-base : mincl_r1 <= 136
  • The 1-bases below need to be checked to ensure they are actually 1-bases; see "Computing r_1-bases for a set of prime implicates" in Satisfiability/Reductions/Bases/plans/UcpBase.hpp.
  • Computing an 1-base
    shell> QuineMcCluskey-n16-O3-DNDEBUG DES_Sbox_6_fullCNF.cnf > DES_Sbox_6_pi.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 327 < DES_Sbox_6_pi.cnf | SortByClauseLength-O3-DNDEBUG > DES_Sbox_6_sortedpi.cnf
    shell> RUcpGen-O3-DNDEBUG DES_Sbox_6_sortedpi.cnf > DES_Sbox_6_gen.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 1 < DES_Sbox_6_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > DES_Sbox_6_1base.cnf
    shell> cat DES_Sbox_6_1base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 136 733 0 733 0 1
     length count
    5 83
    6 53
       
Todo:
Move Sbox-1-specific investigations here

Definition in file Sbox_6.hpp.