diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_deterministic_truncated_xor_differential_model.py index ecc202ab..7dbc3de4 100644 --- a/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_deterministic_truncated_xor_differential_model.py +++ b/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_deterministic_truncated_xor_differential_model.py @@ -19,7 +19,8 @@ from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_BITWISE_DETERMINISTIC_TRUNCATED, \ MILP_BACKWARD_SUFFIX, MILP_BUILDING_MESSAGE, MILP_TRUNCATED_XOR_DIFFERENTIAL_OBJECTIVE -from claasp.cipher_modules.models.milp.utils.utils import fix_variables_value_deterministic_truncated_xor_differential_constraints +from claasp.cipher_modules.models.milp.utils.milp_truncated_utils import \ + fix_variables_value_deterministic_truncated_xor_differential_constraints from claasp.cipher_modules.models.milp.milp_model import MilpModel, verbose_print from claasp.cipher_modules.models.utils import set_component_solution from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model.py index 936de7a4..c241ad3e 100644 --- a/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model.py +++ b/claasp/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model.py @@ -25,7 +25,7 @@ from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_BITWISE_IMPOSSIBLE, \ MILP_BITWISE_IMPOSSIBLE_AUTO, MILP_BACKWARD_SUFFIX, MILP_BUILDING_MESSAGE from claasp.name_mappings import CIPHER_OUTPUT, INPUT_KEY -from claasp.cipher_modules.models.milp.utils import utils as milp_utils +from claasp.cipher_modules.models.milp.utils import utils as milp_utils, milp_truncated_utils class MilpBitwiseImpossibleXorDifferentialModel(MilpBitwiseDeterministicTruncatedXorDifferentialModel): @@ -272,29 +272,12 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe mip.add_constraint(constraint) # finding incompatibility - constraints = [] - forward_output = [c for c in self._forward_cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] - all_inconsistent_vars = [] - backward_components = [c for c in self._backward_cipher.get_all_components() if - c.description == ['round_output'] and set(c.input_id_links) != { - forward_output.id + MILP_BACKWARD_SUFFIX}] - - key_flow = set(get_key_schedule_component_ids(self._cipher)) - {INPUT_KEY} - backward_key_flow = [f'{id}{MILP_BACKWARD_SUFFIX}' for id in key_flow] - - if include_all_components: - backward_components = set(self._backward_cipher.get_all_components()) - set(self._backward_cipher.get_component_from_id(key_flow_id) for key_flow_id in backward_key_flow) - - for backward_component in backward_components: - incompatibility_constraints, inconsistent_vars = milp_utils.generate_incompatiblity_constraints_for_component(self, MILP_BITWISE_IMPOSSIBLE_AUTO, x, x_class, backward_component, include_all_components) - all_inconsistent_vars += inconsistent_vars - constraints.extend(incompatibility_constraints) - - constraints.extend([sum(all_inconsistent_vars) == 1]) + constraints = milp_truncated_utils.generate_all_incompatibility_constraints_for_fully_automatic_model(self, MILP_BITWISE_IMPOSSIBLE_AUTO, x, x_class, include_all_components) for constraint in constraints: mip.add_constraint(constraint) + forward_output = [c for c in self._forward_cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] _, forward_output_id_tuples = forward_output._get_input_output_variables_tuples() mip.add_constraint(p["number_of_unknown_patterns"] == sum( x[output_msb] for output_msb in [id[0] for id in forward_output_id_tuples])) diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_deterministic_truncated_xor_differential_model.py index fdd08e58..57794969 100644 --- a/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_deterministic_truncated_xor_differential_model.py +++ b/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_deterministic_truncated_xor_differential_model.py @@ -21,7 +21,9 @@ from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_WORDWISE_DETERMINISTIC_TRUNCATED, \ MILP_BUILDING_MESSAGE, MILP_TRUNCATED_XOR_DIFFERENTIAL_OBJECTIVE from claasp.cipher_modules.models.milp.utils.utils import espresso_pos_to_constraints, \ - fix_variables_value_deterministic_truncated_xor_differential_constraints, _get_variables_values_as_string + _get_variables_values_as_string +from claasp.cipher_modules.models.milp.utils.milp_truncated_utils import \ + fix_variables_value_deterministic_truncated_xor_differential_constraints from claasp.cipher_modules.models.utils import set_component_solution from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, WORD_OPERATION, LINEAR_LAYER, SBOX, MIX_COLUMN) diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_impossible_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_impossible_xor_differential_model.py index a36a7aa3..251c8de6 100644 --- a/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_impossible_xor_differential_model.py +++ b/claasp/cipher_modules/models/milp/milp_models/milp_wordwise_impossible_xor_differential_model.py @@ -29,7 +29,7 @@ from claasp.cipher_modules.models.milp.utils.utils import espresso_pos_to_constraints from claasp.cipher_modules.models.utils import set_component_solution from claasp.name_mappings import CIPHER_OUTPUT, INPUT_KEY -from claasp.cipher_modules.models.milp.utils import utils as milp_utils +from claasp.cipher_modules.models.milp.utils import utils as milp_utils, milp_truncated_utils class MilpWordwiseImpossibleXorDifferentialModel(MilpWordwiseDeterministicTruncatedXorDifferentialModel): @@ -299,36 +299,17 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe mip.add_constraint(constraint) # finding incompatibility - constraints = [] - forward_output = [c for c in self._forward_cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] - all_inconsistent_vars = [] - backward_components = [c for c in self._backward_cipher.get_all_components() if - c.description == ['round_output'] and set(c.input_id_links) != { - forward_output.id + MILP_BACKWARD_SUFFIX}] - - key_flow = set(get_key_schedule_component_ids(self._cipher)) - {INPUT_KEY} - backward_key_flow = [f'{id}{MILP_BACKWARD_SUFFIX}' for id in key_flow] - - if include_all_components: - backward_components = set(self._backward_cipher.get_all_components()) - set( - self._backward_cipher.get_component_from_id(key_flow_id) for key_flow_id in backward_key_flow) - - for backward_component in backward_components: - incompatibility_constraints, inconsistent_vars = milp_utils.generate_incompatiblity_constraints_for_component( - self, MILP_WORDWISE_IMPOSSIBLE_AUTO, x, x_class, backward_component, include_all_components) - all_inconsistent_vars += inconsistent_vars - constraints.extend(incompatibility_constraints) + constraints = milp_truncated_utils.generate_all_incompatibility_constraints_for_fully_automatic_model(self, MILP_WORDWISE_IMPOSSIBLE_AUTO, x, x_class, include_all_components) # decryption input is fixed and non-zero constraints.extend( [x_class[id] <= 1 for id in self._backward_cipher.inputs] + [sum([x_class[id] for id in self._backward_cipher.inputs]) >= 1]) - constraints.extend([sum(all_inconsistent_vars) == 1]) - for constraint in constraints: mip.add_constraint(constraint) # unknown patterns are tuples of the form (1,x) (i.e pattern = 2 or 3) + forward_output = [c for c in self._forward_cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] _, forward_output_id_tuple = forward_output._get_wordwise_input_output_linked_class_tuples(self) mip.add_constraint( p["number_of_unknown_patterns"] == sum(x[output_msb] for output_msb in [id[0] for id in forward_output_id_tuple])) diff --git a/claasp/cipher_modules/models/milp/utils/milp_truncated_utils.py b/claasp/cipher_modules/models/milp/utils/milp_truncated_utils.py new file mode 100644 index 00000000..2faa0f52 --- /dev/null +++ b/claasp/cipher_modules/models/milp/utils/milp_truncated_utils.py @@ -0,0 +1,114 @@ +from claasp.cipher_modules.inverse_cipher import get_key_schedule_component_ids +from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_BITWISE_IMPOSSIBLE_AUTO, \ + MILP_WORDWISE_IMPOSSIBLE_AUTO, MILP_BACKWARD_SUFFIX +from claasp.cipher_modules.models.milp.utils.utils import milp_if_then +from claasp.name_mappings import CIPHER_OUTPUT, INPUT_KEY + +def generate_incompatiblity_constraints_for_component(model, model_type, x, x_class, backward_component, include_all_components): + + incompatiblity_constraints = [] + + if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: + output_size = backward_component.output_bit_size + input_ids, output_ids = backward_component._get_input_output_variables() + + else: + output_size = backward_component.output_bit_size // model.word_size + input_ids, output_ids = backward_component._get_wordwise_input_output_linked_class(model) + + + if include_all_components: + # for multiple input components such as the XOR, ensures compatibility occurs on the correct branch + inputs_to_be_kept = [] + for index, input_id in enumerate(["_".join(i.split("_")[:-1]) for i in set(backward_component.input_id_links)]): + if INPUT_KEY not in input_id and [link + MILP_BACKWARD_SUFFIX for link in + model._cipher.get_component_from_id(input_id).input_id_links] == [ + backward_component.id]: + inputs_to_be_kept.extend([_ for _ in input_ids if input_id in _]) + backward_vars = [x_class[id] for id in (inputs_to_be_kept or input_ids) if INPUT_KEY not in id] + else: + backward_vars = [x_class[id] for id in output_ids] + + if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: + forward_vars = [x_class["_".join(id.split("_")[:-2] + [id.split("_")[-1]])] for id in output_ids] + else: + forward_vars = [x_class["_".join(id.split("_")[:-4] + id.split("_")[-3:])] for id in output_ids] + + inconsistent_vars = [x[f"{backward_component.id}_inconsistent_{_}"] for _ in range(output_size)] + + for inconsistent_index in range(output_size): + if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: + incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] == 1] + else: + incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] + incompatiblity_constraints.extend(milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, + model._model.get_max(x_class) * 2)) + + + return incompatiblity_constraints, inconsistent_vars + + +def generate_all_incompatibility_constraints_for_fully_automatic_model(model, model_type, x, x_class, include_all_components): + + assert model_type in [MILP_BITWISE_IMPOSSIBLE_AUTO, MILP_WORDWISE_IMPOSSIBLE_AUTO] + + constraints = [] + forward_output = [c for c in model._forward_cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] + all_inconsistent_vars = [] + backward_components = [c for c in model._backward_cipher.get_all_components() if + c.description == ['round_output'] and set(c.input_id_links) != { + forward_output.id + MILP_BACKWARD_SUFFIX}] + + key_flow = set(get_key_schedule_component_ids(model._cipher)) - {INPUT_KEY} + backward_key_flow = [f'{id}{MILP_BACKWARD_SUFFIX}' for id in key_flow] + + if include_all_components: + backward_components = set(model._backward_cipher.get_all_components()) - set( + model._backward_cipher.get_component_from_id(key_flow_id) for key_flow_id in backward_key_flow) + + for backward_component in backward_components: + incompatibility_constraints, inconsistent_vars = generate_incompatiblity_constraints_for_component(model, model_type, x, x_class, backward_component, include_all_components) + all_inconsistent_vars += inconsistent_vars + constraints.extend(incompatibility_constraints) + + constraints.extend([sum(all_inconsistent_vars) == 1]) + + return constraints + + +def fix_variables_value_deterministic_truncated_xor_differential_constraints(milp_model, model_variables, fixed_variables=[]): + constraints = [] + if 'Wordwise' in milp_model.__class__.__name__: + prefix = "_word" + suffix = "_class" + else: + prefix = "" + suffix = "" + + for fixed_variable in fixed_variables: + if fixed_variable["constraint_type"] == "equal": + for index, bit_position in enumerate(fixed_variable["bit_positions"]): + component_bit = f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}' + constraints.append(model_variables[component_bit] == fixed_variable["bit_values"][index]) + else: + if sum(fixed_variable["bit_values"]) == 0: + constraints.append(sum(model_variables[f'{fixed_variable["component_id"]}{prefix}_{i}{suffix}'] for i in fixed_variable["bit_positions"]) >= 1) + else: + M = milp_model._model.get_max(model_variables) + 1 + d = milp_model._binary_variable + one_among_n = 0 + + for index, bit_position in enumerate(fixed_variable["bit_positions"]): + # eq = 1 iff bit_position == diff_index + eq = d[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}_is_diff_index'] + one_among_n += eq + + # x[diff_index] < fixed_variable[diff_index] or fixed_variable[diff_index] < x[diff_index] + dummy = d[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}_is_diff_index'] + a = model_variables[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}'] + b = fixed_variable["bit_values"][index] + constraints.extend([a <= b - 1 + M * (2 - dummy - eq), a >= b + 1 - M * (dummy + 1 - eq)]) + + constraints.append(one_among_n == 1) + + return constraints diff --git a/claasp/cipher_modules/models/milp/utils/utils.py b/claasp/cipher_modules/models/milp/utils/utils.py index 0f6c1a8f..d5463f2e 100644 --- a/claasp/cipher_modules/models/milp/utils/utils.py +++ b/claasp/cipher_modules/models/milp/utils/utils.py @@ -32,7 +32,6 @@ MILP_WORDWISE_DETERMINISTIC_TRUNCATED, MILP_BACKWARD_SUFFIX, MILP_TRUNCATED_XOR_DIFFERENTIAL_OBJECTIVE, \ MILP_XOR_DIFFERENTIAL_OBJECTIVE, MILP_BITWISE_IMPOSSIBLE, MILP_WORDWISE_IMPOSSIBLE, MILP_BITWISE_IMPOSSIBLE_AUTO, \ MILP_WORDWISE_IMPOSSIBLE_AUTO -from claasp.name_mappings import INPUT_KEY ### -------------------------External solver parsing methods------------------------- ### @@ -647,88 +646,6 @@ def milp_xor_truncated_wordwise(model, input_1, input_2, output): all_vars = [x[i] for i in input_1 + input_2 + output] return espresso_pos_to_constraints(espresso_inequalities, all_vars) -def fix_variables_value_deterministic_truncated_xor_differential_constraints(milp_model, model_variables, fixed_variables=[]): - constraints = [] - if 'Wordwise' in milp_model.__class__.__name__: - prefix = "_word" - suffix = "_class" - else: - prefix = "" - suffix = "" - - for fixed_variable in fixed_variables: - if fixed_variable["constraint_type"] == "equal": - for index, bit_position in enumerate(fixed_variable["bit_positions"]): - component_bit = f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}' - constraints.append(model_variables[component_bit] == fixed_variable["bit_values"][index]) - else: - if sum(fixed_variable["bit_values"]) == 0: - constraints.append(sum(model_variables[f'{fixed_variable["component_id"]}{prefix}_{i}{suffix}'] for i in fixed_variable["bit_positions"]) >= 1) - else: - M = milp_model._model.get_max(model_variables) + 1 - d = milp_model._binary_variable - one_among_n = 0 - - for index, bit_position in enumerate(fixed_variable["bit_positions"]): - # eq = 1 iff bit_position == diff_index - eq = d[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}_is_diff_index'] - one_among_n += eq - - # x[diff_index] < fixed_variable[diff_index] or fixed_variable[diff_index] < x[diff_index] - dummy = d[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}_is_diff_index'] - a = model_variables[f'{fixed_variable["component_id"]}{prefix}_{bit_position}{suffix}'] - b = fixed_variable["bit_values"][index] - constraints.extend([a <= b - 1 + M * (2 - dummy - eq), a >= b + 1 - M * (dummy + 1 - eq)]) - - constraints.append(one_among_n == 1) - - return constraints - -def generate_incompatiblity_constraints_for_component(model, model_type, x, x_class, backward_component, include_all_components): - - assert model_type in [MILP_BITWISE_IMPOSSIBLE_AUTO, MILP_WORDWISE_IMPOSSIBLE_AUTO] - - incompatiblity_constraints = [] - - if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: - output_size = backward_component.output_bit_size - input_ids, output_ids = backward_component._get_input_output_variables() - - else: - output_size = backward_component.output_bit_size // model.word_size - input_ids, output_ids = backward_component._get_wordwise_input_output_linked_class(model) - - - if include_all_components: - # for multiple input components such as the XOR, ensures compatibility occurs on the correct branch - inputs_to_be_kept = [] - for index, input_id in enumerate(["_".join(i.split("_")[:-1]) for i in set(backward_component.input_id_links)]): - if f'{INPUT_KEY}' not in input_id and [link + MILP_BACKWARD_SUFFIX for link in - model._cipher.get_component_from_id(input_id).input_id_links] == [ - backward_component.id]: - inputs_to_be_kept.extend([_ for _ in input_ids if input_id in _]) - backward_vars = [x_class[id] for id in (inputs_to_be_kept or input_ids) if INPUT_KEY not in id] - else: - backward_vars = [x_class[id] for id in output_ids] - - if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: - forward_vars = [x_class["_".join(id.split("_")[:-2] + [id.split("_")[-1]])] for id in output_ids] - else: - forward_vars = [x_class["_".join(id.split("_")[:-4] + id.split("_")[-3:])] for id in output_ids] - - inconsistent_vars = [x[f"{backward_component.id}_inconsistent_{_}"] for _ in range(output_size)] - - for inconsistent_index in range(output_size): - if model_type == MILP_BITWISE_IMPOSSIBLE_AUTO: - incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] == 1] - else: - incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] - incompatiblity_constraints.extend(milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, - model._model.get_max(x_class) * 2)) - - - return incompatiblity_constraints, inconsistent_vars - ### -------------------------Solution parser ------------------------- ### def _get_component_values_for_impossible_models(model, objective_variables, components_variables):