boolcrypt.functionalequations module
Solve functional equations with a SAT solver.
- boolcrypt.functionalequations.reduce(equations, mode='gauss', bpr=None, verbose=False, debug=False, filename=None)[source]
Reduce a Boolean system of equations given as a list of Boolean polynomials.
mode can be “gauss” (a BooleanPolynomialVector is returned) or “groebner” (a PolynomialSequence_gf2 is returned)
>>> from boolcrypt.utilities import lut2anf, matrix2anf, compose_anf_fast >>> sbox3b = [0, 1, 2, 3, 4, 6, 7, 5] # one linear component >>> bpr = BooleanPolynomialRing(3, "x0, x1, x2") >>> equations = lut2anf(sbox3b) >>> list(equations) [x0*x2 + x0 + x1*x2, x0*x2 + x1, x2] >>> m = matrix2anf(sage.all.matrix(bpr, 3, 3, [1, 0, 1, 1, 1, 1, 1, 1, 0])) >>> equations = compose_anf_fast(m, equations) >>> list(equations) [x0*x2 + x0 + x1*x2 + x2, x0 + x1*x2 + x1 + x2, x0 + x1*x2 + x1] >>> list(reduce(equations, mode="gauss", verbose=True, debug=True)) reducing 3 equations with mode gauss and degrees (d,#) Counter({2: 3}) system coefficient matrix: [x0*x2 x0 x1*x2 x1 x2] [-----------------------------] [ 1 1 1 0 1] [ 0 1 1 1 1] [ 0 1 1 1 0] reduced system coefficient matrix: [x0*x2 x0 x1*x2 x1 x2] [-----------------------------] [ 1 0 0 1 0] [ 0 1 1 1 0] [ 0 0 0 0 1] gauss-reduction obtained 3 equations with degrees (d,#) Counter({2: 2, 1: 1}) [x0*x2 + x1, x0 + x1*x2 + x1, x2] >>> reduce(equations, mode="groebner", verbose=True) # sbox3b is a permutation reducing 3 equations with mode groebner and degrees (d,#) Counter({2: 3}) groebner-reduction obtained 3 equations with degrees (d,#) Counter({1: 3}) [x0, x1, x2]
- boolcrypt.functionalequations.find_fixed_vars(equations, only_linear=False, initial_r_mode=None, repeat_with_r_mode=None, initial_fixed_vars=None, bpr=None, check=True, verbose=False, debug=False, filename=None)[source]
Find fixed variables in a system of equations given as a list of Boolean polynomials.
Given a system with Boolean variables x0 > … > xi > … > xn, find fixed/dependent variables, that is, assignments x{i} = f(x{i+1},..,xn). Note that the term order of the Boolean polynomial ring affects the variables that are fixed.
This method returns a pair containing an OrderedDic with the fixed variables found and a BooleanPolynomialVector with the resulting system after replacing the fixed variables by their value/expression.
The parameters initial_r_mode and repeat_with_r_mode can be “gauss” or “groebner” as in reduce(). initial_r_mode is used to reduce the the given list of equations. If repeat_with_r_mode is given, this method is repeatdly called again (with initial reduction the one given by repeat_with_r_mode) until no fixed variables are found.
If the optional parameter initial_fixed_vars is given with a dictionary containing initial fixed variables, this method replaces the expression of these initial fixed variables with the new fixed variables found.
If only_linear=True, only find linear assignment, that is, relations x{i} = f(x{i+1},..,xn) with f of degree up to 1.
If check=True, ensures that no fixed variables appears in the resulting system or in the value/expression of other fixed variable.
verbose and debug determine the amount of information printed to the output. if a string is given to filename, the output is printed to that file
>>> from sage.crypto.sbox import SBox >>> from boolcrypt.utilities import lut2anf >>> sbox3b = SBox((0, 1, 2, 3, 4, 6, 7, 5)) # one linear component >>> list(lut2anf(list(sbox3b))) [x0*x2 + x0 + x1*x2, x0*x2 + x1, x2] >>> bpr = BooleanPolynomialRing(6, "y0, y1, y2, x0, x1, x2", order="lex") >>> input_vars, output_vars = list(reversed(bpr.gens()[3:])), list(reversed(bpr.gens()[:3])) >>> eqs = [bpr(f) for f in sbox3b.polynomials(X=input_vars, Y=output_vars)] >>> eqs = reduce(eqs, mode="groebner", bpr=bpr) >>> list(eqs) [y0 + x0*x2 + x0 + x1*x2, y1 + x0*x2 + x1, y2 + x2] >>> fixed_vars, new_eqs = find_fixed_vars(eqs, only_linear=False, ... verbose=True, debug=True) finding fixed variables in 3 equations with degrees (d, #) Counter({2: 2, 1: 1}) in Boolean PolynomialRing in y0, y1, y2, x0, x1, x2 with term order Lexicographic term order eqs[2] = y2 + x2 found fixed variable y2 <- x2 eqs[1] = y1 + x0*x2 + x1 found fixed variable y1 <- x0*x2 + x1 eqs[0] = y0 + x0*x2 + x0 + x1*x2 found fixed variable y0 <- x0*x2 + x0 + x1*x2 found 3 fixed variables, resulting in 0 equations >>> fixed_vars, list(new_eqs) (OrderedDict([(y2, x2), (y1, x0*x2 + x1), (y0, x0*x2 + x0 + x1*x2)]), []) >>> fixed_vars, new_eqs = find_fixed_vars(eqs, only_linear=True, initial_r_mode="gauss", ... repeat_with_r_mode="gauss", verbose=True, debug=False) reducing 3 equations with mode gauss and degrees (d,#) Counter({2: 2, 1: 1}) gauss-reduction obtained 3 equations with degrees (d,#) Counter({2: 2, 1: 1}) found 1 fixed variables, resulting in 2 equations with degrees (d, #) Counter({2: 2}) > repeating find_fixed_vars with initial reduction_mode gauss reducing 2 equations with mode gauss and degrees (d,#) Counter({2: 2}) gauss-reduction obtained 2 equations with degrees (d,#) Counter({2: 2}) found 1 fixed variables, resulting in 2 equations with degrees (d, #) Counter({2: 2}) > last find_fixed_vars call found 0 new fixed variables and removed 0 equations >>> fixed_vars, list(new_eqs) (OrderedDict([(y2, x2)]), [y0 + x0*x2 + x0 + x1*x2, y1 + x0*x2 + x1]) >>> x, y, z, t = BooleanPolynomialRing(names="x, y, z, t").gens() >>> eqs = [(x*y + z + 1) * (t*z + y) + 1] >>> fixed_vars, new_eqs = find_fixed_vars(eqs, verbose=True, debug=True) finding fixed variables in 1 equations with degrees (d, #) Counter({4: 1}) in Boolean PolynomialRing in x, y, z, t with term order Lexicographic term order eqs[0] = x*y*z*t + x*y + y*z + y + 1 adding equations from common factors eqs[1] = y + 1 found fixed variable y <- 1 eqs[0] = x*z*t + x + z found 1 fixed variables, resulting in 1 equations with degrees (d, #) Counter({3: 1}) >>> fixed_vars, list(new_eqs) (OrderedDict([(y, 1)]), [x*z*t + x + z])
- boolcrypt.functionalequations.solve_functional_equation(lhs_anfs, rhs_anfs, lhs_input_vars, rhs_input_vars, num_sat_solutions, return_mode, find_redundant_equations=None, initial_equations=None, initial_fixed_vars=None, reduction_mode='gauss', only_linear_fixed_vars=False, find_linear_combinations_in_solutions=False, threads=1, num_sols_per_base_sol_to_check=1, bpr=None, ignore_varnames=None, ignore_initial_parsing=False, check_find_fixed_vars=True, return_total_num_solutions=False, verbose=False, debug=False, filename=None)[source]
Solve a functional equation F = G given by list of Boolean polynomials.
This methods requires the CryptoMiniSat package to be installed in SageMath.
The left hand side F(x) = …F1(F0(x)) is given a list of ANF [F0, F1, …], where some of them can be symbolic ANFs. The right hand side G(x) = …G1(G0(x)) can be given similarly [G0, G1, …], or it can be given a list of integers [d0, d1, …, dd]. In the latter case, the problem changes to find F that only have monomials with degrees [d0, d1, …, dd]. At least one of the ANFs Fi or Gj should be a symbolic anf.
lhs_input_vars is a list of the inputs vars (a list of Boolean variables or strings) for each ANF in F (similarly for rhs_input_vars and G). If rhs_anfs is given as a list of integers, the value of rhs_input_vars is ignored.
num_sat_solutions is the number of solutions to be found by the SAT solver. To find all solutions, use None or sage.all.infinity. Note that number of actual solutions can be higher than the number of solutions internally found by the SAT solver, as fixed variables and free variables are not passed to the SAT solver.
If the system of equations is found to be inconsistent (unsatisfiable), a ValueError exception is raised.
If return_mode=”list_anfs”, return a list of solutions [s0, s1, …], where each solution si = [siF, siG] is a pair containing the list of non-symbolic ANFs of the left and right side, that is, [siF, siG] = [[siF0, siF1, …], [siG0, siG1, …]].
If return_mode=”list_coeffs”, return a tuple containing the list of solutions [s0, s1, …], where each si is a list containing the ANF coefficients of [siF, siG], and a list with the free variables.
If return_mode=”symbolic_anf”, the solutions are given symbolically that is, a 4-tuple is returned (symF, symG, eqs, num_sols). For symF = [symF0, symF1, …], symFi is the symbolic ANF of Fi, where each coefficient is substituted with the fixed variables found (and similar for symG and symGi). The list eqs contain the equations that the symbolic coefficients satisfy that could not be reduced more. The number num_sols represents the total number of solutions found.
If return_mode=”symbolic_coeffs”, the solutions are given symbolically but a 3-tuple is returned (fvs, eqs, num_sols). fvs is a dictionary of fixed variables mapping the variables to their symbolic or constant values, and (eqs, num_sols) is similar as in return_mode=”symbolic_anf”.
If return_mode=raw_equations, return the list of equations associated to the functional problem before finding fixed variables and before calling the SAT solver.
If return_mode=”lincomb_solutions”, it returns the linear combinations among the solutions obtained from the SAT solver (see below the explanation regarding find_linear_combinations_in_solutions).
A Boolean polynomial ring bpr can be given to determine the term order. Otherwise, lexicographic order will be used (x0 > x1 > …, F0 > F1 > … > G0 > G1 > … ).
A list of equations can be given in find_redundant_equations. In that case, instead of solving the functional equation, it is returned the list of equations that are satisfied by all solutions.
A list of fixed variables can be given in initial_fixed_vars as a dictionary mapping variables to their constant or symbolic values.
A list of Boolean equations (or strings) can be given in initial_equations which will be added as extra constraints to the funcional equation.
reduction_mode is the type of reduction (None, “gauss” or “groebner”) to apply before the SAT solver.
Before the SAT solver is called, fixed variables are searched in the equations. If only_linear_fixed_vars is True, only linear assignments are searched, that is, relations x{i} = f(x{i+1},..,xn) with f of degree up to 1.
find_linear_combinations_in_solutions determines whether to search for linear combinations among the solutions obtained from the SAT solver. The obtained linear combinations are used to simplify the system of equations and the list of fixed variables. If the number of obtained SAT solutions is less than the given num_sat_solutions, find_linear_combinations_in_solutions is automatically enabled.
If return_total_num_solutions is True, append to the output the number of total solutions (taking into account the free variables).
If ignore_initial_parsing is True, then initial_fixed_vars is not used to replace variables in the list of ANF or in the list of initial equations (in the first pass), and other checks regarding the BooleanPolynomialRing are ignored. The default value of ignore_initial_parsing (False) is recommended.
If check_find_fixed_vars is True, internal calls to find_fixed_vars are done with check=True (see find_fixed_vars).
A list of variables (strings or Boolean variables) can be given in ignore_varnames, which won’t be included in the solutions and will be set to 0 if they are free variables.
num_sols_per_base_sol_to_check determines the number of solutions per base solution that are checked, that is, that are given to the verification test F = G where F and G are substituted with the exact non-symbolic coefficients of the solution.
threads determines the number of threads for the SAT solver to use.
verbose and debug (True or False values) determine the amount of information printed to the output. if a string is given to filename, the output is printed to that file
>>> from boolcrypt.utilities import lut2anf, invert_lut >>> # example 1: finding the inverse of F0 by solving F1(F0) = Identity >>> f0 = lut2anf((0, 1, 2, 3, 4, 6, 7, 5)) >>> f1 = get_symbolic_anf(2, 3, 3) >>> g0 = lut2anf(list(range(2**3))) # identity >>> input_vars = ["x0", "x1", "x2", "x3"] >>> list_anfs = solve_functional_equation([f0, f1], [g0], [input_vars, input_vars], [input_vars], ... num_sat_solutions=1, return_mode="list_anfs", verbose=True) solving the functional equation F1(F0) = G0 - F1: [ x0*x1 x0*x2 x1*x2| x0 x1 x2| 1] [--------------------+--------------------+------] [a0_0_1 a0_0_2 a0_1_2| a0_0 a0_1 a0_2| a0] [a1_0_1 a1_0_2 a1_1_2| a1_0 a1_1 a1_2| a1] [a2_0_1 a2_0_2 a2_1_2| a2_0 a2_1 a2_2| a2] - F0: [x0*x2 x1*x2| x0 x1 x2] [-----------+-----------------] [ 1 1| 1 0 0] [ 1 0| 0 1 0] [ 0 0| 0 0 1] - G0: [x0 x1 x2] [--------] [ 1 0 0] [ 0 1 0] [ 0 0 1] number of input variables: 4 number of symbolic coefficients: 21 ... | computing F and G ... | getting equations from F + G = 0 ... | finding fixed and free variables and reducing system reducing 21 equations with mode gauss and degrees (d,#) Counter({1: 21}) gauss-reduction obtained 21 equations with degrees (d,#) Counter({1: 21}) found 21 fixed variables, resulting in 0 equations > repeating find_fixed_vars with initial reduction_mode gauss > last find_fixed_vars call found 0 new fixed variables and removed 0 equations fixed variables (21): [('a2', 0), ('a2_2', 1), ('a2_1', 0), ('a2_0', 0), ('a2_1_2', 0), ('a2_0_2', 0), ('a2_0_1', 0), ('a1', 0), ('a1_2', 0), ('a1_1', 1), ('a1_0', 0), ('a1_1_2', 1), ('a1_0_2', 1), ('a1_0_1', 0), ('a0', 0), ('a0_2', 0), ('a0_1', 0), ('a0_0', 1), ('a0_1_2', 1), ('a0_0_2', 0), ('a0_0_1', 0)] free variables (0): [] ... | ignoring SAT solving step total number of solutions: 1 ... | returning outputs with mode='list_anfs' >>> get_anf_coeffmatrix_str(list_anfs[0][0][1], input_vars=input_vars) # f1 [x0*x2 x1*x2| x0 x1 x2] [-----------+-----------------] [ 0 1| 1 0 0] [ 1 1| 0 1 0] [ 0 0| 0 0 1] >>> # same example, but now f1 is given and f0 is symbolic >>> f0 = get_symbolic_anf(2, 3, 3) >>> f1 = lut2anf(invert_lut([0, 1, 2, 3, 4, 6, 7, 5])) >>> list_anfs = solve_functional_equation([f0, f1], [g0], [input_vars, input_vars], [input_vars], ... num_sat_solutions=1, return_mode="list_anfs") >>> get_anf_coeffmatrix_str(list_anfs[0][0][0], input_vars=input_vars) # f0 [x0*x2 x1*x2| x0 x1 x2] [-----------+-----------------] [ 1 1| 1 0 0] [ 1 0| 0 1 0] [ 0 0| 0 0 1] >>> # example 2: finding a 2-bit linear permutation F0 by solving [(y,x), F0] = [1, 1] >>> # with the extra condition a0_0 + 0 >>> f0 = get_symbolic_anf(1, 2, 2, ct_terms=False) >>> f1 = lut2anf([0, 2, 1, 3]) # (x, y) to (y, x) >>> input_vars = ["x0", "x1"] >>> init_eq = ["a0_0", anf2matrix(f0, input_vars).determinant() + 1] >>> result = solve_functional_equation([f0, f1], [1, 1], [input_vars, input_vars], None, ... num_sat_solutions=None, return_mode="symbolic_anf", initial_equations=init_eq, reduction_mode=None, ... verbose=True, debug=True) solving the functional equation F1(F0) = degrees([1, 1]) - F1: [x0 x1] [-----] [ 0 1] [ 1 0] - F0: [ x0 x1] [---------] [a0_0 a0_1] [a1_0 a1_1] input variables (2): ['x0', 'x1'] symbolic coefficients (4): ['a0_0', 'a0_1', 'a1_0', 'a1_1'] Boolean PolynomialRing in x0, x1, a0_0, a0_1, a1_0, a1_1 initial equations (2): a0_0 a0_0*a1_1 + a0_1*a1_0 + 1 ... | computing F and G - F (after composition): [ x0 x1] [---------] [a1_0 a1_1] [a0_0 a0_1] ... | getting equations from F + G = 0 no equation added from F + G = 0 ... | finding fixed and free variables finding fixed variables in 2 equations with degrees (d, #) Counter({1: 1, 2: 1}) in Boolean PolynomialRing in x0, x1, a0_0, a0_1, a1_0, a1_1 with term order Lexicographic term order eqs[1] = a0_0*a1_1 + a0_1*a1_0 + 1 eqs[0] = a0_0 found fixed variable a0_0 <- 0 prev_eqs[0] <-- a0_1*a1_0 + 1 found 1 fixed variables, resulting in 1 equations with degrees (d, #) Counter({2: 1}) fixed variables (1): [('a0_0', 0)] free variables (1): [a1_1] ... | solving 1 equations with 2 variables using SAT solver solver options: num_sat_solutions=+Infinity, threads=1 system variables: [a1_0, a0_1] ... | parsing 1 SAT solutions found (total number of solutions 2 = 2^{1}) SAT solutions: {a0_1: 1, a1_0: 1} Base solution 1 out of 1, checking full solution 1 out of 1: - sat solution : {a0_1: 1, a1_0: 1} - sat solution + fixed vars : OrderedDict([(a0_1, 1), (a1_0, 1), (a0_0, 0)]) - sat solution + fixed vars + free vars : {a0_1: 1, a1_0: 1, a0_0: 0, a1_1: 0} - F: [x0 x1] [-----] [ 1 0] [ 0 1] ... | finding linear combinations of variables among the SAT solutions linear combinations (2): ['a1_0 + 1', 'a0_1 + 1'] linear combinations (matrix form) [a1_0 a0_1 1] [--------------] [ 1 0 1] [ 0 1 1] ... | reducing system with the linear combinations obtained finding fixed variables in 3 equations with degrees (d, #) Counter({1: 2, 2: 1}) in Boolean PolynomialRing in x0, x1, a0_0, a0_1, a1_0, a1_1 with term order Lexicographic term order eqs[2] = a0_1 + 1 found fixed variable a0_1 <- 1 eqs[1] = a1_0 + 1 found fixed variable a1_0 <- 1 found 2 fixed variables, resulting in 0 equations fixed variables (3): [('a0_0', 0), ('a0_1', 1), ('a1_0', 1)] number of system variables changed to 0 system variables (0): [] number of equations changed to 0 ... | returning outputs with mode='symbolic_anf' >>> get_anf_coeffmatrix_str(result[0][0][0], input_vars=input_vars) # f0 [ x0 x1] [---------] [ 0 1] [ 1 a1_1] >>> list(result[1]) # equations []
- boolcrypt.functionalequations.find_inverse(anf, inv_degree, inv_position='left', prefix_inv_coeffs='a', verbose=False, debug=False, filename=None, **solve_args)[source]
Find the inverse of an ANF by calling solve_functional_equation().
Given a function F, find A s.t. A(F) = Identity if inv_position=”left”. If inv_position=”right”, find A’ s.t. F(A) = Identity. If no inverse is found, None returned.
This method does not support symbolic ANF, and the input function F must be defined in the boolean polynomial ring BooleanPolynomialRing(n,’x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and the ANF of the inverse is returned.>>> sage.all.set_random_seed(0) >>> from boolcrypt.utilities import lut2anf, matrix2anf, compose_anf_fast >>> anf = lut2anf((0, 1, 2, 3, 4, 6, 7, 5)) >>> inv_anf = find_inverse(anf, 2) >>> get_anf_coeffmatrix_str(inv_anf) # , input_vars=["x0", "x1", "x2"]) [x0*x2 x1*x2| x0 x1 x2] [-----------+-----------------] [ 0 1| 1 0 0] [ 1 1| 0 1 0] [ 0 0| 0 0 1] >>> get_anf_coeffmatrix_str(compose_anf_fast(inv_anf, anf), input_vars=["x0", "x1", "x2"]) [x0 x1 x2] [--------] [ 1 0 0] [ 0 1 0] [ 0 0 1] >>> matrix = sage.all.matrix(GF(2), 2, 3, [[1, 1, 0], [1, 1, 1]]) >>> anf = matrix2anf(matrix) >>> result = find_inverse(anf, 1, inv_position="right", return_mode="symbolic_anf", num_sat_solutions=None) >>> get_anf_coeffmatrix_str(result[0][0][0], input_vars=["x0", "x1", "x2"]) [ x0 x1 x2| 1] [--------------------------+--------] [a1_0 + 1 a1_1 a1_2| a1] [ a1_0 a1_1 a1_2| a1] [ 1 1 0| 0] >>> list(result[1]) # equations [] >>> matrix * anf2matrix(result[0][0][0], input_vars=["x0", "x1", "x2"]) [1 0 0] [0 1 0]
- boolcrypt.functionalequations.find_equivalence(left_anf, right_anf, left_equiv_degree=1, right_equiv_degree=1, equiv_ct_terms=True, prefix_left_equiv_coeffs='b', prefix_right_equiv_coeffs='a', add_invertibility_equations=False, verbose=False, debug=False, filename=None, **solve_args)[source]
Find a pair of functions (A, B) such that B F A = G.
Given the left function F and the right function G, this method finds a pair of functions (A, B) of given degrees such that B F A = G. If no solution is found, None is returned.
If given degrees are 1 and equiv_ct_terms=True (resp. False), this methods finds whether F and G are affine (resp. linear) equivalent. Note that right_equiv_degree affects the right equivalence A and left_equiv_degree affects the left equivalence B.
If F and G are the same, this methods finds self-equivalences.
The pair (A, B) is found by solving the functional equation B F A = G.
The parameter add_invertibility_equations can be [False, “right”, “left”, “both”]. If “right” or “both”, an additional constraint is added to ensure the affine function B is a permutation (only supported with degree=1). If “left” or “both”, an additional constraint is added to ensure the affine function A is a permutation (only supported with degree=1). If False, no additional constraint is added regarding invertibility. Note that if F and G are permutations with the same input size, then no invertibility constraint is needed.
This method does not support symbolic ANF, and the input functions F and G must be defined in the boolean polynomial ring BooleanPolynomialRing(n, ‘x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and a pair containing the ANF of A and B is returned.>>> from boolcrypt.utilities import lut2anf, get_lut_inversion >>> from boolcrypt.equivalence import get_linear_repr >>> from boolcrypt.equivalence import check_self_le_anf >>> left_anf = lut2anf([0, 1, 2, 3, 4, 6, 7, 5]) >>> right_anf = lut2anf(get_linear_repr([0, 1, 2, 3, 4, 6, 7, 5])) >>> right_lin, left_lin = find_equivalence(left_anf, right_anf, equiv_ct_terms=False) # linear >>> get_anf_coeffmatrix_str(right_lin, input_vars=["x0", "x1", "x2"]) [x0 x1 x2] [--------] [ 0 1 0] [ 1 1 1] [ 0 0 1] >>> right_anf = lut2anf([x.__xor__(1) for x in [0, 1, 2, 3, 4, 6, 7, 5]]) >>> find_equivalence(left_anf, right_anf, equiv_ct_terms=False) No solution found (found invalid equation 0 == 1) >>> right_aff, left_aff = find_equivalence(left_anf, right_anf, equiv_ct_terms=True) # affine >>> get_anf_coeffmatrix_str(right_aff, input_vars=["x0", "x1", "x2"]) [x0 x1 x2| 1] [--------+--] [ 0 1 0| 0] [ 1 0 0| 0] [ 0 0 1| 1] >>> find_equivalence(left_anf, lut2anf(get_lut_inversion(3))) No solution found (system of equations is inconsistent (unsatisfiable)) >>> right_se, left_se = find_equivalence(left_anf, left_anf, 1, 1, equiv_ct_terms=False) # linear SE >>> assert check_self_le_anf(left_anf, right_se, left_se, None) >>> right_se, left_se = find_equivalence(left_anf, left_anf, 2, 2, equiv_ct_terms=False) # non-linear SE >>> assert check_self_le_anf(left_anf, right_se, left_se, None) >>> get_anf_coeffmatrix_str(right_se, input_vars=["x0", "x1", "x2"]) [x0*x1 x0*x2 x1*x2| x0 x1 x2] [-----------------+-----------------] [ 0 0 0| 0 1 1] [ 1 1 1| 0 1 1] [ 0 0 0| 1 0 1]
- boolcrypt.functionalequations.find_half_affine_equivalence(left_anf, inv_right_anf, prefix_equiv_coeffs='a', add_invertibility_equations=True, verbose=False, debug=False, filename=None, **solve_args)[source]
Find an affine permutation A such that F A G^{-1} is affine.
Given the left permutation F and the right permutation G^{-1}, this method finds an affine permutation A such that F A G^{-1} is affine Note that this is equivalent to the existence of B such that B F A = G. In particular, if F = G, A is a right affine self-equivalence of F. If no solution is found, None is returned.
If add_invertibility_equations is True, an additional constraint is added to ensure A is invertible (not needed if F and G are permutations with the same input size).
This method does not support symbolic ANF, and the input functions F and G must be defined in the boolean polynomial ring BooleanPolynomialRing(n, ‘x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and the ANF of A is returned.>>> sage.all.set_random_seed(0) >>> from boolcrypt.utilities import lut2anf, invert_lut >>> from boolcrypt.equivalence import check_self_ae_anf >>> anf = lut2anf((0, 1, 2, 3, 4, 6, 7, 5)) >>> inv_anf = lut2anf(invert_lut([x.__xor__(1) for x in [0, 1, 2, 3, 4, 6, 7, 5]])) >>> right_se = find_half_affine_equivalence(anf, inv_anf) setting to 0 the free variables [a0_2, a0, a1_2, a1, a2] >>> get_anf_coeffmatrix_str(right_se, input_vars=["x0", "x1", "x2"]) [x0 x1 x2] [--------] [ 1 1 0] [ 1 0 0] [ 0 0 1] >>> inv_anf = lut2anf(invert_lut((0, 1, 2, 3, 4, 6, 7, 5))) >>> right_se = find_half_affine_equivalence(anf, inv_anf) setting to 0 the free variables [a0_2, a0, a1_2, a1, a2] >>> assert check_self_ae_anf(anf, right_se, None, inv_anf) >>> get_anf_coeffmatrix_str(right_se, input_vars=["x0", "x1", "x2"]) [x0 x1 x2] [--------] [ 1 1 0] [ 1 0 0] [ 0 0 1]
- boolcrypt.functionalequations.find_nondiagonal_ase(left_anf, right_anf, se_ct_terms=True, prefix_se_left_coeffs='b', prefix_se_right_coeffs='a', verbose=False, debug=False, filename=None, **solve_args)[source]
Find an affine non-diagonal self-equivalence of F || G.
Given the function F by left_anf and G by right_anf, finds an affine self-equivalence (A, B) of the concatenation F || G, where A is non-diagonal (A in matrix form is not a block diagonal matrix up to block row permutations). If no solution is found, None is returned.
If se_ct_terms=False, the constant terms of A and B are set to zero.
This method does not support symbolic ANF, and the input functions F and G must be defined in the boolean polynomial ring BooleanPolynomialRing(n, ‘x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and a pair with the ANF of A and B is returned.>>> sage.all.set_random_seed(0) >>> from boolcrypt.utilities import lut2anf, invert_lut, get_lut_inversion >>> from boolcrypt.equivalence import check_self_le_anf >>> left_anf = lut2anf([0, 1, 2, 3, 4, 5, 7, 6]) >>> right_anf = left_anf >>> right_se, left_se = find_nondiagonal_ase(left_anf, right_anf, se_ct_terms=False) >>> concat_anf = concatenate_anf(left_anf, right_anf) >>> assert check_self_le_anf(concat_anf, right_se, left_se, None) >>> get_anf_coeffmatrix_str(right_se, input_vars=["x" + str(i) for i in range(6)]) [x0 x1 x2 x3 x4 x5] [-----------------] [ 1 0 1 0 1 0] [ 0 1 0 0 0 0] [ 0 1 1 0 0 0] [ 0 0 0 1 0 0] [ 0 0 0 0 0 1] [ 0 0 0 0 1 0] >>> left_anf = lut2anf(get_lut_inversion(3)) >>> right_anf = left_anf >>> find_nondiagonal_ase(left_anf, right_anf, se_ct_terms=False) No solution found (system of equations is inconsistent (unsatisfiable))
- boolcrypt.functionalequations.find_noninvertible_ase(anf, se_ct_terms=True, prefix_left_se_coeffs='b', prefix_right_se_coeffs='a', verbose=False, debug=False, filename=None, **solve_args)[source]
Find a non-invertible pair (A, B) such that F A = B F.
An affine non-invertible self-equivalence of F is a pair of non-invertible affine functions (A, B) such that B F = F A. A is also called a right SE and B a left SE. If no solution is found, None is returned.
If se_ct_terms=False, the constant terms of A and B are set to zero.
This method does not support symbolic ANF, and the input function F must be defined in the boolean polynomial ring BooleanPolynomialRing(n,’x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and a pair containing the ANF of A and B is returned.>>> from boolcrypt.utilities import lut2anf, get_lut_inversion >>> anf = lut2anf([0, 1, 2, 3, 4, 5, 7, 6]) >>> right_se, left_se = find_noninvertible_ase(anf) setting to 0 the free variables [b0, b1, b2] >>> get_anf_coeffmatrix_str(right_se, input_vars=["x0", "x1", "x2"]) [x1] [--] [ 0] [ 0] [ 1] >>> get_anf_coeffmatrix_str(left_se, input_vars=["x0", "x1", "x2"]) [x1] [--] [ 0] [ 0] [ 1] >>> find_noninvertible_ase(lut2anf(get_lut_inversion(3))) No solution found (system of equations is inconsistent (unsatisfiable))
- boolcrypt.functionalequations.find_horizontal_decomposition(anf, degree_anf, num_inputs_first_factor, aff_ct_terms=True, prefix_left_aff_coeffs='b', prefix_right_aff_coeffs='a', prefix_first_factor='p', prefix_second_factor='q', verbose=False, debug=False, filename=None, **solve_args)[source]
Find an horizontal decomposition P(x’)|Q(x’’) of G(x) in the affine class.
An horizontal decomposition of G(x) is a pair of functions P(x’), Q(x’’), such that x = x’ || x’’ and (P,Q) and G are affine equivalent (linear equivalent if aff_ct_terms=False), that is, B (P, Q) A = G. P and Q are called the first and the second factor, respectively. If no solution is found, None is returned.
The triple ((P, Q), A, B) is found by solving B (P, Q) A = G.
If aff_ct_terms=False, finds A and B linear instead of affine.
This method does not support symbolic ANF, and the input function G must be defined in the boolean polynomial ring BooleanPolynomialRing(n,’x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found abd the triple ((P, Q), A, B), each one in ANF form, is returned.>>> sage.all.set_random_seed(0) >>> from boolcrypt.utilities import lut2anf, get_lut_inversion >>> anf = lut2anf([1, 0, 3, 2, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]) # 2nd to last 4b aff class >>> decomp, right_aff, left_aff = find_horizontal_decomposition(anf, 2, 1) setting to 0 the free variables [a0, p0, q0, q1, q2] >>> get_anf_coeffmatrix_str(decomp, input_vars=["x0", "x1", "x2", "x3"]) [x2*x3| x0 x1 x2 x3] [-----+-----------------------] [ 0| 1 0 0 0] [ 0| 0 0 1 0] [ 0| 0 0 0 1] [ 1| 0 1 1 1] >>> get_anf_coeffmatrix_str(right_aff, input_vars=["x0", "x1", "x2", "x3"]) [x0 x1 x2 x3] [-----------] [ 0 1 0 0] [ 1 0 0 0] [ 0 0 1 0] [ 0 0 0 1] >>> get_anf_coeffmatrix_str(left_aff, input_vars=["x0", "x1", "x2", "x3"]) [x0 x1 x2 x3| 1] [-----------+--] [ 0 0 0 1| 1] [ 1 0 0 0| 0] [ 0 1 0 0| 0] [ 0 0 1 0| 0] >>> anf = lut2anf((0, 1, 2, 3, 4, 6, 7, 5)) >>> find_horizontal_decomposition(anf, 2, 1) # non-linear 3b cannot be decomposed No solution found (system of equations is inconsistent (unsatisfiable))
- boolcrypt.functionalequations.find_ccz_equivalence(left_anf, right_anf, equiv_degree=1, equiv_ct_terms=True, add_invertibility_equations=True, prefix_am_coeffs='a', verbose=False, debug=False, filename=None, **solve_args)[source]
Find an affine A such that A(graph F) = graph G.
Given the left function F and the right function G, this method finds an invertible admissible mapping A of given degree such that the graph of G is equal to the graph of F transformed by A. If no solution is found, None is returned.
Graph(f) is is the set of points {(x, F(x))}, and similar for Graph(G).
If the given degree is 1 and equiv_ct_terms=True (resp. False), this method finds an affine (resp. linear) admissible mapping.
If F and G are the same, this methods finds Graph(F) self-equivalences/automorphisms, that is, invertibles A such that A(graph F) = graph F.
A = (a_0, a_1) is returned by solving the functional equation G(a_0(u, F(u))) = a_1(u, F(u)).
If add_invertibility_equations=True, the equations that impose A to be invertible are added to the system of equations (only supported for equiv_degree=1).
This method does not support symbolic ANF, and the input functions F and G must be defined in the boolean polynomial ring BooleanPolynomialRing(n, ‘x’) with n the number of input variables.
Named arguments from
**solve_argsare passed to solve_functional_equation(). By default, return_mode=”list_anfs” and num_sat_solutions=”1”. If these two parameters are not given, only one solution is found and the ANF of A is returned.>>> sage.all.set_random_seed(0) >>> from boolcrypt.utilities import get_lut_inversion, lut2anf >>> left_anf = lut2anf((0, 1, 2, 3, 4, 6, 7, 5)) >>> am = find_ccz_equivalence(left_anf, left_anf, only_linear_fixed_vars=True, equiv_ct_terms=False) >>> get_anf_coeffmatrix_str(am, input_vars=["x" + str(i) for i in range(3*2)]) # Graph-SE [x0 x1 x2 x3 x4 x5] [-----------------] [ 0 0 0 0 1 0] [ 1 0 0 0 0 0] [ 0 0 0 0 0 1] [ 1 1 0 1 0 0] [ 0 0 1 1 0 1] [ 0 0 1 0 0 0] >>> find_ccz_equivalence(left_anf, lut2anf(get_lut_inversion(3)), only_linear_fixed_vars=True) No solution found (system of equations is inconsistent (unsatisfiable)) >>> # CCZ of inversion found with sboxU.ccz_equivalent_permutations >>> left_anf = lut2anf([0, 15, 9, 7, 4, 14, 1, 3, 10, 6, 13, 2, 8, 5, 11, 12]) >>> right_anf = lut2anf(get_lut_inversion(4)) >>> # next call might require to increase Python's recursionlimit >>> am = find_ccz_equivalence(left_anf, right_anf, equiv_ct_terms=False, ... only_linear_fixed_vars=True, verbose=True) >>> get_anf_coeffmatrix_str(am, input_vars=["x" + str(i) for i in range(4*2)]) [x0 x1 x2 x3 x4 x5 x6 x7] [-----------------------] [ 0 1 0 1 0 0 0 0] [ 0 0 1 1 0 0 0 0] [ 1 1 1 1 0 0 0 0] [ 1 1 0 1 0 0 0 0] [ 0 1 1 1 1 1 0 0] [ 0 1 0 1 1 1 1 0] [ 0 0 0 0 1 0 1 0] [ 0 0 1 0 1 0 1 1]