OKlibrary  0.2.1.6
Sbox_8.hpp File Reference

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

Go to the source code of this file.


Detailed Description

On investigations into Sbox eight of the Data Encryption Standard.

Todo:
Basic data
  • Generating the full CNF representation:
    1. The CNF-file "DES_Sbox_8_fullCNF.cnf" is created by the Maxima-function output_dessbox_fullcnf_stdname(8) 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_8_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(8),6).
  • The minimum CNF representation has at most 69 clauses. See "Using weighted MaxSAT to compute small CNFs".
Todo:
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 69)
  • Computing the weighted MaxSAT problem:
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG DES_Sbox_8_fullCNF.cnf > DES_Sbox_8_shg.cnf
    shell> cat DES_Sbox_8_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > DES_Sbox_8_shg.wcnf
       
  • Running then:
    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_s69.ass;
    shell> cat DES_Sbox_8_fullCNF.cnf_primes | FilterDimacs DES_Sbox_8_s69.ass > DES_Sbox_8_s69.cnf
    shell> cat DES_Sbox_8_s69.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 69 390 0 390 1 1
     length count
    5 26
    6 41
    7 2
       
  • 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_8_s69.cnf")$
      maxima> Sbox_primes_F : read_fcl_f("DES_Sbox_8_fullCNF.cnf_primes")$
      maxima> hardness_wpi_cs(setify(Sbox_min_F[2]), setify(Sbox_primes_F[2]));
      3
           
Todo:
1-base : mincl_r1 <= 152
  • 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_8_fullCNF.cnf > DES_Sbox_8_pi.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 167 < DES_Sbox_8_pi.cnf | SortByClauseLength-O3-DNDEBUG > DES_Sbox_8_sortedpi.cnf
    shell> RUcpGen-O3-DNDEBUG DES_Sbox_8_sortedpi.cnf > DES_Sbox_8_gen.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 1 < DES_Sbox_8_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > DES_Sbox_8_1base.cnf
    shell> cat DES_Sbox_8_1base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 152 844 0 844 0 1
     length count
    5 68
    6 84
       
Todo:
Move Sbox-1-specific investigations here

Definition in file Sbox_8.hpp.