Utils

General

Direct building of CNFs representing boolean equalities

Building a CNF representing a generic boolean equality can be time consuming. This module offers functions to directly build the CNF of basic boolean equalities. It also offers function to directly build CNFs for the Lipmaa-Moriai algorithm which is a cornerstone when searching XOR differential trails.

Every function returns a list of strings representing clauses whose satisfiability is equivalent to the equality they represent.

Running SAT solver

Sat Model allows to use many SAT solvers like CryptoMiniSat, Glucose, Minisat and others. Unfortunately, some of them do not take input from stdin and need an input file. Functions of this section supply the best running method for SAT solvers in Sat Model.

cms_add_clauses_to_solver(numerical_cnf, solver)

Add clauses to the (internal) SAT solver.

It needs to be overwritten in this class because it must handle the XOR clauses.

cnf_and(result, variables)

Return a list of strings.

Representing the CNF of the Boolean equality result = And(variable_0, variable_1, ..., variable_{n-1}).

INPUT:

• result – string; the variable for the result

• variables – list; the list of variables which are operands

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_and
sage: cnf_and('r', ['a', 'b', 'c'])
['-r a', '-r b', '-r c', 'r -a -b -c']

cnf_and_differential(diff_in_0, diff_in_1, diff_out, hw)

Return a tuple of strings representing the CNF of the probability of the differential relation.

INPUT:

• diff_in_0 – string; the difference for the bit of the first input

• diff_in_1 – string; the difference for the bit of the second input

• diff_out – string; the difference for the bit of the output

• hw – string; the bit for the hamming weight

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_and_differential
sage: cnf_and_differential('and_0', 'and_1', 'and_out', 'hw')
('-and_out hw', 'and_0 and_1 -hw', '-and_0 hw', '-and_1 hw')

cnf_and_linear(mask_in_0, mask_in_1, mask_out, hw)

Return a tuple of strings representing the CNF of the probability of the linear relation.

(mask_in_0 & in_0) ^ (mask_in_1 & in_1) = (mask_out & out), being out = in_0 & in_1.

INPUT:

• mask_in_0 – string; the mask for the bit of the first input

• mask_in_1 – string; the mask for the bit of the second input

• mask_out – string; the mask for the bit of the output

• hw – string; the bit for the hamming weight

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_and_linear
sage: cnf_and_linear('and_0', 'and_1', 'and_out', 'hw')
('-and_0 hw', '-and_1 hw', '-and_out hw', 'and_out -hw')

cnf_and_seq(out_ids, in_ids)

cnf_carry(carry, x, y, previous_carry)

Return a tuple of strings.

Representing the CNF of the Boolean equality carry = Or(And(x, y), And(x, previous_carry), And(y, previous_carry)). It represents the general form of a carry when performing modular addition between two bitvectors.

INPUT:

• carry – string; the carry to be comuted (current carry)

• x – string; the bit of the first addendum

• y – string; the bit of the second addendum

• previous_carry – string; the previous carry

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_carry
sage: cnf_carry('c_3', 'x_3', 'y_3', 'c_2')
('x_3 y_3 -c_3',
 '-x_3 -y_3 c_3',
 'x_3 c_2 -c_3',
 '-x_3 -c_2 c_3',
 'y_3 c_2 -c_3',
 '-y_3 -c_2 c_3')

cnf_carry_comp2(carry, x, previous_carry)

Return a tuple of strings.

Representing the CNF of the Boolean equality carry = And(Not(x), previous_carry). It represents the general form of a carry when performing modular addition between the notwise of a vector and 1.

INPUT:

• carry – string; the carry to be comuted (current carry)

• x – string; the bit of the input addendum

• previous_carry – string; the previous carry

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_carry_comp2
sage: cnf_carry_comp2('c_3', 'x_2', 'c_2')
('-c_3 c_2', '-c_3 -x_2', 'c_3 -c_2 x_2')

cnf_equivalent(variables)

Return a list of strings.

Representing the CNF of the equivalence of Boolean variables variable_0 = variable_1 = ... = variable_2.

INPUT:

• variables – list; the variables that must be equivalent

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_equivalent
sage: cnf_equivalent(['a', 'b'])
['a -b', 'b -a']

cnf_hw_lipmaa(hw, alpha, beta, gamma)

Return a tuple of strings representing the CNF of the Boolean equality.

Not(hw_i) = And(Xor(Not(alpha_{i+1}), beta_{i+1}), Xor(Not(alpha_{i+1}), gamma_{i+1})) (Lipmaa-Moriai algorithm).

INPUT:

• hw – string; the variable for the Hamming weight

• alpha – string; the bit in the first mask

• beta – string; the bit in the second mask

• gamma – string; the bit in the result mask

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_hw_lipmaa
sage: cnf_hw_lipmaa('hw_6', 'alpha_7', 'beta_7', 'gamma_7')
('alpha_7 -gamma_7 hw_6',
 'beta_7 -alpha_7 hw_6',
 'gamma_7 -beta_7 hw_6',
 'alpha_7 beta_7 gamma_7 -hw_6',
 '-alpha_7 -beta_7 -gamma_7 -hw_6')

cnf_inequality(left_var, right_var)

Return a list of strings representing the CNF of the Boolean equality left_var = Not(right_var).

INPUT:

• left_var – string; the left side variable

• right_var – string; the right side variable

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_inequality
sage: cnf_inequality('a', 'b')
('a b', '-a -b')

cnf_lipmaa(hw, dummy, beta_1, alpha, beta, gamma)

Return a tuple of strings representing the CNF of the Boolean equalities.

And(Not(hw_i), Xor(dummy_i, beta_{i-1})) = 0 and dummy_i = Xor(alpha_i, beta_i, gamma_i) (Lipmaa-Moriai algorithm).

INPUT:

• hw – string; the variable for the Hamming weight bit

• dummy – string; the variable for the XOR of the three masks

• beta_1 – string; the next bit in the second mask

• alpha – string; the bit in the first mask

• beta – string; the bit in the second mask

• gamma – string; the bit in the result mask

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_lipmaa
sage: cnf_lipmaa('hw_10', 'dummy_10', 'beta_11', 'alpha_10', 'beta_10', 'gamma_10')
('beta_11 -dummy_10 hw_10',
 '-beta_11 dummy_10 hw_10',
 'alpha_10 beta_10 dummy_10 -gamma_10',
 'alpha_10 beta_10 -dummy_10 gamma_10',
 'alpha_10 -beta_10 dummy_10 gamma_10',
 '-alpha_10 beta_10 dummy_10 gamma_10',
 'alpha_10 -beta_10 -dummy_10 -gamma_10',
 '-alpha_10 beta_10 -dummy_10 -gamma_10',
 '-alpha_10 -beta_10 dummy_10 -gamma_10',
 '-alpha_10 -beta_10 -dummy_10 gamma_10')

cnf_modadd_inequality(z, u, v)

Return a tuple of strings representing the CNF of the Boolean inequality z >= Xor(u, v).

It is needed for the XOR linear constraints of modular addition (see formula (1) in Automatic Search of Linear Trails in ARX with Applications to SPECK and Chaskey.

INPUT:

• z – string; the bit of the hamming weight

• u – string; the bit of the result

• v – string; the bit of an addendum

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_modadd_inequality
sage: cnf_modadd_inequality('z', 'u', 'v')
('z u -v', 'z -u v')

cnf_n_window_heuristic_on_w_vars(hw_bit_ids)

cnf_or(result, variables)

Return a list of strings.

Representing the CNF of the Boolean equality result = Or(variable_0, variable_1, ..., variable_{n-1}).

INPUT:

• result – string; the variable for the result

• variables – list; the list of variables which are operands

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_or
sage: cnf_or('r', ['a', 'b', 'c'])
['r -a', 'r -b', 'r -c', '-r a b c']

cnf_or_seq(out_ids, in_ids)

cnf_result_comp2(result, x, carry)

Return a tuple of strings representing the CNF of the Boolean equality result = Xor(Not(x), carry).

It represents the general form of a result when performing modular addition between the notwise of a vector and 1.

INPUT:

• result – string; the result to be comuted

• x – string; the bit of the input addendum

• carry – string; the carry

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_result_comp2
sage: cnf_result_comp2('r_3', 'x_3', 'c_3')
('c_3 -r_3 -x_3', '-c_3 r_3 -x_3', '-c_3 -r_3 x_3', 'c_3 r_3 x_3')

cnf_vshift_false(out_id, in_id, shift_id)

Return a tuple of strings.

Representing the CNF of the Boolean branch when shifting by variable amount and having to decide between a bit and false.

INPUT:

• out_id – string; the bit of the new state

• in_id – string; the bit to be assigned to out_id if not shifted

• shift_id – string; the bit determining the shift

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_vshift_false
sage: cnf_vshift_false('s_1', 'i_1', 'k_7')
('-s_1 i_1', '-s_1 -k_7', 's_1 -i_1 k_7')

cnf_vshift_id(out_id, in_id, in_shifted, shift_id)

Return a tuple of strings.

Representing the CNF of the Boolean branch when shifting by variable amount and having to decide between two bits.

INPUT:

• out_id – string; the bit of the new state

• in_id – string; the bit to be assigned to out_id if not shifted

• in_shifted – string; the bit to be assigned to out_id if shifted

• shift_id – string; the bit determining the shift

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_vshift_id
sage: cnf_vshift_id('s_3', 'i_3', 'i_4', 'k_7')
('-s_3 i_3 k_7', 's_3 -i_3 k_7', '-s_3 i_4 -k_7', 's_3 -i_4 -k_7')

cnf_xor(result, variables)

Return a list of strings.

Representing the CNF of the Boolean equality result = Xor(variable_0, variable_1, ..., variable_{n-1}).

INPUT:

• result – string; the variable for the result

• variables – list; the variables

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_xor
sage: cnf_xor('r', ['a', 'b', 'c'])
['-r a b c',
 'r -a b c',
 'r a -b c',
 'r a b -c',
 '-r -a -b c',
 '-r -a b -c',
 '-r a -b -c',
 'r -a -b -c']

cnf_xor_seq(results, variables)

Return a list of strings.

Representing the CNF of the Boolean equality result = Xor(variable_0, variable_1, ..., variables_n) with n at least 3. Note that results[:-1] are intermediate results and results[-1] must be the string identifying the whole result.

INPUT:

• results – list; the results

• variables – list; the variables

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_xor_seq
sage: cnf_xor_seq(['i_0', 'i_1', 'r_7'], ['a_7', 'b_7', 'c_7', 'd_7'])
['-i_0 a_7 b_7',
 'i_0 -a_7 b_7',
 'i_0 a_7 -b_7',
 ...
 'r_7 -i_1 d_7',
 'r_7 i_1 -d_7',
 '-r_7 -i_1 -d_7']

cnf_xor_truncated(result, variable_0, variable_1)

Return a list of strings representing the CNF of the Boolean XOR when searching for DETERMINISTIC TRUNCATED XOR DIFFERENTIAL. I.e., an XOR behaving as in the following table:

variable_0	variable_1	result
0	0	0
0	1	1
0	2	2
1	0	1
1	1	0
1	2	2
2	0	2
2	1	2
2	2	2

INPUT:

• result – tuple of two strings; the result variable

• variable_0 – tuple of two string; the first variable

• variable_1 – tuple of two string; the second variable

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_xor_truncated
sage: cnf_xor_truncated(('r0', 'r1'), ('a0', 'a1'), ('b0', 'b1'))
['r0 -a0',
 'r0 -b0',
 'a0 b0 -r0',
 'a1 b1 r0 -r1',
 'a1 r0 r1 -b1',
 'b1 r0 r1 -a1',
 'r0 -a1 -b1 -r1']

cnf_xor_truncated_seq(results, variables)

Return a list of strings representing the CNF of the Boolean XOR performed between more than 2 inputs when searching for DETERMINISTIC TRUNCATED XOR DIFFERENTIAL.

See also

cnf_xor_truncated()

INPUT:

• results – list; intermediate results + final result

• variables – list; the variables

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.utils import cnf_xor_truncated_seq
sage: cnf_xor_truncated_seq([('i0', 'i1'), ('r0', 'r1')], [('a0', 'a1'), ('b0', 'b1'), ('c0', 'c1')])
['i0 -a0',
 'i0 -b0',
 'a0 b0 -i0',
 ...
 'i1 r0 r1 -c1',
 'c1 r0 r1 -i1',
 'r0 -i1 -c1 -r1']

create_numerical_cnf(cnf)

get_cnf_bitwise_truncate_constraints(a, a_0, a_1)

get_cnf_semi_deterministic_window_1(A_t0, A_t1, A_t2, A_v0, A_v1, A_v2, B_t0, B_t1, B_t2, B_v0, B_v1, B_v2, C_t0, C_t1, C_t2, C_v0, C_v1, p0, q0, r0)

get_cnf_semi_deterministic_window_2(A_t0, A_t1, A_t2, A_t3, A_v0, A_v1, A_v2, A_v3, B_t0, B_t1, B_t2, B_t3, B_v0, B_v1, B_v2, B_v3, C_t0, C_t1, C_t2, C_t3, C_v0, C_v1, p0, q0, r0)

get_cnf_semi_deterministic_window_3(A_t0, A_t1, A_t2, A_t3, A_t4, A_v0, A_v1, A_v2, A_v3, A_v4, B_t0, B_t1, B_t2, B_t3, B_t4, B_v0, B_v1, B_v2, B_v3, B_v4, C_t0, C_t1, C_t2, C_t3, C_t4, C_v0, C_v1, p0, q0, r0)

get_cnf_truncated_linear_constraints(a, a_0)

get_semi_deterministic_cnf_window_0(A_t0, A_t1, A_v0, A_v1, B_t0, B_t1, B_v0, B_v1, C_t0, C_t1, C_v0, C_v1, p0, q0, r0)

modadd_truncated(result, variable_0, variable_1, carry, next_carry)

modadd_truncated_lsb(result, variable_0, variable_1, next_carry)

modadd_truncated_msb(result, variable_0, variable_1, carry)

numerical_cnf_to_dimacs(number_of_variables, numerical_cnf)

run_minisat(solver_specs, options, dimacs_input, input_file_name, output_file_name)

Call the MiniSat solver specified in solver_specs, using input and output files.

run_parkissat(solver_specs, options, dimacs_input, input_file_name)

Call the Parkissat solver specified in solver_specs, using input and output files.

run_sat_solver(solver_specs, options, dimacs_input, host=None, env_vars_string='')

Call the SAT solver specified in solver_specs, using input and output pipes.

run_yices(solver_specs, options, dimacs_input, input_file_name)

Call the Yices SAT solver specified in solver_specs, using input file.