OKlibrary  0.2.1.6
Sbox_3.hpp File Reference

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

Go to the source code of this file.


Detailed Description

On investigations into Sbox three of the Data Encryption Standard.

Todo:
Basic data
  • Generating the full CNF representation:
    1. The CNF-file "DES_Sbox_3_fullCNF.cnf" is created by the Maxima-function output_dessbox_fullcnf_stdname(3) 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_3_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(3),6).
  • The minimum CNF representation has at most 68 clauses. See "Using weighted MaxSAT to compute small CNFs".
Todo:
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 68)
  • Computing the weighted MaxSAT problem:
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG DES_Sbox_3_fullCNF.cnf > DES_Sbox_3_shg.cnf
    shell> cat DES_Sbox_3_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > DES_Sbox_3_shg.wcnf
       
  • Running then:
    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_s68.ass;
    shell> cat DES_Sbox_3_fullCNF.cnf_primes | FilterDimacs DES_Sbox_3_s68.ass > DES_Sbox_3_s68.cnf
    shell> cat DES_Sbox_3_s68.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_3_s68.cnf")$
      maxima> Sbox_primes_F : read_fcl_f("DES_Sbox_3_fullCNF.cnf_primes")$
      maxima> hardness_wpi_cs(setify(Sbox_min_F[2]), setify(Sbox_primes_F[2]));
      3
           
Todo:
1-base : mincl_r1 <= 138
  • 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_3_fullCNF.cnf > DES_Sbox_3_pi.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 185 < DES_Sbox_3_pi.cnf | SortByClauseLength-O3-DNDEBUG > DES_Sbox_3_sortedpi.cnf
    shell> RUcpGen-O3-DNDEBUG DES_Sbox_3_sortedpi.cnf > DES_Sbox_3_gen.cnf
    shell> RandomShuffleDimacs-O3-DNDEBUG 2 < DES_Sbox_3_gen.cnf | SortByClauseLengthDescending-O3-DNDEBUG | RUcpBase-O3-DNDEBUG > DES_Sbox_3_1base.cnf
    shell> cat DES_Sbox_3_1base.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    10 138 752 0 752 0 1
     length count
    5 76
    6 62
       
Todo:
Move Sbox-1-specific investigations here

Definition in file Sbox_3.hpp.