Plans for the cryptanalysis of the Data Encryption Standard in Maxima/Lisp.
More...
Go to the source code of this file.
Detailed Description
Plans for the cryptanalysis of the Data Encryption Standard in Maxima/Lisp.
 Todo:
 Convenience functions

Convenience functions are needed for the translations of the DES and generalisedDES to SAT.

A function such as output_des_fcl(sbox_l,n) should be written which outputs the result of des_fcl(sbox_l) to the file n.

We also need a function, output_des_fcl_kd(sbox_l,seed,n), for outputting a random DES key discovery instance.

output_des_fcl_kd should generate a random plaintext and ciphertext using the seed, and output the result of des_fcl, with the plaintext and ciphertext unitclauses to the file n.
 Todo:
 Variable ordering and standardisation

At present, the variables in the standard translation of the full DES, des2fcl(...)[1], are in the order:

First half of input: 32 variables, desr(i,1) for i in [1,...,32];

Second half of input: 32 variables, desr(i,0) for i in [1,...32];

Result of each round: 16 * 32 = 512 variables, desr(i,r) for r in [1,...,16] and i in [1,...,32];

Key variables: 64 variables, desk(i) for i in [1,...,64];

Result of xor with key in each round: 16 * 48 = 768 variables, desi(i,r) for r in [1,...,16] and i in [1,...,48];

Result of Sboxes: 16 * 32 = 512 variables, deso(i,r) for r in [1,...,16] and i in [1,...,32].

Auxilliary variables for Sbox translations.

The variables in the generalised translation of the mround DES, des2fcl_gen(...,r)[1], are in the order:

Key variables: 64 variables, desk(i) for i in [1,...,64];

First half of input: 32 variables, desr(i,1) for i in [1,...,32]);

Second half of input: 32 variables, desr(i,0) for i in [1,...32];

For each round r in [1,...,16]:

Result of each round: 16 * 32 = 512 variables, desr(i,r) fpr i in [1,...,32];

Result of xor with key in each round: 16 * 48 = 768 variables, desi(i,r) for r in [1,...,16] and i in [1,...,48];

Result of Sboxes: 16 * 32 = 512 variables, deso(i,r) for r in [1,...,16] and i in [1,...,32].

Auxilliary variables for Sbox translations.

These variable orderings were based on the the general structure and order of the DES specification.

There is a clear separation between the standard DES and generalised DES, and so they have different variable orderings.

We must decide whether these variable orderings are suitable, and whether the order makes sense when standardising with standardise_fcl:

In the translation of the generalised DES, the current order of the variables ensures that variables have the same index, whether they appear in a translation of 10round DES or 12round DES.

This is a desirable property, as it makes it easier to compare translations, and to remember which variables are which, as the number of rounds in the translation changes.

A key question is: should the order of the auxilliary variables be fixed?

It is better not to include auxilliary variables in the "round by round" variables of the generalised translation. That way, the round variables, such as desi(...) etc, keep the same index across different Sbox translations of the DES.
 Todo:
 Sbox boolean 6xm functions

Consider the 4 boolean 6 x 1 functions for each DES Sbox; see des_sbox_bit_fulldnf_cl and des_sbox_bit_fullcnf_fcs in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/DataEncryptionStandard/Sboxes.mac.

We wish to translate the DES where the Sbox is considered as 4 6x1 boolean functions.

There is also the possibility of generalising this to 4/m boolean 6xm functions, or even combinations of 1 6x2 and 2 6x1 boolean functions.

This is possible in several ways:

We provide several constraint generators:

des_sboxc: generator for standard Sbox constraints as boolean 6x4 functions.

des_sboxc_6tm: generator for the DES Sboxes as boolean 6xm functions, where m in {1,2,4} is given as an additional parameter.

des_sboxc_6t_l: generator for the DES Sboxes for arbitrary list L where the Sboxes occur as 6xL[1], 6xL[2],..., 6xL[n] boolean functions where n is the length of L.

des_sboxc_6t_l is likely too much of a generalisation, but des_sboxc_6tm and generalisations of des2fcl etc, using des_sbox_6tm are definitely necessary.

Translating the 6x4 DES Sboxes to smaller 6x1 or 6x2 constraints when we translate to SAT or CSP:

In this way, des_sboxc and des2fcl remain the same, but when using, for instance, des2fcl, the formal clauselists for each Sbox are the union of the clauselists for 4 Sbox boolean 6x1 functions.

It seems best to provide several constraint generators, so that we see all different types of constraint in their own right.
 Todo:
 Add variants with reduced number of rounds

Variants of DES with smaller numbers of rounds (from 1 to 3) are considered in [Logical cryptanalysis as a SAT problem; Massaci and Marraro].

For discussions of the notion of "DES with reduced number of rounds", see "Add variants with reduced number of rounds" in ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/plans/general.hpp.

The translations of variants with smaller numbers of rounds will be investigated just as much as the full DES.

Tests are needed for all functions.

DONE Variable ordering:

The variables returned by des_var should be ordered "round by round". That is, the variables for round i+1 should occur after round i in the list.

Using a "round by round" order on the variables ensures that all variables from round i always have the same index after standardisation, no matter the variant we use.

DONE This "round by round" variable ordering scheme differs from the original ordering used for the full DES translation. It is more complex and so we keep the original DES translation and put the functions for the generalised version in "GeneralisedConstraintTranslation.mac".

DONE We need to implement translations of these variants to compare.

DONE We should offer generalised versions of the current functions.

DONE These generalised functions should take the number r of rounds.

DONE So the following functions should be created with an additional round parameter r:

des_xor() > des_xor_gen(r).

des_sboxc() > des_sboxc_gen(r).

des_var() > des_var_gen(r).

des_cipher2fcl(cipher) > des_cipher2fcl_gen(r,cipher).

des2fcl(sbox_l) > des2fcl_gen(r,sbox_l).

DONE (To test the water first, we implement "_gen" versions of each function) Therefore in this case, the full DES should be considered a special case of the general scheme with an arbitrary number of rounds. A special convenience function needs then to be provided for the translation of the 16 round DES.
 Todo:
 Improve tests
 Todo:
 Create constraint evaluation system

We wish to provide tests for functions such as "des_round_xor". To do this, we must evaluate the generated constraints.

We need a constraint evaluation system.

This system should:

Take a list of constraints.

Take an assignment to all "input varables". The "input variables" should be enough to determine all others.

Evaluate each constraint using an associated evaluation function. For example functions in ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/Cipher.mac.

Propagate the inferred variables for each constraint to all others.

Return the assignment to the variables after all propagations.
 Todo:
 TripleDES
 Todo:
 Links
 Todo:
 Translating the constraintsystem into SAT, CSP, ...

In Cryptanalysis/DataEncryptionStandard/ConstraintTranslation.mac we compute the "constraint system" corresponding to the DESconstraint.

Now translations into SAT, CSP etc. are needed.

SAT translation:

Constraint translation:

We already translate to a system of high level constraints.

We have two types of constraints in the DES:

Sbox constraints:

The constraint for the 6x4 boolean function for DES Sbox i is a list of the form [i,[v_1,...,v_6],[w_1,...,w_4]].

i indicates the constraint represents DES Sbox i.

[v_1,...,v_6] are the 6 input variables.

[w_1,...,w_4] are the 4 output variables.

How to represent the 6x1 Sbox boolean functions? Or more generally 6xm for m < 4?

For the 6x1 Sbox boolean functions, we must specify the output bit, so we have the constraint where w_1 is the jth output variable of the ith DES Sbox.

More generally, we have 6xm Sbox constraints:
[i,[v_1,...,v_6],[w_1,...,w_m],[j_1,...,j_m]]
where w_l is the j_lth output bit of the ith DES Sbox for l in {1,...,m}.

XOR constraints:

See 'The notion of a "linear constraint"' for the details of the XOR constraint.

An XOR constraint is a list [x,b] where x is a list of literals and b is in {0,1}, such that the constraint is that where l is the length of x.

We treat the Sbox (6x4 and 6x1) and XOR constraints as the "boxes" we consider, and therefore (currently) do not consider further decompositions.

As with the AES, we do not translate these constraints to boolean constraints as given in ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/Conditions.mac. See "Translating the constraintsystem into SAT, CSP, ..." in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/plans/general.hpp.

Translating DES constraints to Minion:

We should provide a translation for input into the Minion solver.

Sbox constraints should be translated to "table" constraints where we specify the truth table for each Sbox.

XOR constraints should be translated to "watchsumleq" and "watchsumgeq" constraints.

We need a function "output_des_minion" which takes the number of rounds and uses des_sboxc and des_xor etc to generate the constraints associated with the DES given the input parameters, and outputs the corresponding Minion input file.

We also need a function "output_des_minion_6tm" which takes the number of rounds, and the parameter m and uses des_sboxc_6tm and des_xor_6tm etc to generate the constraints associated with the DES given the input parameters, and outputs the corresponding Minion input file. See "Sbox boolean 6xm functions".

We should also translate to one of the constraint modelling languages; see "Constraint modelling languages" in Buildsystem/ExternalSources/SpecialBuilds/plans/CSP.hpp.

See also "Translating the constraintsystem into SAT, CSP, ..." in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/plans/general.hpp.
 Todo:
 DONE (see des_sbox_bit_fulldnf_cl) Add 6to1 bit Sbox functions
Definition in file general.hpp.