OKlibrary  0.2.1.6
GeneralisedConstraintTranslation.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 22.5.2011 (Swansea) */
00002 /* Copyright 2011, 2012, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 /* We use the same variables and round-specific functions as the full DES
00023    translation, so include them: */
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Conversions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac");
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/DataEncryptionStandard/ConstraintTranslation.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/RoundFunction.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/KeySchedule.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/LinearEquations.mac")$
00031 
00032 /*
00033   Considering generalised DES, that is, DES with an arbitrary number of rounds.
00034 */
00035 
00036 /* ***********************
00037    * The complete system *
00038    ***********************
00039 */
00040 
00041 /* All xor-constraints: */
00042 des_xor_gen(r) := lappend(create_list(des_round_xor(r_t),r_t,1,r))$
00043 
00044 /* All sbox-constraints: */
00045 des_sboxc_gen(r) := lappend(create_list(des_sbox_deso(r_t),r_t,1,r))$
00046 
00047 
00048 /*
00049    Allowing arbitrary DES S-box constraints built from 6x1-bit S-box functions,
00050    where the boxes are specified by lists of the indices of the output-bits
00051    they output (1,...,32).
00052 */
00053 
00054 /* Inputs bits (indices) necessary to compute the given output bit: */
00055 des_sbox_output2inputs(i) := create_list(floor((i-1)/4)*6 + j, j, 1, 6)$
00056 des_sbox_outputs2inputs(L) := stable_unique(lappend(map(des_sbox_output2inputs,L)))$
00057 /* Computing the S-boxes constraints for r in {1,...,16}, where out_l is a
00058    list of lists of indices in 1,..,32
00059    (one list for each "arbitrary"/"combined" S-box): */
00060 des_sbox_deso_l(out_l,r) := block(
00061  [I : create_list(create_list(desi_var(i,r),i,des_sbox_outputs2inputs(C)),C,out_l),
00062   O : create_list(create_list(deso_var(i,r),i,C),C,out_l)],
00063   create_list([i,I[i],O[i]], i,1,length(out_l)))$
00064 /* Specifying the output bits each S-box outputs; allowing arbitary
00065    (possibly smaller or larger) S-boxes to be used: */
00066 des_sboxc_gen_l(output_bits_l, r) :=
00067   lappend(create_list(des_sbox_deso_l(output_bits_l, r_t),r_t,1,r))$
00068 
00069 
00070 /* All (constraint-)variables: */
00071 des_var_gen(r) := append(
00072  /* Key variables first as they don't change */
00073  create_list(desk_var(i), i,1,64),
00074  lappend(
00075    create_list(
00076      append(
00077        create_list(desr_var(i,r_t),i,1,32),
00078        if r_t > 0 then create_list(desi_var(i,r_t),i,1,48) else [],
00079        if r_t > 0 then create_list(deso_var(i,r_t),i,1,32) else []),
00080      r_t,-1,r)))$
00081 
00082 
00083 /* **************************************************************
00084    * Assignments to plaintext, key and ciphertext variables     *
00085    **************************************************************
00086 */
00087 
00088 
00089 /*
00090   Translating plaintext-, ciphertext- and key-assignments into formal
00091   clause-sets and partial assignments, using partial boolean vectors.
00092   A "partial boolean vector" contains besides 0,1 also possibly "und".
00093 */
00094 
00095 /* Synonym for des_plain2pa for DES with an arbitrary number or rounds: */
00096 des_plain2pa_gen(plain) := des_plain2pa(plain)$
00097 /* Synonym for des_plain2fcl for DES with an arbitrary number or rounds: */
00098 des_plain2fcl_gen(plain) := des_plain2fcl(plain)$
00099 /* The plaintext variables are always the same list of variables, no matter
00100    the number of rounds. */
00101 
00102 /* Translating the partial boolean vector, cipher, of length 64, to
00103    the corresponding partial assignment on the DES ciphertext variables. The
00104    partial assignment sets the i-th ciphertext variable of the r-round DES
00105    to cipher[i], for all i where cipher[i] is defined. */
00106 des_cipher2pa_gen(cipher,r) := block(
00107   [V : create_list(desr_var(i,r_t), r_t,[r,r-1], i,1,32)],
00108   setify(
00109     delete(und,
00110          create_list(block([x:cipher[i]],
00111              if x=und then und else (2*x-1)*V[des_final_permutation[i]]),
00112            i,1,64))))$
00113 /* Now translating cipher to a formal clause-list containing exactly the
00114    unit-clauses satisfied by des_cipher2pa(cipher). The variable list is
00115    the list of all ciphertext variables. The order of the variable-
00116    and clause-lists is the standard one on the DES ciphertext variables. */
00117 des_cipher2fcl_gen(cipher,r) := block(
00118   [V : create_list(desr_var(i,r_t), r_t,[r,r-1], i,1,32), L],
00119   L : sort(listify(des_cipher2pa(cipher)), l2order_p(interleave_l(-V,V))),
00120   [V, map(set,L)])$
00121 
00122 /* Synonym for des_key2pa for DES with an arbitrary number or rounds: */
00123 des_key2pa_gen(key) := des_key2pa(key)$
00124 /* Synonym for des_key2fcl for DES with an arbitrary number or rounds: */
00125 des_key2fcl_gen(key) := des_key2fcl(key)$
00126 /* The key variables are always the same list of variables, no matter the
00127    number of rounds. */
00128 
00129 
00130 /* Generating random plaintext-key-ciphertext triples: */
00131 
00132 
00133 /* Generating a triple of DES plaintext, key and ciphertext as 64-element
00134    boolean-vectors where the plaintext and key have been generated by a
00135    pseudo-random number generator. The pseudo-random number generator is
00136    initialised using positive-integer seed. */
00137 des_random_pkctriple(seed,r) := block([P_hex,K_hex,C_hex],
00138   set_random(make_random_state(seed)),
00139   P_hex : lpad(int2hex(random(2**64)),"0",16),
00140   K_hex : lpad(int2hex(random(2**64)),"0",16),
00141   C_hex : des_encryption_hex_gen(r, P_hex,K_hex),
00142   return(map(hexstr2binv, [P_hex,K_hex,C_hex])))$
00143 
00144 
00145 /* A pseudo-random plaintext-key-ciphertext-triple as a partial assignment: */
00146 des_random_pkctriple_pa(seed,r) := block([rnd_pkc,P,K,C,pa],
00147   rnd_pkc : des_random_pkctriple(seed,r),
00148   P : des_plain2pa_gen(rnd_pkc[1]),
00149   K : des_key2pa_gen(rnd_pkc[2]),
00150   C : des_cipher2pa_gen(rnd_pkc[3],r),
00151   return(union(P,K,C)))$
00152 /* A pseudo-random plaintext-key-ciphertext-triple as a partial assignment,
00153    standardising the variable names to 1,...,length(des_var_gen(r));
00154    the order given by des_var_gen(r): */
00155 des_random_pkctriple_pa_std(seed,r) := block([pa, std_var_map],
00156   std_var_map : sm2hm(l2osm_inv(des_var_gen(r))),
00157   pa : des_random_pkctriple_pa(seed,r),
00158   pa : substitutetotal_c(pa,std_var_map),
00159   return(pa))$
00160 /* Now outputting the pseudo-random plaintext-key-ciphertext-triple as a
00161    partial assignment, with standardised variable names to the file
00162    des_pkctriple_r${r}_s${seed}.pa: */
00163 output_des_random_pkctriple_pa_std(seed,r) :=
00164   output_pa(
00165     des_random_pkctriple_pa_std(seed,r),
00166     sconcat("des_pkctriple_r",r,"_s",seed,".pa"))$
00167 /* Now generating a pseudo-random plaintext-key-ciphertext-triple as a
00168    partial assignment, without the key variables in the output: */
00169 des_random_pcpair_pa(seed,r) := block([rnd_pkc, P, C, pa],
00170   rnd_pkc : des_random_pkctriple(seed,r),
00171   P : des_plain2pa_gen(rnd_pkc[1]),
00172   C : des_cipher2pa_gen(rnd_pkc[3],r),
00173   return(union(P,C)))$
00174 des_random_pcpair_pa_std(seed,r) := block([pa, std_var_map],
00175   std_var_map : sm2hm(l2osm_inv(des_var_gen(r))),
00176   pa : des_random_pcpair_pa(seed,r),
00177   pa : substitutetotal_c(pa,std_var_map),
00178   return(pa))$
00179 output_des_random_pc_pa_std(seed,r) :=
00180   output_pa(
00181     des_random_pcpair_pa_std(seed,r),
00182     sconcat("des_pcpair_r",r,"_s",seed,".pa"))$
00183 /* Now generating a pseudo-random plaintext-key-ciphertext-triple as a
00184    partial assignment, without the ciphertext variables in the output: */
00185 des_random_pkpair_pa(seed,r) := block([rnd_pkc, P, K, pa],
00186   rnd_pkc : des_random_pkctriple(seed,r),
00187   P : des_plain2pa_gen(rnd_pkc[1]),
00188   K : des_key2pa_gen(rnd_pkc[2]),
00189   return(union(P,K)))$
00190 des_random_pkpair_pa_std(seed,r) := block([pa, std_var_map],
00191   std_var_map : sm2hm(l2osm_inv(des_var_gen(r))),
00192   pa : des_random_pkpair_pa(seed,r),
00193   pa : substitutetotal_c(pa,std_var_map),
00194   return(pa))$
00195 output_des_random_pk_pa_std(seed,r) :=
00196   output_pa(
00197     des_random_pkpair_pa_std(seed,r),
00198     sconcat("des_pkpair_r",r,"_s",seed,".pa"))$
00199 /* Now generating a pseudo-random plaintext-key-ciphertext-triple as a
00200    partial assignment, without the plaintext variables in the output: */
00201 des_random_kcpair_pa(seed,r) := block([rnd_pkc, K, C, pa],
00202   rnd_pkc : des_random_pkctriple(seed,r),
00203   K : des_key2pa_gen(rnd_pkc[2]),
00204   C : des_cipher2pa_gen(rnd_pkc[3],r),
00205   return(union(K,C)))$
00206 des_random_kcpair_pa_std(seed,r) := block([pa, std_var_map],
00207   std_var_map : sm2hm(l2osm_inv(des_var_gen(r))),
00208   pa : des_random_kcpair_pa(seed,r),
00209   pa : substitutetotal_c(pa,std_var_map),
00210   return(pa))$
00211 output_des_random_kc_pa_std(seed,r) :=
00212   output_pa(
00213     des_random_kcpair_pa_std(seed,r),
00214     sconcat("des_kcpair_r",r,"_s",seed,".pa"))$
00215 
00216 
00217 /* ***********************
00218    * CNF translation     *
00219    ***********************
00220 */
00221 
00222 /* Generates a CNF formal clause-list representing the r-round DES.
00223 
00224    Sbox i is translated using the formal clause-list sbox_l[i] for i in
00225    {1,...,8}. The input and output variables of Sbox i are
00226    [sbox_l[i][1],...,sbox_l[i][10]]. All other variables in sbox_l[i] are
00227    auxilliary variables used by the representation.
00228    Xor constraints are translated using their prime implicates. */
00229 des2fcl_gen(sbox_l, r) := block(
00230   [xor_cl_l, sbox_cl_l : [], num_sbox_aux_var_l,
00231    new_var_ind : 1, rename_aux_vars],
00232   xor_cl_l : create_list(even_parity_wv_cl(C[1]), C, des_xor_gen(r)),
00233   num_sbox_aux_var_l : create_list(length(sbox_l[i][1])-10, i, 1, 8),
00234   rename_aux_vars : lambda([sbox_cst],
00235     block([aux_vars],
00236       aux_vars :
00237         create_list(desaux_var(i),
00238           i, new_var_ind, new_var_ind + num_sbox_aux_var_l[sbox_cst[1]]-1),
00239       new_var_ind : new_var_ind + num_sbox_aux_var_l[sbox_cst[1]],
00240       rename_fcl(sbox_l[sbox_cst[1]],
00241         append(sbox_cst[2],sbox_cst[3],aux_vars))[2])),
00242   sbox_cl_l : map(rename_aux_vars, des_sboxc_gen(r)),
00243   return([append(des_var_gen(r),create_list(desaux_var(i),i,1,new_var_ind-1)),
00244           lappend(append(xor_cl_l,reverse(sbox_cl_l)))]))$
00245 /* Outputting the DES translation to file, where sbox_name is an alphanumeric
00246    string without spaces identifying the S-box translation: */
00247 output_des2fcl_gen(sbox_name, sbox_l, r, n) := block([Fs],
00248   Fs : standardise_fcl(des2fcl_gen(sbox_fcl_l,r)),
00249   output_fcl_v(
00250     sconcat(r, "-round DES; translated using the ", sbox_name,
00251             " translation for the S-boxes (6-to-4)."),
00252     Fs[1],n, Fs[2]))$
00253 output_des2fcl_gen_std(sbox_name, sbox_l, r) :=
00254   output_des2fcl_gen(sbox_name, sbox_l, r,
00255     sconcat("des_6t4_",sbox_name,"_r",r,".cnf"))$
00256 /* Allowing arbitrary S-boxes specified by a list of lists of the output
00257    bits they produce (the inputs bits are determined from these): */
00258 des2fcl_gen_l(sbox_l,sbox_outputs_l, r) := block(
00259   [xor_cl_l, sbox_cl_l : [], num_sbox_aux_var_l,
00260    new_var_ind : 1, rename_aux_vars],
00261   xor_cl_l : create_list(even_parity_wv_cl(C[1]), C, des_xor_gen(r)),
00262   rename_aux_vars : lambda([sbox_cst],
00263     block([aux_vars,
00264        num_aux_vars :
00265          length(sbox_l[sbox_cst[1]][1]) -
00266            (length(sbox_cst[2]) + length(sbox_cst[3]))],
00267       aux_vars :
00268         create_list(desaux_var(i),
00269           i, new_var_ind, new_var_ind + num_aux_vars-1),
00270       new_var_ind : new_var_ind + num_aux_vars,
00271       rename_fcl(sbox_l[sbox_cst[1]],
00272         append(sbox_cst[2],sbox_cst[3],aux_vars))[2])),
00273   sbox_cl_l : map(rename_aux_vars, des_sboxc_gen_l(sbox_outputs_l,r)),
00274   return([append(des_var_gen(r),create_list(desaux_var(i),i,1,new_var_ind-1)),
00275           lappend(append(xor_cl_l,reverse(sbox_cl_l)))]))$
00276