OKlibrary  0.2.1.6
general.hpp File Reference

On investigations into the Data Encryption Standard. More...

Go to the source code of this file.


Detailed Description

On investigations into the Data Encryption Standard.

Todo:
Understanding DES
  • First implementations of encryption/decryption at the Maxima-level are needed.
  • At least in two versions, as follows:
    1. Following the specific descriptions of the various permutations and S-boxes.
    2. Emphasising the abstract flow information (abstracting away of the specific nature of the special functions involved).
  • We also need to think about different organisations of the round. Perhaps the key-involvement could happen at the beginning or end of a round, instead of in the middle.
  • See Investigations/Cryptography/DataEncryptionStandard/plans/Sboxes/general.hpp for investigations into the DES Sboxes.
Todo:
Generating satisfying DES assignments
  • Using the functions:
    • output_des_random_pcpair_pa_std,
    • output_des_random_pkpair_pa_std,
    • output_des_random_kcpair_pa_std,
    • output_des_random_pkctriple_pa_std
    in DataEncryptionStandard/GeneralisedConstraintTranslation.mac we can generate unit-clauses representing random satisfying partial assignments for various combinations of the DES plaintext, key and ciphertext variables.
  • To generate a total satisfying assignment, we can simply use a partial assignment generated by these functions and then apply unit-clause propagation:
    # Generate canonical DES instance over 5-rounds
    maxima> sbox_fcl_l : create_list(dualts_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
    maxima> output_des2fcl_gen_std("canon", sbox_fcl_l, 5);
    # Generate satisfying total assignment for 5-round DES and seed 1
    > Total_SAT_Add4DES_Instance des_6t4_canon_r5.cnf 1 1 > des_6t4_canon_r5_s1.ta
       
    See Total_SAT_Add4DES_Instance.
  • We should implement scripts to do this, and application tests.
  • Such generated assignments can be used to determine which sub-instance generated by SplittingViaOKsolver contains the known satisfying assignments (while it is not known whether there are other satisfying assignments).
  • We should also implement scripts to find such a satisfiable instance in this case.
  • SplittingViaOKsolver with respect to the DES is discussed in "Applying SplittingViaOKsolver" in Investigations/Cryptography/DataEncryptionStandard/plans/KeyDiscovery/5.hpp.
Todo:
DES benchmarks
Todo:
Basic translation
  • Just following the definitions, of course "ignoring" the permutations, that is, they just are interpreted as "rewirings".
  • Since the key schedule thus now is basically trivial (only input key bits are used), all what remains are the S-boxes and binary additions.
  • The S-boxes have 6 input and 4 output bits, and thus yield 10-bit boolean functions.
  • These can be analysed completely, and we can study the various representations (at least minimum, canonical, r_0- and r_1-bases).
  • We should obtain a considerably smaller formula than what Massacci and Marraro obtained. To be comparable, for the minimum translation we also need two versions: one treating an S-box as one 6-to-4 bit function, and one treating it as 4 6-bit functions.
  • The canonical translation for the 6-to-4 bit Sbox contains 64 new variables and 705 clauses:
    maxima> ncl_list_full_dualts(10,64);
    [[2,640],[11,64],[64,1]]
    nvar_full_dualts(10,64) - 10;
    64
       
  • Using the canonical box translation and treating the Sboxes as 6-to-4 bit functions, the full 16 round DES will contain:
    • 64+56+9984=10104 variables:
      1. 64 variables for the input plaintext.
      2. 56 variables for the key.
      3. 16*(48+512+32+32)=9984 variables from 16 rounds consisting of:
        1. 48 variables for the output of the key addition.
        2. 8*64=512 variables for the S-box representation.
        3. 32 variables for the output of Sbox substitutions.
        4. 32 variables for the output of the final addition.
    • 81920+5120+8192+128=95360 clauses:
      1. 16*8*640=81920 clauses of size 2 (16 rounds * 8 Sboxes * 640 clauses = 81,920).
      2. 16*(48+32)*4=5120 clauses of size 4 (16 rounds * (48-bit addition + 32-bit addition) * 4 clauses = 5120).
      3. 16*8*64=8192 clauses of size 11 (16 rounds * 8 Sboxes * 64 clauses = 8,192).
      4. 16*8=128 clauses of size 64 (16 rounds * 8 Sboxes * 1 clause = 128).
  • In comparison to Massaci and Marraro, they have 61,935 clauses and 10,336 variables.
  • Using a minimum-representation for the S-boxes, we get:
    1. 64+56+16*(48+32+32)=1912 variables.
    2. If a minimum representation of an S-box (a 10-bit boolean function) needs P clauses (assuming that the eight different S-boxes share the same size), then 16*((48+32)*4+8*P)= 5120 + 128*P clauses are used.
    3. We should have P <= 100, and so less than 20000 clauses are needed (for this smallest representation).
    4. Alternatively every S-box is represented by 4 1-bit-output functions.
    5. If such a (6-bit) function uses Q clauses, then 16*((48+32)*4+8*4*Q)= 5120 + 512*Q clauses are used.
    6. Likely Q <= 30, and thus around 20000 clauses are needed.
  • DONE (No, both follow by UCP; see "Encryption and decryption") Do we need also to include decryption? Can the basic scheme encrypt and decrypt by just unit-clause propagation?
Todo:
Encryption and decryption
  • We consider encryption and decryption instances of the 16 round DES.
  • These instances are the full 16 round DES translation.
  • Unit-clauses are added for the plaintext and key, or ciphertext and key. This is for encryption and decryption respectively.
  • See "Basic translation" for statistics for these instances.
  • The task of the solver is then to derive the ciphertext or plaintext variables for encryption and decryption respectively.
  • Using the canonical translation for the Sboxes:
    • Encryption and decryption of DES follows by unit-clause propagation.
    • Encryption:
      • Generating an encryption instance for 16 rounds using ArgoSAT test vectors (see Cryptography/DataEncryptionStandard/plans/KeyDiscovery/general.hpp):
        sbox_fcl_l : create_list(dualtsplus_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
        F : des2fcl(sbox_fcl_l)$
        P : des_plain2fcl(hexstr2binv("038E596D4841D03B"))$
        K : des_key2fcl(hexstr2binv("15FBC08D31B0D521"))$
        F_std : standardise_fcs([F[1],append(F[2],P[2],K[2])])$
        output_fcs_v(sconcat("DES ArgoSat comparison over 16 rounds with the first ", unknown_bits, " key bits undefined."), F_std[1] , sconcat("des_argocomp_encrypt.cnf"), F_std[2]);
             
      • precosat236 and OKsolver_2002 need 0 decisions to solve this instance:
        shell> precosat236 des_argocomp_encrypt.cnf
        *snip*
        c 0 conflicts, 0 decisions, 0 random
        *snip*
        shell> OKsolver_2002-O3-DNDEBUG des_argocomp_encrypt.cnf
        *snip*
        c number_of_nodes                       0
        *snip*
             
    • Decryption:
      • Generating a decryption instance for 16 rounds and ArgoSAT test vectors (see Cryptography/DataEncryptionStandard/plans/KeyDiscovery/general.hpp):
        sbox_fcl_l : create_list(dualtsplus_fcl([listify(setn(10)), des_sbox_fulldnf_cl(i)]), i, 1, 8)$
        F : des2fcl(sbox_fcl_l)$
        C : des_cipher2fcl(hexstr2binv("A2FB6032638EC79D"))$
        K : des_key2fcl(hexstr2binv("15FBC08D31B0D521"))$
        F_std : standardise_fcs([F[1],append(F[2],C[2],K[2])])$
        output_fcs_v(sconcat("DES ArgoSat comparison over 16 rounds with the first ", unknown_bits, " key bits undefined."), F_std[1] , sconcat("des_argocomp_decrypt.cnf"), F_std[2]);
             
      • precosat236 and OKsolver_2002 need 0 decisions to solve this instance:
        shell> precosat236 des_argocomp_decrypt.cnf
        *snip*
        c 0 conflicts, 0 decisions, 0 random
        *snip*
        shell> OKsolver_2002-O3-DNDEBUG des_argocomp_decrypt.cnf
        *snip*
        c number_of_nodes                       0
        *snip*
             
Todo:
r_2-bases of a round
  • It seems not effective, and also not needed for obtaining an r_1-base, to integrate the addition of 4 (selected) bits to the S-box output, yielding a 14-bit boolean function: this should create a lot of clauses, which are also obtained, as r_1-bases, by just translating the additions.
  • However on the input-side of an S-box more interesting things happen: 4 (selected) bits yield 6 bits by partial repetition, they are added with 6 key bits, and yield the input of the S-box. This yields also a 14-bit boolean function, whose use should improve the above basic translation.
  • Again we consider at least minimum, canonical and r_0-, r_1-based representations.
  • We should obtain r_2-based representations of a round.
  • Do we have an r_1-base of the operation which applies all Sboxes to the 48-bit input?
    • This is complicated by the fact that the Sboxes share input bits due to repetition.
Todo:
Understanding the Massacci-Marraro translation
  • The reference is [SAT 2000, editors Gent, van Maaren, Walsh, pages 343-375].
  • Their benchmarks should become part of the OKlibrary (ExternalSources).
  • The article speaks about the "commercial version" ? Likely this means just full DES?
  • It seems superfluous variables are used, since the "superstructure", the permutations and the whole structure, is not trivialised, but is represented by "logical" formulas.
  • On pages 356-361 one finds accordingly strange considerations regarding various circuits.
  • The S-boxes:
    1. On page 351, last paragraph it says that just by unit-clause propagation encryption can be performed.
    2. However on pages 356-357 Espresso and minimisation is mentioned, in two versions, considering an S-box as a 6-to-4 bit functions and as 4 6-bit functions.
    3. Apparently they go for a minimum representation?
    4. If they use the 6-to-4 bit representation, then the output bit can't be inferred.
    5. But using the 4 6-bit functions, the output bit is trivially inferred since it's the only variable left.
    6. So that seems to be it.
    7. However in Section 4.3 they speak of "PLAs" ("Programmable Logic Arrays") and of minterms (constituting the canonical DNF, consisting of all full DNF-clauses).
    8. We have some information on PLAs in Buildsystem/ExternalSources/SpecialBuilds/docus/Espresso.hpp. We need to have full information there.
    9. Then Espresso is used to minimise some PLAs. They speak actually again of "minterms", where they could "obtain a further improvement in terms of the number of minterms associated with each output"? When using (only) minterms, there is no choice!
    10. Since in Figure 3 in the article a disjunction of minterms is used, perhaps they use roughly the canonical translation for the full DNF?
  • Overall one sees with that article the fundamental problem of "logic cryptoanalysis": Careless use of all sorts of extended boolean formulas, which are then *somehow* transformed into some "clausal form", which is not considered on its own, but is just treated as some sort of "file format". On the contrary, in the OKlibrary full attention is given to clauses (as one would with graphs).
Todo:
More advanced treatments
  • It seems complicated to "break" the barriers between the rounds, but we should try.
  • The point is that even if we have a very good representation of a round, the sixteen rounds together likely still have enough confusion power to make the problem very hard for a SAT solver.
  • Definitely xor-constraint can be merged.

Definition in file general.hpp.