OKlibrary  0.2.1.6
Methods.hpp File Reference

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 hitting-clause-set todos and move method here
Todo:
Add instructions for using Pseudo-boolean 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))," ",1-last(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 4-bit 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
    1---01-- 1
    -0--00-- 1
    0---1-0- 1
    --11---1 1
    -1--1--1 1
    --1--0-1 1
    1-----10 1
    --0---00 1
    -111-1-- 1
    -10-01-- 1
    10-1-0-- 1
    --001-1- 1
    -0-1-11- 1
    --101-0- 1
    ---0110- 1
    0-0-0--1 1
    -1-0--01 1
    0-10---0 1
    -1-10--0 1
    -0-1--10 1
    -101-01- 1
    00---111 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 [ESPRESSO-SIGNATURE: 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 clause-set 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> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG 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 clause-set 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 clause-set 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 4-bit 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 clause-set. 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 4-bit 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 4-bit 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 clause-set 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> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_byte_field_mul_full_2.cnf> AES_byte_field_mul_2_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > 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 ubcsat-okl to find small solutions like so:
    shell> ubcsat-okl  -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 clause-set:
    shell> ubcsat-okl  -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 new-ubcsat-okl 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 "QuineMcCluskey-n16-O3-DNDEBUG" to generate the prime implicates:
    shell> QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox_full.cnf > sbox_pi.cnf
       
Todo:
Add todos.

Definition in file Methods.hpp.