Skip to content

Commit

Permalink
FEATURE/Feature: add SAT deterministic truncated trail search
Browse files Browse the repository at this point in the history 
The SAT constraints for deterministic truncated XOR differential trail
search have been added.
  • Loading branch information
@ale-depi
ale-depi committed Dec 13, 2023
1 parent 1f816ba commit 5db90d7
Show file tree
Hide file tree
Showing 3 changed files with 67 additions and 20 deletions.
4 changes: 2 additions & 2 deletions claasp/cipher_modules/models/sat/sat_model.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ def _get_cipher_inputs_components_solutions_double_ids(self, variable2value):
if f'{cipher_input}_{i}_1' in variable2value:
value ^= variable2value[f'{cipher_input}_{i}_1']
values.append(f'{value}')
component_solution = set_component_solution(''.join(values))
component_solution = set_component_solution(''.join(values).replace('2', '?'))
components_solutions[cipher_input] = component_solution

return components_solutions
Expand All @@ -191,7 +191,7 @@ def _get_component_value_double_ids(self, component, variable2value):
if f'{component.id}_{i}_1' in variable2value:
variable_value ^= variable2value[f'{component.id}_{i}_1']
values.append(f'{variable_value}')
value = ''.join(values)
value = ''.join(values).replace('2', '?')

return value

Expand Down
46 changes: 46 additions & 0 deletions claasp/cipher_modules/models/sat/utils/utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -653,6 +653,52 @@ def cnf_xor_truncated_seq(results, variables):
return model


def modadd_truncated_lsb(result, variable_0, variable_1, next_carry):
return [f'{variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{next_carry[0]}',
f'{variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{next_carry[1]}',
f'{variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[0]}',
f'{variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[1]}',
f'{next_carry[0]} {variable_0[0]} {variable_0[1]} {variable_1[0]} -{variable_1[1]}',
f'{variable_0[0]} {variable_0[1]} {variable_1[0]} {result[1]} -{variable_1[1]}',
f'{variable_0[0]} {variable_0[1]} {variable_1[0]} -{variable_1[1]} -{result[0]}',
f'{next_carry[0]} {variable_0[0]} {variable_1[0]} {variable_1[1]} -{variable_0[1]}',
f'{variable_0[0]} {variable_1[0]} {variable_1[1]} {result[1]} -{variable_0[1]}',
f'{variable_0[0]} {variable_1[0]} {variable_1[1]} -{variable_0[1]} -{result[0]}',
f'{next_carry[0]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]}',
f'{variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[0]}',
f'{variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}']


def modadd_truncated(result, variable_0, variable_1, carry, next_carry):
return [f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{next_carry[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{next_carry[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[1]}',
f'{carry[0]} {carry[1]} {next_carry[0]} {variable_0[0]} {variable_0[1]} {variable_1[0]} -{variable_1[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {result[1]} -{variable_1[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} -{variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {next_carry[0]} {variable_0[0]} {variable_1[0]} {variable_1[1]} -{variable_0[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} {variable_1[1]} {result[1]} -{variable_0[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} {variable_1[1]} -{variable_0[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {next_carry[0]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}',
f'{next_carry[0]} -{carry[0]}',
f'{result[0]} -{carry[0]}']


def modadd_truncated_msb(result, variable_0, variable_1, carry):
return [f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {variable_1[1]} -{result[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} {result[1]} -{variable_1[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_0[1]} {variable_1[0]} -{variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} {variable_1[1]} {result[1]} -{variable_0[1]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} {variable_1[1]} -{variable_0[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[0]}',
f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}',
f'{result[0]} -{carry[0]}']


# ---------------------------- #
# - Running SAT solver - #
# ---------------------------- #
Expand Down
37 changes: 19 additions & 18 deletions claasp/components/modular_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -909,24 +909,25 @@ def sat_deterministic_truncated_xor_differential_trail_constraints(self):
"""
in_ids_0, in_ids_1 = self._generate_input_double_ids()
out_len, out_ids_0, out_ids_1 = self._generate_output_double_ids()
constraints = []
for i in range(out_len):
pivot = (in_ids_0[i], in_ids_1[i], in_ids_0[i + out_len], in_ids_1[i + out_len])
for j in range(0, i):
constraints.extend(f'{out_ids_0[j]} -{p}' for p in pivot)
for j in range(i + 1, out_len):
constraints.extend(f'-{in_ids_0[j]} -{p}' for p in pivot)
constraints.extend(f'-{in_ids_1[j]} -{p}' for p in pivot)
constraints.extend(f'-{in_ids_0[j + out_len]} -{p}' for p in pivot)
constraints.extend(f'-{in_ids_1[j + out_len]} -{p}' for p in pivot)
constraints.extend(f'-{out_ids_0[j]} -{p}' for p in pivot)
constraints.extend(f'-{out_ids_1[j]} -{p}' for p in pivot)
xor_constraints = sat_utils.cnf_xor_truncated((out_ids_0[i], out_ids_1[i]),
(pivot[0], pivot[1]),
(pivot[2], pivot[3]))
constraints.extend(xor_constraints)

return out_ids_0 + out_ids_1, constraints
carry_ids_0 = [f'carry_{out_id}_0' for out_id in out_ids_0]
carry_ids_1 = [f'carry_{out_id}_1' for out_id in out_ids_1]
constraints = [f'-{carry_ids_0[-1]} -{carry_ids_1[-1]}']
constraints.extend(sat_utils.modadd_truncated_msb((out_ids_0[0], out_ids_1[0]),
(in_ids_0[0], in_ids_1[0]),
(in_ids_0[out_len], in_ids_1[out_len]),
(carry_ids_0[0], carry_ids_1[0])))
for i in range(1, out_len - 1):
constraints.extend(sat_utils.modadd_truncated((out_ids_0[i], out_ids_1[i]),
(in_ids_0[i], in_ids_1[i]),
(in_ids_0[i+out_len], in_ids_1[i+out_len]),
(carry_ids_0[i], carry_ids_1[i]),
(carry_ids_0[i-1], carry_ids_1[i-1])))
constraints.extend(sat_utils.modadd_truncated_lsb((out_ids_0[-1], out_ids_1[-1]),
(in_ids_0[out_len-1], in_ids_1[out_len-1]),
(in_ids_0[2*out_len-1], in_ids_1[2*out_len-1]),
(carry_ids_0[-2], carry_ids_1[-2])))

return out_ids_0 + out_ids_1 + carry_ids_0 + carry_ids_1, constraints

def sat_xor_linear_mask_propagation_constraints(self, model=None):
"""
Expand Down

0 comments on commit 5db90d7

Please sign in to comment.