OKlibrary  0.2.1.6
Sbox_4.hpp File Reference

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

Go to the source code of this file.


Detailed Description

On investigations into Sbox four of the Data Encryption Standard.

Todo:
Basic data
  • Generating the full CNF representation:
    1. The CNF-file "DES_Sbox_4_fullCNF.cnf" is created by the Maxima-function output_dessbox_fullcnf_stdname(4) 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_4_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(4),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_4_fullCNF.cnf > DES_Sbox_4_shg.cnf
    shell> cat DES_Sbox_4_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > DES_Sbox_4_shg.wcnf
       
  • Running then:
    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_s69.ass;
    shell> cat DES_Sbox_4_fullCNF.cnf_primes | FilterDimacs DES_Sbox_4_s69.ass > DES_Sbox_4_s69.cnf
    shell> cat DES_Sbox_4_s69.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 68 382 0 382 1 1
     length count
    5 28
    6 38
    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_4_s69.cnf")$
      maxima> Sbox_primes_F : read_fcl_f("DES_Sbox_4_fullCNF.cnf_primes")$
      maxima> hardness_wpi_cs(setify(Sbox_min_F[2]), setify(Sbox_primes_F[2]));
      3
           
Todo:
1-base : mincl_r1 <= 128
  • 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_4_fullCNF.cnf > DES_Sbox_4_pi.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 346 < DES_Sbox_4_pi.cnf | SortByClauseLength-O3-DNDEBUG > DES_Sbox_4_sortedpi.cnf
    shell> RUcpGen-O3-DNDEBUG DES_Sbox_4_sortedpi.cnf > DES_Sbox_4_gen.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 4 < DES_Sbox_4_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > DES_Sbox_4_1base.cnf
    shell> cat DES_Sbox_4_1base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 69 387 0 387 1 1
     length count
    5 29
    6 38
    7 2
       
Todo:
Move Sbox-1-specific investigations here

Definition in file Sbox_4.hpp.