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 Maximalevel are needed.

At least in two versions, as follows:

Following the specific descriptions of the various permutations and Sboxes.

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 keyinvolvement 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 unitclauses 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 unitclause propagation:
# Generate canonical DES instance over 5rounds
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 5round 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 subinstance 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 Sboxes and binary additions.

The Sboxes have 6 input and 4 output bits, and thus yield 10bit boolean functions.

These can be analysed completely, and we can study the various representations (at least minimum, canonical, r_0 and r_1bases).

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 Sbox as one 6to4 bit function, and one treating it as 4 6bit functions.

The canonical translation for the 6to4 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 6to4 bit functions, the full 16 round DES will contain:

64+56+9984=10104 variables:

64 variables for the input plaintext.

56 variables for the key.

16*(48+512+32+32)=9984 variables from 16 rounds consisting of:

48 variables for the output of the key addition.

8*64=512 variables for the Sbox representation.

32 variables for the output of Sbox substitutions.

32 variables for the output of the final addition.

81920+5120+8192+128=95360 clauses:

16*8*640=81920 clauses of size 2 (16 rounds * 8 Sboxes * 640 clauses = 81,920).

16*(48+32)*4=5120 clauses of size 4 (16 rounds * (48bit addition + 32bit addition) * 4 clauses = 5120).

16*8*64=8192 clauses of size 11 (16 rounds * 8 Sboxes * 64 clauses = 8,192).

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 minimumrepresentation for the Sboxes, we get:

64+56+16*(48+32+32)=1912 variables.

If a minimum representation of an Sbox (a 10bit boolean function) needs P clauses (assuming that the eight different Sboxes share the same size), then 16*((48+32)*4+8*P)= 5120 + 128*P clauses are used.

We should have P <= 100, and so less than 20000 clauses are needed (for this smallest representation).

Alternatively every Sbox is represented by 4 1bitoutput functions.

If such a (6bit) function uses Q clauses, then 16*((48+32)*4+8*4*Q)= 5120 + 512*Q clauses are used.

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 unitclause 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.

Unitclauses 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 unitclause 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_2002O3DNDEBUG 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_2002O3DNDEBUG des_argocomp_decrypt.cnf
*snip*
c number_of_nodes 0
*snip*
 Todo:
 r_2bases of a round

It seems not effective, and also not needed for obtaining an r_1base, to integrate the addition of 4 (selected) bits to the Sbox output, yielding a 14bit boolean function: this should create a lot of clauses, which are also obtained, as r_1bases, by just translating the additions.

However on the inputside of an Sbox 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 Sbox. This yields also a 14bit boolean function, whose use should improve the above basic translation.

Again we consider at least minimum, canonical and r_0, r_1based representations.

We should obtain r_2based representations of a round.

Do we have an r_1base of the operation which applies all Sboxes to the 48bit input?

This is complicated by the fact that the Sboxes share input bits due to repetition.
 Todo:
 Understanding the MassacciMarraro translation

The reference is [SAT 2000, editors Gent, van Maaren, Walsh, pages 343375].

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 356361 one finds accordingly strange considerations regarding various circuits.

The Sboxes:

On page 351, last paragraph it says that just by unitclause propagation encryption can be performed.

However on pages 356357 Espresso and minimisation is mentioned, in two versions, considering an Sbox as a 6to4 bit functions and as 4 6bit functions.

Apparently they go for a minimum representation?

If they use the 6to4 bit representation, then the output bit can't be inferred.

But using the 4 6bit functions, the output bit is trivially inferred since it's the only variable left.

So that seems to be it.

However in Section 4.3 they speak of "PLAs" ("Programmable Logic
Arrays") and of minterms (constituting the canonical DNF, consisting of all full DNFclauses).

We have some information on PLAs in Buildsystem/ExternalSources/SpecialBuilds/docus/Espresso.hpp. We need to have full information there.

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!

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 xorconstraint can be merged.
Definition in file general.hpp.