Methods for finding various representations of the AES boxes.
More...
Go to the source code of this file.
Detailed Description
Methods for finding various representations of the AES boxes.
 Todo:
 Overview

In the following file we present various methods which are useful for computing different representations of the AES boxes.

For finding minimum and small (minimal) representations of the AES boxes, we have:

Espresso.

Minimising using hypergraph transversal tools.

Minimisation using Iterative SAT methods.

Maxima functions.

R QCA package.

Minimisation using Weighted MaxSAT.

For computing the prime implicates, we have:
 Todo:
 Connections

See Investigations/BooleanFunctions/plans/Permutations.hpp for general investigations on permutations of {0,1}^n.
 Todo:
 Tidy hittingclauseset todos and move method here
 Todo:
 Add instructions for using Pseudoboolean SAT solvers for minimisation

Pseudoboolean or PB SAT solvers offer the ability to encode linear constraints such as cardinality constraints into a specialised CNF format.

Such solvers might better handle cardinality constraints compared to the translations used in "Iterative SAT solving", and so we# should investigate their use.
 Todo:
 Espresso

Espresso is a popular logic minimisation tool with a variety of methods for generating small and minimum sized logical representations.

To use Espresso we must give a "pla" file as input. Therefore we must translate a full CNF (as generated by functions in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/SboxAnalysis.mac etc) into a PLA file:
fcl2tt(FF) :=
append(
map(lambda([C],
endcons(0,
map(lambda([L], if elementp(L, C) then 0 else 1), FF[1]))), FF[2]),
listify(map(lambda([C],
endcons(1,
map(lambda([L], if elementp(L, C) then 0 else 1), FF[1]))),
setdifference(all_tass(FF[1]),setify(FF[2])))))$
output_tt2pla(TT, n) :=
with_stdout(n,
if length(TT) = 0 then block(print(".i 0"), print(".0 1"))
else block(
print(".i ", length(TT[1])1),
print(".o 1"),
for tt_line in TT do
print(apply(sconcat,rest(tt_line,1))," ",1last(tt_line))))$
Note here that the truth table produced is then negated for representation in the PLA file, as we want espresso to minimise the CNF and by default it will find a minimum/minimal representation of the DNF.

So for example, to generate the small scale 4bit sbox as a PLA file, we then do:
maxima> SboxCNF: fcs2fcl(ss_sbox_fullcnf_fcs(2,4,ss_polynomial_2_4))$
maxima> output_tt2pla(fcl2tt( SboxCNF ),"Sbox.pla")$

To then minimise the boxes, we can then use either the "exact" or "signature" methods of the espresso utility:
shell> espresso2.3 Dexact Sbox.pla
.i 8
.o 1
.p 22
101 1
000 1
010 1
111 1
111 1
101 1
110 1
000 1
1111 1
1001 1
1010 1
0011 1
0111 1
1010 1
0110 1
0001 1
1001 1
0100 1
1100 1
0110 1
10101 1
00111 1
.e
Note that "espresso2.3 Dsignature Sbox.pla" should yield the same result, but may have different complexity depending on the input.

The exact and signature algorithms are discussed in [ESPRESSOSIGNATURE: A New Exact Minimizer for Logic Functions; Mcgeer,Sanghavi,Brayton,Vincentelli].

We need a conversion function from the PLA format back to a CNF file.

The above code on PLA generation should be moved into the appropriate Maxima file.
 Todo:
 Minimising using hypergraph transversal tools

Given a full CNF as generated by one of the box CNF generation functions (see ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac etc), for example:
maxima> output_ssmult_fullcnf_stdname(2,2,4,ss_polynomial_2_4);
we can generate the subsumption hypergraph for this clauseset and its prime implicates, and then use tools within the OKlibrary to compute all minimum transversals of the generated hypergraph, and hence all minimum CNF representations.

This can be done like so:
shell> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG ss_byte2_4_field_mul_full_2.cnf > ss_byte2_4_field_mul_shg_2.cnf
shell> BoundedTransversals_bv < ss_byte2_4_field_mul_shg_2.cnf > ss_byte2_4_field_mul_transversals_2.cnf

We can generate all minimum CNF representations using a provided script:
shell> ${OKPLATFORM}/OKsystem/OKlib/Satisfiability/Optimisation/all_minimum_cnf ss_byte2_4_field_mul_full_2.cnf
shell> echo ss_byte2_4_field_mul_full_2.cnf.trans_*  wc w
2
 Todo:
 Minimisation using Iterative SAT methods

Optimising the size of CNF representations for a given clauseset using standard SAT solvers can be approached by generating the subsumption hypergraph for the original (full) CNF and its prime implicates and then adding additional cardinality clauses to the subsumption hypergraph restricting the number of variables set to true and hence the number of clauses in our representation.

By continuing to reduce the cardinality of the result until the subsumption hypergraph clauseset is unsatisfiable (i.e., there is no CNF representation with a number of clauses less than the cardinality), we can iteratively search for the solution.

So, for example, we generate the subsumption hypergraph for the 4bit small scale Sbox like so:
maxima> output_ss_sbox_fullcnf_stdname(2);
and then shell> ${OKPLATFORM}/OKsystem/OKlib/Satisfiability/Optimisation/minimise_cnf_oksolver ss_byte2_4_field_mul_full_2.cnf
c Starting level 14
c Starting level 13
c Starting level 12
c Starting level 11
c Starting level 10
c Starting level 9
c Starting level 8
c Found (a) minimum size representation for " ss_byte2_4_field_mul_full_2.cnf " of size 9
c Subsumption hypergraph for the minimisation problem for ss_byte2_4_field_mul_full_2.cnf
p cnf 8 9
5 2 0
2 5 0
6 3 0
3 6 0
7 1 4 0
4 1 7 0
8 7 4 0
8 4 7 0
1 8 0

Note the above uses the OKsolver to check for satisfiability of each clauseset. Further scripts should be written to check using other solvers. See "Solvers to be used for experimentation" in Cryptography/AdvancedEncryptionStandard/plans/Experimentation.hpp.
 Todo:
 Maxima functions

Given a full CNF as generated by one of the box CNF generation functions (see ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac etc), we can generate all minimum CNF representations like so:
ss_mul3_min_cnfs : all_minequiv_bvs_cs(ssmult_fullcnf_fcs(3,2,4,ss_polynomial_2_4)[2])$

To just generate the prime implicates, we have:
> ss_box_pi : min_2resolution_closure_cs(
fcs2cs(ss_sbox_fullcnf_fcs(3,4,ss_polynomial_2_4)) )$
 Todo:
 R QCA package

The R QCA package is written to deal with problems arising from sociology, derives small CNF/DNF representations for (partial) truth tables (see "Packages" in BuildSystem/ExternalSources/SpecialBuilds/plans/R.hpp).

To use the R QCA package we must a truth table as a data file readable by the R systems readtable function. Therefore we must translate a full CNF (as generated by functions in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/SboxAnalysis.mac etc) into a table format:
fcl2tt(FF) :=
append(
map(lambda([C],
endcons(0,
map(lambda([L], if elementp(L, C) then 0 else 1), FF[1]))), FF[2]),
listify(map(lambda([C],
endcons(1,
map(lambda([L], if elementp(L, C) then 0 else 1), FF[1]))),
setdifference(all_tass(FF[1]),setify(FF[2])))))$
output_tt2table(TT, n) :=
with_stdout(n,
if length(TT) = 0 then (print("O"), print(1))
else block(
apply(print, endcons("O",create_list(i,i,1,length(TT[1])1))),
for tt_line in TT do
apply(print,tt_line)))$

So for example, to generate the small scale 4bit sbox as a R data file, we then do:
maxima> SboxCNF: fcs2fcl(ss_sbox_fullcnf_fcs(2,4,ss_polynomial_2_4))$
maxima> output_tt2table(fcl2tt(SboxCNF),"Sbox.dat")$

We can then use the R QCA package to try to generate a small representation:
R> oklib_load_all()
R> library(QCA)
R> sbox_tt = read.table("Sbox.dat",header=TRUE)
R> eqmcc(sbox_tt, outcome="O", expl.0=TRUE)

This method is unlikely to yield much however, as even for this smaller problem (the example 4bit Sbox), we get:
Error: Impossible to solve the PI chart (too many possible combinations).
 Todo:
 Minimisation using Weighted MaxSAT

Given a full CNF as generated by one of the box CNF generation functions (see ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac etc), for example:
maxima> output_rijnmult_fullcnf_stdname(2);
we can generate the subsumption hypergraph for this clauseset and its prime implicates, and then convert this to a weighted MaxSAT problem, which encodes that we wish to find an assignment setting the minimum number of variables to true: shell> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG AES_byte_field_mul_full_2.cnf> AES_byte_field_mul_2_shg.cnf  MinOnes2WeightedMaxSATO3DNDEBUG > AES_byte_field_mul_2_shg.wcnf

We can then use both complete and incomplete weighted partial MaxSAT solvers to find minimum and small (minimal) solutions.

We can use ubcsatokl to find small solutions like so:
shell> ubcsatokl alg gsat w runs 100 cutoff 1000000 i AES_byte_field_mul_2_shg.wcnf
and then assuming we find a good solution, we can then extract the solution as a CNF file of the small size clauseset: shell> ubcsatokl alg gsat w runs 100 cutoff 1000000 wtarget 20 solve 1 seed 1402276559 i AES_byte_field_mul_2_shg.wcnf r model AES_byte_field_mul_2_m20.result;
shell> cat AES_byte_field_mul_full_2.cnf_primes  FilterDimacs AES_byte_field_mul_2_m20.result

See "Add newubcsatokl as an option for run_ubcsat" in ExperimentSystem/ControllingLocalSearch/plans/DataCollection.hpp for discussion on extending run_ubcsat to allow us to find good algorithms for such minimisation problems.

Add discussion of complete MaxSAT solvers.
 Todo:
 C++ QuineMcCluskey methods

One method for generating the prime implicates of a particular boolean function is to use the C++ QuineMcCluskey implementation, by generating the full CNF as a DIMACS file:
maxima> output_rijnsbox_fullcnf_stdname();
which, in this example, generates the file "AES_Sbox_full.cnf" and then using "QuineMcCluskeyn16O3DNDEBUG" to generate the prime implicates: shell> QuineMcCluskeyn16O3DNDEBUG AES_Sbox_full.cnf > sbox_pi.cnf
 Todo:
 Add todos.
Definition in file Methods.hpp.