diff --git a/claasp/cipher_modules/models/cp/cp_models/cp_xor_linear_model.py b/claasp/cipher_modules/models/cp/cp_models/cp_xor_linear_model.py index 7e6bd1d7..3b33c7d3 100644 --- a/claasp/cipher_modules/models/cp/cp_models/cp_xor_linear_model.py +++ b/claasp/cipher_modules/models/cp/cp_models/cp_xor_linear_model.py @@ -239,6 +239,17 @@ def find_all_xor_linear_trails_with_fixed_weight(self, fixed_weight, fixed_value sage: trails = cp.find_all_xor_linear_trails_with_fixed_weight(1) # long sage: len(trails) 12 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.cp.cp_models.cp_xor_linear_model import CpXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: cp = CpXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = cp.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key]) + sage: len(trails) + 8 """ start = tm.time() self.build_xor_linear_trail_model(fixed_weight, fixed_values) @@ -276,6 +287,17 @@ def find_all_xor_linear_trails_with_weight_at_most(self, min_weight, max_weight= sage: trails = cp.find_all_xor_linear_trails_with_weight_at_most(0, 1) sage: len(trails) 13 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.cp.cp_models.cp_xor_linear_model import CpXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: cp = CpXorLinearModel(speck) + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = cp.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) + sage: len(trails) + 73 """ start = tm.time() self.build_xor_linear_trail_model(0, fixed_values) @@ -316,7 +338,18 @@ def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name='Chuf sage: cp= CpXorLinearModel(speck) sage: trail = cp.find_lowest_weight_xor_linear_trail() sage: trail['total_weight'] - 3.0 + '3.0' + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.cp.cp_models.cp_xor_linear_model import CpXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=16, key_bit_size=32, number_of_rounds=4) + sage: cp = CpXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32) + sage: trail = cp.find_lowest_weight_xor_linear_trail(fixed_values=[key]) + sage: trail['total_weight'] + '3.0' """ start = tm.time() self.build_xor_linear_trail_model(-1, fixed_values) @@ -349,6 +382,15 @@ def find_one_xor_linear_trail(self, fixed_values=[], solver_name='Chuffed'): sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4) sage: cp = CpXorLinearModel(speck) sage: cp.find_one_xor_linear_trail() # random + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.cp.cp_models.cp_xor_linear_model import CpXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4) + sage: cp = CpXorLinearModel(speck) + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64) + sage: cp.find_one_xor_linear_trail(fixed_values=[key]) # random """ start = tm.time() self.build_xor_linear_trail_model(0, fixed_values) @@ -381,7 +423,18 @@ def find_one_xor_linear_trail_with_fixed_weight(self, fixed_weight=-1, fixed_val sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4) sage: cp = CpXorLinearModel(speck) - sage: trail = cp.find_one_xor_linear_trail_with_fixed_weight(3) # random + sage: trail = cp.find_one_xor_linear_trail_with_fixed_weight(3) + sage: trail['total_weight'] + '3.0' + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.cp.cp_models.cp_xor_linear_model import CpXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: cp = CpXorLinearModel(speck) + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trail = cp.find_one_xor_linear_trail_with_fixed_weight(3, fixed_values=[key]) sage: trail['total_weight'] '3.0' """ diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_xor_differential_model.py index f04d0eb3..2c9e186e 100644 --- a/claasp/cipher_modules/models/milp/milp_models/milp_xor_differential_model.py +++ b/claasp/cipher_modules/models/milp/milp_models/milp_xor_differential_model.py @@ -24,11 +24,11 @@ from claasp.cipher_modules.models.milp.milp_model import MilpModel, verbose_print from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_XOR_DIFFERENTIAL, MILP_PROBABILITY_SUFFIX, \ MILP_BUILDING_MESSAGE, MILP_XOR_DIFFERENTIAL_OBJECTIVE -from claasp.cipher_modules.models.milp.utils.utils import _string_to_hex, _get_variables_values_as_string +from claasp.cipher_modules.models.milp.utils.utils import _string_to_hex, _get_variables_values_as_string, _filter_fixed_variables from claasp.cipher_modules.models.utils import integer_to_bit_list, set_component_solution, \ get_single_key_scenario_format_for_fixed_values from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, - WORD_OPERATION, LINEAR_LAYER, SBOX, MIX_COLUMN) + WORD_OPERATION, LINEAR_LAYER, SBOX, MIX_COLUMN, INPUT_KEY) class MilpXorDifferentialModel(MilpModel): @@ -148,7 +148,7 @@ def find_all_xor_differential_trails_with_fixed_weight(self, fixed_weight, fixed EXAMPLES:: # single-key setting - from claasp.cipher_modules.models.milp.milp_models.milp_xor_differential_model import MilpXorDifferentialModel + sage: from claasp.cipher_modules.models.milp.milp_models.milp_xor_differential_model import MilpXorDifferentialModel sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: speck = SpeckBlockCipher(number_of_rounds=5) sage: milp = MilpXorDifferentialModel(speck) @@ -184,8 +184,10 @@ def find_all_xor_differential_trails_with_fixed_weight(self, fixed_weight, fixed end = time.time() building_time = end - start + if fixed_values == []: + fixed_values = get_single_key_scenario_format_for_fixed_values(self._cipher) if self.is_single_key(fixed_values): - inputs_ids = [i for i in self._cipher.inputs if "key" not in i] + inputs_ids = [i for i in self._cipher.inputs if INPUT_KEY not in i] else: inputs_ids = self._cipher.inputs @@ -202,27 +204,7 @@ def find_all_xor_differential_trails_with_fixed_weight(self, fixed_weight, fixed self._number_of_trails_found += 1 verbose_print(f"trails found : {self._number_of_trails_found}") list_trails.append(solution) - fixed_variables = [] - for index, input in enumerate(inputs_ids): - fixed_variable = {} - fixed_variable["component_id"] = input - input_bit_size = self._cipher.inputs_bit_size[index] - fixed_variable["bit_positions"] = list(range(input_bit_size)) - fixed_variable["constraint_type"] = "not_equal" - fixed_variable["bit_values"] = integer_to_bit_list( - BitArray(solution["components_values"][input]["value"]).int, input_bit_size, 'big') - fixed_variables.append(fixed_variable) - - for cipher_round in self._cipher.rounds_as_list: - for component in cipher_round.components: - fixed_variable = {} - fixed_variable["component_id"] = component.id - output_bit_size = component.output_bit_size - fixed_variable["bit_positions"] = list(range(output_bit_size)) - fixed_variable["constraint_type"] = "not_equal" - fixed_variable["bit_values"] = integer_to_bit_list( - BitArray(solution["components_values"][component.id]["value"]).int, output_bit_size, 'big') - fixed_variables.append(fixed_variable) + fixed_variables = self._get_fixed_variables_from_solution(fixed_values, inputs_ids, solution) fix_var_constraints = self.exclude_variables_value_constraints(fixed_variables) number_new_constraints += len(fix_var_constraints) @@ -230,6 +212,8 @@ def find_all_xor_differential_trails_with_fixed_weight(self, fixed_weight, fixed mip.add_constraint(constraint) except Exception: looking_for_other_solutions = 0 + finally: + sys.stdout = sys.__stdout__ number_constraints = mip.number_of_constraints() mip.remove_constraints(range(number_constraints - number_new_constraints, number_constraints)) @@ -401,7 +385,7 @@ def find_all_xor_differential_trails_with_weight_at_most(self, min_weight, max_w fixed_values = get_single_key_scenario_format_for_fixed_values(self._cipher) inputs_ids = self._cipher.inputs if self.is_single_key(fixed_values): - inputs_ids = [i for i in self._cipher.inputs if "key" not in i] + inputs_ids = [i for i in self._cipher.inputs if INPUT_KEY not in i] list_trails = [] for weight in range(min_weight, max_weight + 1): @@ -421,8 +405,7 @@ def find_all_xor_differential_trails_with_weight_at_most(self, min_weight, max_w self._number_of_trails_found += 1 verbose_print(f"trails found : {self._number_of_trails_found}") list_trails.append(solution) - fixed_variables = self.get_fixed_variables_for_all_xor_differential_trails_with_weight_at_most( - fixed_values, inputs_ids, solution) + fixed_variables = self._get_fixed_variables_from_solution(fixed_values, inputs_ids, solution) fix_var_constraints = self.exclude_variables_value_constraints(fixed_variables) for constraint in fix_var_constraints: @@ -430,6 +413,8 @@ def find_all_xor_differential_trails_with_weight_at_most(self, min_weight, max_w number_new_constraints += len(fix_var_constraints) except Exception: looking_for_other_solutions = 0 + finally: + sys.stdout = sys.__stdout__ number_constraints = mip.number_of_constraints() mip.remove_constraints(range(number_constraints - number_new_constraints, number_constraints)) self._number_of_trails_found = 0 @@ -597,31 +582,29 @@ def find_one_xor_differential_trail_with_fixed_weight(self, fixed_weight, fixed_ return solution - def get_fixed_variables_for_all_xor_differential_trails_with_weight_at_most(self, fixed_values, inputs_ids, - solution): + def _get_fixed_variables_from_solution(self, fixed_values, inputs_ids, solution): fixed_variables = [] - for index, input in enumerate(inputs_ids): - input_bit_size = self._cipher.inputs_bit_size[index] + for input in inputs_ids: + input_bit_size = self._cipher.inputs_bit_size[self._cipher.inputs.index(input)] fixed_variable = {"component_id": input, "bit_positions": list(range(input_bit_size)), "constraint_type": "not_equal", "bit_values": (integer_to_bit_list( BitArray(solution["components_values"][input]["value"]).int, input_bit_size, 'big'))} + _filter_fixed_variables(fixed_values, fixed_variable, input) + fixed_variables.append(fixed_variable) - fixed_variables += [fixed_variable for dictio in fixed_values - if dictio["component_id"] == input and - dictio["bit_values"] != fixed_variable["bit_values"]] - - for component in self._cipher.get_all_components(): - output_bit_size = component.output_bit_size - fixed_variable = {"component_id": component.id, - "bit_positions": list(range(output_bit_size)), - "constraint_type": "not_equal", - "bit_values": integer_to_bit_list( - BitArray(solution["components_values"][component.id]["value"]).int, - output_bit_size, 'big')} - fixed_variables.append(fixed_variable) + for component in self._cipher.get_all_components(): + output_bit_size = component.output_bit_size + fixed_variable = {"component_id": component.id, + "bit_positions": list(range(output_bit_size)), + "constraint_type": "not_equal", + "bit_values": integer_to_bit_list( + BitArray(solution["components_values"][component.id]["value"]).int, + output_bit_size, 'big')} + _filter_fixed_variables(fixed_values, fixed_variable, component.id) + fixed_variables.append(fixed_variable) return fixed_variables diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py index 1f31d4de..db80122d 100644 --- a/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py +++ b/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py @@ -139,6 +139,17 @@ def find_all_xor_linear_trails_with_fixed_weight(self, fixed_weight, fixed_value sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(1) sage: len(trails) == 4 True + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: sat = SatXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key]) # long + sage: len(trails) == 8 + True """ start_building_time = time.time() self.build_xor_linear_trail_model(weight=fixed_weight, fixed_variables=fixed_values) @@ -156,7 +167,9 @@ def find_all_xor_linear_trails_with_fixed_weight(self, fixed_weight, fixed_value value_to_avoid = int(value_as_hex_string, base=16) bit_len = len(value_as_hex_string) * 4 minus = ['-' * (value_to_avoid >> i & 1) for i in reversed(range(bit_len))] - if component.endswith(INPUT_BIT_ID_SUFFIX) or component.endswith(OUTPUT_BIT_ID_SUFFIX): + if CONSTANT in component and component.endswith(INPUT_BIT_ID_SUFFIX): + continue + elif component.endswith(INPUT_BIT_ID_SUFFIX) or component.endswith(OUTPUT_BIT_ID_SUFFIX): component_id = component[:-2] suffix = component[-2:] else: @@ -191,7 +204,6 @@ def find_all_xor_linear_trails_with_weight_at_most(self, min_weight, max_weight, EXAMPLES:: - # without key schedule sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: speck = SpeckBlockCipher(number_of_rounds=3) @@ -199,6 +211,17 @@ def find_all_xor_linear_trails_with_weight_at_most(self, min_weight, max_weight, sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 2) # long sage: len(trails) == 187 True + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: sat = SatXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) # long + sage: len(trails) == 73 + True """ solutions_list = [] for weight in range(min_weight, max_weight + 1): @@ -240,6 +263,17 @@ def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name='cryp sage: trail = sat.find_lowest_weight_xor_linear_trail() sage: trail['total_weight'] 1.0 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=16, key_bit_size=32, number_of_rounds=4) + sage: sat = SatXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32) + sage: trail = sat.find_lowest_weight_xor_linear_trail(fixed_values=[key]) + sage: trail['total_weight'] + 3.0 """ current_weight = 0 start_building_time = time.time() @@ -296,6 +330,15 @@ def find_one_xor_linear_trail(self, fixed_values=[], solver_name='cryptominisat' ... 'status': 'SATISFIABLE', 'building_time_seconds': 0.010079622268676758} + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(number_of_rounds=4) + sage: sat = SatXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64) + sage: sat.find_one_xor_linear_trail(fixed_values=[key]) # random """ start_building_time = time.time() self.build_xor_linear_trail_model(fixed_variables=fixed_values) @@ -332,6 +375,17 @@ def find_one_xor_linear_trail_with_fixed_weight(self, fixed_weight, fixed_values sage: trail = sat.find_one_xor_linear_trail_with_fixed_weight(7) sage: trail['total_weight'] 7.0 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: sat = SatXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trail = sat.find_one_xor_linear_trail_with_fixed_weight(3, fixed_values=[key]) + sage: trail['total_weight'] + 3.0 """ start_building_time = time.time() self.build_xor_linear_trail_model(weight=fixed_weight, fixed_variables=fixed_values) diff --git a/claasp/cipher_modules/models/smt/smt_models/smt_xor_linear_model.py b/claasp/cipher_modules/models/smt/smt_models/smt_xor_linear_model.py index e1474ee9..4c023ba5 100644 --- a/claasp/cipher_modules/models/smt/smt_models/smt_xor_linear_model.py +++ b/claasp/cipher_modules/models/smt/smt_models/smt_xor_linear_model.py @@ -173,6 +173,17 @@ def find_all_xor_linear_trails_with_fixed_weight(self, fixed_weight, fixed_value sage: trails = smt.find_all_xor_linear_trails_with_fixed_weight(1) sage: len(trails) 4 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: smt = SmtXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = smt.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key]) # long + sage: len(trails) + 8 """ start_building_time = time.time() self.build_xor_linear_trail_model(weight=fixed_weight, fixed_variables=fixed_values) @@ -189,7 +200,9 @@ def find_all_xor_linear_trails_with_fixed_weight(self, fixed_weight, fixed_value value_as_hex_string = solution['components_values'][component]['value'] value_to_avoid = int(value_as_hex_string, base=16) bit_len = len(value_as_hex_string) * 4 - if component.endswith(INPUT_BIT_ID_SUFFIX) or component.endswith(OUTPUT_BIT_ID_SUFFIX): + if CONSTANT in component and component.endswith(INPUT_BIT_ID_SUFFIX): + continue + elif component.endswith(INPUT_BIT_ID_SUFFIX) or component.endswith(OUTPUT_BIT_ID_SUFFIX): component_id = component[:-2] suffix = component[-2:] else: @@ -236,6 +249,17 @@ def find_all_xor_linear_trails_with_weight_at_most(self, min_weight, max_weight, sage: trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 2) # long sage: len(trails) 187 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: smt = SmtXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) + sage: len(trails) + 73 """ solutions_list = [] for weight in range(min_weight, max_weight + 1): @@ -274,9 +298,20 @@ def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name='z3') sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: speck = SpeckBlockCipher(number_of_rounds=3) sage: smt = SmtXorLinearModel(speck) - sage: trail = smt.find_lowest_weight_xor_linear_trail) + sage: trail = smt.find_lowest_weight_xor_linear_trail() sage: trail['total_weight'] 2.0 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=16, key_bit_size=32, number_of_rounds=4) + sage: smt = SmtXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32) + sage: trail = smt.find_lowest_weight_xor_linear_trail(fixed_values=[key]) + sage: trail['total_weight'] + 3.0 """ current_weight = 0 start_building_time = time.time() @@ -333,6 +368,14 @@ def find_one_xor_linear_trail(self, fixed_values=[], solver_name='z3'): ... 'total_weight': 67, 'building_time_seconds': 0.003168344497680664} + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4) + sage: smt = SmtXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64) + sage: smt.find_one_xor_linear_trail(fixed_values=[key]) #random """ start_building_time = time.time() self.build_xor_linear_trail_model(fixed_variables=fixed_values) @@ -366,9 +409,20 @@ def find_one_xor_linear_trail_with_fixed_weight(self, fixed_weight, fixed_values sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: speck = SpeckBlockCipher(number_of_rounds=3) sage: smt = SmtXorLinearModel(speck) - sage: result = smt.find_one_xor_linear_trail_with_fixed_weight(7) - sage: result['total_weight'] + sage: trail = smt.find_one_xor_linear_trail_with_fixed_weight(7) + sage: trail['total_weight'] 7.0 + + # including the key schedule in the model + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) + sage: smt = SmtXorLinearModel(speck) + sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + sage: trail = smt.find_one_xor_linear_trail_with_fixed_weight(3, fixed_values=[key]) + sage: trail['total_weight'] + 3.0 """ start_building_time = time.time() self.build_xor_linear_trail_model(weight=fixed_weight, fixed_variables=fixed_values) diff --git a/claasp/components/constant_component.py b/claasp/components/constant_component.py index caa9f7db..11306a57 100644 --- a/claasp/components/constant_component.py +++ b/claasp/components/constant_component.py @@ -21,7 +21,6 @@ from claasp.component import Component from claasp.cipher_modules.models.sat.utils import constants from claasp.cipher_modules.models.smt.utils import utils as smt_utils -from claasp.cipher_modules.models.milp.utils import utils as milp_utils from claasp.cipher_modules.code_generator import constant_to_bitstring diff --git a/claasp/components/modular_component.py b/claasp/components/modular_component.py index 05a9a4eb..ae55aab4 100644 --- a/claasp/components/modular_component.py +++ b/claasp/components/modular_component.py @@ -1178,7 +1178,7 @@ def twoterms_milp_probability_xor_linear_constraints(self, binary_variable, inte constraints.append(x[f"{self.id}_chunk_{chunk_number}_dummy_{i}"] + x[input_vars[output_bit_size + i]] + x[input_vars[i]] + x[output_vars[i]] + - x[f"{self.id}_chunk_{chunk_number}_dummy_{i + 1}"] >= - 4) + x[f"{self.id}_chunk_{chunk_number}_dummy_{i + 1}"] <= 4) constraints.append(correlation[f"{self.id}_modadd_probability{chunk_number}"] == sum( x[f"{self.id}_chunk_{chunk_number}_dummy_{i}"] for i in range(output_bit_size))) diff --git a/claasp/components/xor_component.py b/claasp/components/xor_component.py index 30f6bcb3..a4218d60 100644 --- a/claasp/components/xor_component.py +++ b/claasp/components/xor_component.py @@ -601,13 +601,7 @@ def milp_xor_linear_constraints(self, model): for i in range(number_of_inputs): for j in range(output_bit_size): - input_component_id = input_vars[output_bit_size * i + j].rsplit('_', 1)[0] - if input_component_id in model.cipher.inputs: - constraints.append(x[ind_output_vars[j]] == x[ind_input_vars[output_bit_size * i + j]]) - else: - input_component = model.cipher.get_component_from_id(input_component_id) - if CONSTANT not in input_component.type: - constraints.append(x[ind_output_vars[j]] == x[ind_input_vars[output_bit_size * i + j]]) + constraints.append(x[ind_output_vars[j]] == x[ind_input_vars[output_bit_size * i + j]]) return variables, constraints diff --git a/tests/unit/cipher_modules/models/sat/sat_models/sat_xor_linear_model_test.py b/tests/unit/cipher_modules/models/sat/sat_models/sat_xor_linear_model_test.py index 9114692e..aa589a85 100644 --- a/tests/unit/cipher_modules/models/sat/sat_models/sat_xor_linear_model_test.py +++ b/tests/unit/cipher_modules/models/sat/sat_models/sat_xor_linear_model_test.py @@ -15,13 +15,13 @@ def test_branch_xor_linear_constraints(): assert constraints[-2] == '-xor_2_10_15_o cipher_output_2_12_31_i' assert constraints[-1] == 'xor_2_10_15_o -cipher_output_2_12_31_i' - def test_find_all_xor_linear_trails_with_weight_at_most(): - speck = SpeckBlockCipher(number_of_rounds=3) + speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) sat = SatXorLinearModel(speck) - trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 2) + key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) - assert len(trails) == 187 + assert len(trails) == 73 def test_find_lowest_weight_xor_linear_trail(): diff --git a/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_linear_model_test.py b/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_linear_model_test.py index a1db0176..d706f129 100644 --- a/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_linear_model_test.py +++ b/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_linear_model_test.py @@ -4,10 +4,12 @@ def test_find_all_xor_linear_trails_with_weight_at_most(): - speck = SpeckBlockCipher(number_of_rounds=3) + speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4) smt = SmtXorLinearModel(speck) - trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 2) - assert len(trails) == 187 + key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16) + trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) + + assert len(trails) == 73 def test_find_lowest_weight_xor_linear_trail():