general.hpp File Reference

On investigations into KeeLoq cipher. More...

Go to the source code of this file.

Detailed Description

On investigations into KeeLoq cipher.

  • KeeLoq is a 528-round iterated shift-register cipher with 32-bit plaintext, and ciphertext, and 64-bit keys.
  • The KeeLoq encryption cipher consists of the following:
  • A key point here is that the KeeLoq round function is the combination of a small XXX and the XOR of X more bits, meaning that the entire round function is a XX bit boolean function.
  • Algebraic attacks using SAT solvers are discussed in [Algebraic and Slide Attacks on KeeLoq; Bard, Courtois, Wagner 2008], theoretically breaking the cipher in time equivalent to 2^53 encryptions, compared to 2^64 for brute-force.
Analysing the KeeLoq round function
  • The KeeLoq round function is given as a boolean function by the Maxima function keeloq_round_bf in Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/Cipher.mac.
  • Computing statistics:
    maxima> Round_DNF : bf2fulldnf_fcl(keeloq_round_bf,9)$
    maxima> statistics_fcs(Round_DNF);
    maxima> Round_CNF : bf2fullcnf_fcl(keeloq_round_bf,9)$
    maxima> statistics_fcs(Round_CNF);
    maxima> output_fcs("KeeLoq Round Function", Round_CNF, "KeeLoq_Round_full.cnf")$
    shell> QuineMcCluskeySubsumptionHypergraphWithFullStatistics-n16-O3-DNDEBUG KeeLoq_Round_full.cnf > KeeLoq_Round_full.cnf_shg
    shell> cat KeeLoq_Round_full.cnf_primes_stats
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
          9     224      9      9     224     1760     NA     NA     224     1760     0
     length   count
          7      32
          8     192
    shell> cat KeeLoq_Round_full.cnf_shg_stats
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
        224     256    224    224     256      512     NA     NA     256      512     0
     length   count
          2     256
    shell> ${OKplatform}/OKlib/Satisfiability/Optimisation/minimise_cnf_cryptominisat KeeLoq_Round_full.cnf > KeeLoq_Round_min.cnf
    shell> cat KeeLoq_Round_min.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG
         pn      pc      n    nmi       c        l     n0   n0mi      c0       l0  cmts
          9      96      9      9      96      736     NA     NA      96      736     1
     length   count
          7      32
          8      64
    maxima> Round_primes : read_fcl_f("KeeLoq_Round_full.cnf_primes")$
    maxima> Round_min : read_fcl_f("KeeLoq_Round_min.cnf")$
    maxima> hardness_wpi_cs(setify(Round_min[2]), setify(Round_primes[2]));
    So the minimum representation has hardness 1!
  • Investigating the ANF to CNF encoding for the KeeLoq round used in [Algebraic and Slide Attacks on KeeLoq; Bard, Courtois, Wagner 2008]:
     /* Generating the encoding: */
    maxima> Round_anf : lappend(map(lambda([v,C], cons(adjoin(v,map("-",C)),create_list({-v,l},l,listify(C)))),[10,11,12,13,14,15,16,17,18,19,20],[{4,6},{4,8},{5,6},{5,8},{6,7},{7,8},{11,7},{11,6},{20,7},{20,6},{4,5}]))$
    maxima> Round_par_anf : append(
    XXX Apparently each fullxoreqs_wv_fcl(m,1,L) just expresses that the first
        variable in L is equal to all the others ???
    maxima> Round_anf : append(Round_anf,Round_par_anf);
    maxima> statistics_cs(Round_anf);
    /* Checking we compute the right function: */
    maxima> for C in Round_CNF[2] do assert(ucp_0_cs(apply_pa_cs(comp_sl(C),setify(Round_anf))) = {{}});
    maxima> for C in Round_DNF[2] do assert(ucp_0_cs(apply_pa_cs(C,setify(Round_anf))) = {});
     /* Computing a lower-bound on the hardness, the hardness w.r.t the prime
        implicates on the original variables: */
     maxima> hardness_wpi_cs(setify(NLF_nv), setify(Round_primes[2]));
    So the ANF representation used has a higher hardness, and is also a larger representation. The minimum 1-base above should be a much better representation of the KeeLoq round function.
  • KeeLoq should be implemented at the Maxima level, and then translated, so that we can compare these translations.

Definition in file general.hpp.