diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py index ef3da5d2..dab892e3 100644 --- a/claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py +++ b/claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py @@ -130,8 +130,16 @@ def _build_weight_constraints(self, weight): RETURN: - **tuple**; A tuple containing a list of variables and a list of constraints. """ + hw_variables = [var_id for var_id in self._variables_list if var_id.startswith('hw_')] + linear_component_ids = [linear_component["component_id"] for linear_component in self.linear_components] + hw_linear_variables = [] + for linear_component_id in linear_component_ids: + for hw_variable in hw_variables: + if linear_component_id in hw_variable: + hw_linear_variables.append(hw_variable) + hw_variables.extend(hw_linear_variables) if weight == 0: return [], [f'-{var}' for var in hw_variables] @@ -158,7 +166,7 @@ def _build_unknown_variable_constraints(self, num_unknowns): def build_xor_differential_linear_model(self, weight=-1, num_unknown_vars=None): """ - Constructs a model to search for probabilistic truncated XOR differential trails. + Constructs a model to search for differential-linear trails. This model is a combination of the concrete XOR differential model, the bitwise truncated deterministic model, and the linear XOR differential model. @@ -266,22 +274,13 @@ def _parse_solver_output(self, variable2value): elif component.id in [d['component_id'] for d in self.truncated_components]: value = self._get_component_value_double_ids(component, variable2value) components_solutions[component.id] = set_component_solution(value) - hex_value = self._get_component_hex_value(component, constants.OUTPUT_BIT_ID_SUFFIX, variable2value) - components_solutions[component.id + "_o"] = set_component_solution(hex_value, 0) elif component.id in [d['component_id'] for d in self.linear_components]: hex_value = self._get_component_hex_value(component, constants.OUTPUT_BIT_ID_SUFFIX, variable2value) weight = self.calculate_component_weight(component, constants.OUTPUT_BIT_ID_SUFFIX, variable2value) total_weight_lin += weight - hex_value_input = self._get_component_hex_value_input(component, constants.INPUT_BIT_ID_SUFFIX, variable2value) components_solutions[component.id] = set_component_solution(hex_value, weight) - components_solutions[component.id + "_input"] = set_component_solution(hex_value_input, 0) - components_solutions[component.id + "_input"]["links"] = str(component.input_id_links) - components_solutions[component.id + "_input_id_links"] = { - input_id_link: self._get_component_hex_value( - self.cipher.get_component_from_id(input_id_link), constants.OUTPUT_BIT_ID_SUFFIX, variable2value) - for input_id_link in component.input_id_links - } + print("Total weights: diff =", total_weight_diff, "lin =", total_weight_lin) diff --git a/tests/unit/cipher_modules/models/sat/sat_models/sat_differential_linear_test.py b/tests/unit/cipher_modules/models/sat/sat_models/sat_differential_linear_test.py index e5d292e9..4d9259cb 100644 --- a/tests/unit/cipher_modules/models/sat/sat_models/sat_differential_linear_test.py +++ b/tests/unit/cipher_modules/models/sat/sat_models/sat_differential_linear_test.py @@ -1,15 +1,10 @@ -import time - -import numpy as np - from claasp.cipher_modules.models.sat.sat_models.sat_differential_linear_model import SatDifferentialLinearModel -from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list +from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list, \ + differential_linear_checker_for_permutation, differential_linear_checker_for_block_cipher_single_key from claasp.ciphers.block_ciphers.aradi_block_cipher_sbox import AradiBlockCipherSBox from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher from claasp.ciphers.permutations.chacha_permutation import ChachaPermutation -from claasp.ciphers.permutations.gaston_sbox_permutation import GastonSboxPermutation -from claasp.ciphers.permutations.gaston_sbox_permutation_top import GastonSboxPermutationTop -from claasp.utils.utils import get_k_th_bit +import itertools def generate_component_model_types(speck_cipher): @@ -38,68 +33,76 @@ def update_component_model_types_for_linear_components(component_model_types, li component_model_type["model_type"] = "sat_xor_linear_mask_propagation_constraints" -def extract_bits(columns, positions): - num_positions = len(positions) - num_columns = columns.shape[1] - bit_size = columns.shape[0] * 8 - # Initialize the result array - result = np.zeros((num_positions, num_columns), dtype=np.uint8) +def test_differential_linear_trail_with_fixed_weight_6_rounds_speck(): + """Test for finding a differential-linear trail with fixed weight for 6 rounds of Speck.""" + speck = SpeckBlockCipher(number_of_rounds=6) + middle_part_components = [] + bottom_part_components = [] + for round_number in range(2, 4): + middle_part_components.append(speck.get_components_in_round(round_number)) + for round_number in range(4, 6): + bottom_part_components.append(speck.get_components_in_round(round_number)) - # Loop to fill the result array with the required bits - for i in range(num_positions): - for j in range(num_columns): - byte_index = (bit_size - positions[i] -1) // 8 - bit_index = positions[i] % 8 - result[i, j] = get_k_th_bit(columns[:, j][byte_index], bit_index) - return result -def number_to_n_bit_binary_string(number, n_bits): - """Converts a number to an n-bit binary string with leading zero padding.""" - return format(number, f'0{n_bits}b') + middle_part_components = list(itertools.chain(*middle_part_components)) + bottom_part_components = list(itertools.chain(*bottom_part_components)) -def extract_bit_positions1(binary_str): - """Extracts bit positions from a binary+unknows string.""" - binary_str = binary_str[::-1] + middle_part_components = [component.id for component in middle_part_components] + bottom_part_components = [component.id for component in bottom_part_components] - positions = [i for i, bit in enumerate(binary_str) if bit in ['1']] - return positions + plaintext = set_fixed_variables( + component_id='plaintext', + constraint_type='equal', + bit_positions=range(32), + bit_values=integer_to_bit_list(0x02110a04, 32, 'big') + ) -def extract_bit_positions(hex_number): - binary_str = number_to_n_bit_binary_string(hex_number, 512) - print(len(binary_str), binary_str) - #binary_str = bin(hex_number)[2:] # bin() converts to binary, [2:] strips the '0b' prefix + key = set_fixed_variables( + component_id='key', + constraint_type='equal', + bit_positions=range(64), + bit_values=(0,) * 64 + ) - # Reverse the binary string to make the least significant bit at index 0 - binary_str = binary_str[::-1] + modadd_2_7 = set_fixed_variables( + component_id='modadd_4_7', + constraint_type='not_equal', + bit_positions=range(4), + bit_values=[0] * 4 + ) - # Find positions of '1's - positions = [i for i, bit in enumerate(binary_str) if bit == '1'] + ciphertext_difference = set_fixed_variables( + component_id='cipher_output_5_12', + constraint_type='equal', + bit_positions=range(32), + bit_values=integer_to_bit_list(0x02000201, 32, 'big') + ) - return positions + component_model_types = generate_component_model_types(speck) + update_component_model_types_for_truncated_components(component_model_types, middle_part_components) + update_component_model_types_for_linear_components(component_model_types, bottom_part_components) + sat_heterogeneous_model = SatDifferentialLinearModel(speck, component_model_types) -def repeat_input_difference(input_difference, num_samples, num_bytes): - """Repeats the input difference to generate a large sample for testing.""" - bytes_array = input_difference.to_bytes(num_bytes, 'big') - np_array = np.array(list(bytes_array), dtype=np.uint8) - column_array = np_array.reshape(-1, 1) - return np.tile(column_array, (1, num_samples)) + trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight( + weight=8, fixed_values=[key, plaintext, modadd_2_7, ciphertext_difference], solver_name="CADICAL_EXT", num_unknown_vars=31 + ) + assert trail["status"] == 'SATISFIABLE' -def test_differential_linear_trail_with_fixed_weight_3_rounds_speck(): - """Test for finding a differential-linear trail with fixed weight for 8 rounds of Speck.""" - aradi = SpeckBlockCipher(number_of_rounds=5) +def test_differential_linear_trail_with_fixed_weight_3_rounds_chacha(): + """Test for finding a differential-linear trail with fixed weight for 3 rounds of ChaCha permutation.""" + chacha = ChachaPermutation(number_of_rounds=6) import itertools - top_part_components = [] middle_part_components = [] bottom_part_components = [] - for round_number in range(2): - top_part_components.append(aradi.get_components_in_round(round_number)) - for round_number in range(2, 4): - middle_part_components.append(aradi.get_components_in_round(round_number)) - for round_number in range(4, 5): - bottom_part_components.append(aradi.get_components_in_round(round_number)) - top_part_components = list(itertools.chain(*top_part_components)) + for round_number in range(1): + top_part_components.append(chacha.get_components_in_round(round_number)) + for round_number in range(1, 3): + middle_part_components.append(chacha.get_components_in_round(round_number)) + for round_number in range(3, 6): + bottom_part_components.append(chacha.get_components_in_round(round_number)) + middle_part_components = list(itertools.chain(*middle_part_components)) bottom_part_components = list(itertools.chain(*bottom_part_components)) @@ -108,52 +111,51 @@ def test_differential_linear_trail_with_fixed_weight_3_rounds_speck(): plaintext = set_fixed_variables( component_id='plaintext', - constraint_type='not_equal', - bit_positions=range(32), - bit_values=[0] * 32 + constraint_type='equal', + bit_positions=range(512), + bit_values=integer_to_bit_list(0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000000000000000000000000, 512, 'big') ) - key = set_fixed_variables( - component_id='key', + cipher_output_5_24 = set_fixed_variables( + component_id='cipher_output_5_24', constraint_type='equal', - bit_positions=range(64), - bit_values=(0,) * 64 + bit_positions=range(512), + bit_values=integer_to_bit_list(0x00010000000100010000000100030003000000800000008000000000000001800000000000000001000000010000000201000101010000000000010103000101, 512, 'big') ) - modadd_2_7 = set_fixed_variables( - component_id='modadd_4_7', + modadd_3_15 = set_fixed_variables( + component_id=f'modadd_3_15', constraint_type='not_equal', - bit_positions=range(4), - bit_values=[0] * 4 + bit_positions=range(32), + bit_values=[0] * 32 ) - component_model_types = generate_component_model_types(aradi) + component_model_types = generate_component_model_types(chacha) update_component_model_types_for_truncated_components(component_model_types, middle_part_components) update_component_model_types_for_linear_components(component_model_types, bottom_part_components) - sat_heterogeneous_model = SatDifferentialLinearModel(aradi, component_model_types) + sat_heterogeneous_model = SatDifferentialLinearModel(chacha, component_model_types) trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight( - weight=4, fixed_values=[key, plaintext, modadd_2_7], solver_name="CADICAL_EXT", num_unknown_vars=31 + weight=5, fixed_values=[plaintext, modadd_3_15, cipher_output_5_24], solver_name="CADICAL_EXT", num_unknown_vars=511 ) - print(trail) assert trail["status"] == 'SATISFIABLE' + assert trail["total_weight"] <= 5 -def test_differential_linear_trail_with_fixed_weight_3_rounds_ascon(): - """Test for finding a differential-linear trail with fixed weight for 8 rounds of Speck.""" - aradi = GastonSboxPermutationTop(number_of_rounds=3) - import itertools +def test_differential_linear_trail_with_fixed_weight_4_rounds_aradi(): + """Test for finding a differential-linear trail with fixed weight for 4 rounds of Aradi block cipher.""" + aradi = AradiBlockCipherSBox(number_of_rounds=4) + import itertools top_part_components = [] middle_part_components = [] bottom_part_components = [] for round_number in range(1): top_part_components.append(aradi.get_components_in_round(round_number)) - for round_number in range(1, 2): + for round_number in range(1, 3): middle_part_components.append(aradi.get_components_in_round(round_number)) - for round_number in range(2, 3): + for round_number in range(3, 4): bottom_part_components.append(aradi.get_components_in_round(round_number)) - top_part_components = list(itertools.chain(*top_part_components)) middle_part_components = list(itertools.chain(*middle_part_components)) bottom_part_components = list(itertools.chain(*bottom_part_components)) @@ -162,17 +164,30 @@ def test_differential_linear_trail_with_fixed_weight_3_rounds_ascon(): plaintext = set_fixed_variables( component_id='plaintext', - constraint_type='not_equal', - bit_positions=range(640), - bit_values=[0] * 640 + constraint_type='equal', + bit_positions=range(128), + bit_values=integer_to_bit_list(0x00000000000080000000000000008000, 128, 'big') ) + cipher_output_3_86 = set_fixed_variables( + component_id='cipher_output_3_86', + constraint_type='equal', + bit_positions=range(128), + bit_values=integer_to_bit_list(0x90900120800000011010002000000000, 128, 'big') + ) - modadd_2_7 = set_fixed_variables( - component_id='sbox_2_88', + key = set_fixed_variables( + component_id='key', + constraint_type='equal', + bit_positions=range(256), + bit_values=[0] * 256 + ) + + sbox_4_8 = set_fixed_variables( + component_id=f'sbox_3_8', constraint_type='not_equal', - bit_positions=range(5), - bit_values=[0] * 5 + bit_positions=range(4), + bit_values=[0] * 4 ) component_model_types = generate_component_model_types(aradi) @@ -182,47 +197,28 @@ def test_differential_linear_trail_with_fixed_weight_3_rounds_ascon(): sat_heterogeneous_model = SatDifferentialLinearModel(aradi, component_model_types) trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight( - weight=4, fixed_values=[plaintext, modadd_2_7], solver_name="CADICAL_EXT", num_unknown_vars=639 + weight=10, fixed_values=[key, plaintext, sbox_4_8, cipher_output_3_86], solver_name="CADICAL_EXT", num_unknown_vars=128-1 ) - print(trail) assert trail["status"] == 'SATISFIABLE' + assert trail["total_weight"] <= 10 -def generate_uint32_array_from_hex(prefix, hex_string): - # Ensure the hex string is exactly 512 bits (128 hex characters) - if len(hex_string) < 128: - hex_string = hex_string.zfill(128) # Pad with leading zeros if necessary - - # Split the hex string into 32-bit chunks (8 hex characters each) - chunks = [hex_string[i:i + 8] for i in range(0, len(hex_string), 8)] - - # Convert each chunk to a 32-bit integer with '0x' format for C-like output - formatted_chunks = ["0x" + chunk.upper() for chunk in chunks] - - # Construct the C-style uint32_t array as a string - uint32_array = f"uint32_t {prefix}[16] = {{ " + ", ".join(formatted_chunks) + " };" +def test_differential_linear_trail_with_fixed_weight_4_rounds_chacha(): + """Test for finding a differential-linear trail with fixed weight for 4 rounds of ChaCha permutation.""" + chacha = ChachaPermutation(number_of_rounds=8) - return uint32_array - -def test_differential_linear_trail_with_fixed_weight_3_rounds_chacha(): - """Test for finding a differential-linear trail with fixed weight for 8 rounds of Speck.""" - nr = 6 - chacha = ChachaPermutation(number_of_rounds=nr) - #import ipdb; ipdb.set_trace() - #chacha.print() import itertools top_part_components = [] middle_part_components = [] bottom_part_components = [] - for round_number in range(1): + for round_number in range(2): top_part_components.append(chacha.get_components_in_round(round_number)) - for round_number in range(1, 3): + for round_number in range(2, 4): middle_part_components.append(chacha.get_components_in_round(round_number)) - for round_number in range(3, 6): + for round_number in range(4, 8): bottom_part_components.append(chacha.get_components_in_round(round_number)) - top_part_components = list(itertools.chain(*top_part_components)) middle_part_components = list(itertools.chain(*middle_part_components)) bottom_part_components = list(itertools.chain(*bottom_part_components)) @@ -232,20 +228,16 @@ def test_differential_linear_trail_with_fixed_weight_3_rounds_chacha(): plaintext = set_fixed_variables( component_id='plaintext', constraint_type='equal', - bit_positions=range(384), - bit_values=integer_to_bit_list(0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000000000000000000000000, 512, 'big') + bit_positions=range(512), + bit_values=integer_to_bit_list( + 0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000088088780, + 512, + 'big' + ) ) - cipher_output_5_24 = set_fixed_variables( - component_id='cipher_output_5_24', - constraint_type='equal', - bit_positions=range(384), - bit_values=integer_to_bit_list(0x00010000000100010000000100030003000000800000008000000000000001800000000000000001000000010000000201000101010000000000010103000101, 512, 'big') - ) - - - modadd_2_7 = set_fixed_variables( - component_id=f'modadd_3_15', + modadd_4_15 = set_fixed_variables( + component_id=f'modadd_4_15', constraint_type='not_equal', bit_positions=range(32), bit_values=[0] * 32 @@ -258,84 +250,66 @@ def test_differential_linear_trail_with_fixed_weight_3_rounds_chacha(): sat_heterogeneous_model = SatDifferentialLinearModel(chacha, component_model_types) trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight( - weight=5, fixed_values=[plaintext, modadd_2_7, cipher_output_5_24], solver_name="CADICAL_EXT", num_unknown_vars=511 + weight=32, fixed_values=[plaintext, modadd_4_15], solver_name="CADICAL_EXT", num_unknown_vars=511 ) - print(trail) - print(generate_uint32_array_from_hex("ID", trail["components_values"]["plaintext"]["value"])) - print(generate_uint32_array_from_hex("ODmask", trail["components_values"][f"cipher_output_{nr-1}_24"]["value"])) assert trail["status"] == 'SATISFIABLE' - assert trail["total_weight"] <= 5 + assert trail["total_weight"] <= 32 -def test_diff_lin_gaston(): +def test_diff_lin_chacha(): """ - # input_difference = 0x00000000000000000000000000000000000000000000000000000000000000000000000000000001 - # output_mask = 0x00000000000000000000000000000000000000000000000000000100000000000000002000000000 + This test is verifying experimentally the test test_differential_linear_trail_with_fixed_weight_3_rounds_chacha """ + input_difference = 0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000000000000000000000000 + output_mask = 0x00010000000100010000000100030003000000800000008000000000000001800000000000000001000000010000000201000101010000000000010103000101 + number_of_samples = 2 ** 12 + number_of_rounds = 6 + state_size = 512 + chacha = ChachaPermutation(number_of_rounds=number_of_rounds) + corr = differential_linear_checker_for_permutation( + chacha, input_difference, output_mask, number_of_samples, state_size + ) + import math + abs_corr = abs(corr) + assert abs(math.log(abs_corr, 2)) < 3 - input_difference = 0x0020000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 - output_mask = 0x0000000000000040000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +def test_diff_lin_speck(): + """ + This test is verifying experimentally the test test_differential_linear_trail_with_fixed_weight_6_rounds_speck + """ + input_difference = 0x02110a04 + output_mask = 0x02000201 number_of_samples = 2 ** 12 - start_building_time = time.time() - rng = np.random.default_rng() - input_difference_data = repeat_input_difference(input_difference, number_of_samples, 80) - end_building_time = time.time() - sat_time = end_building_time - start_building_time - print("Time in seconds", sat_time) - nr = 3 - gaston = GastonSboxPermutationTop(number_of_rounds=nr) - plaintext1 = rng.integers(low=0, high=256, size=(80, number_of_samples), dtype=np.uint8) - plaintext2 = plaintext1 ^ input_difference_data - start_building_time = time.time() - ciphertext1 = gaston.evaluate_vectorized([plaintext1]) - sat_time = end_building_time - start_building_time - print("Time in seconds", sat_time) - ciphertext2 = gaston.evaluate_vectorized([plaintext2]) - ciphertext3 = ciphertext1[0] ^ ciphertext2[0] - bit_positions_ciphertext = extract_bit_positions(output_mask) - ccc = extract_bits(ciphertext3.T, bit_positions_ciphertext) - print(ccc) - count = 0 - for i in range(number_of_samples): - c_xor = np.bitwise_xor.reduce(ccc.T[i]) - if c_xor == 0: - count += 1 - corr = 2*count/number_of_samples*1.0-1 + number_of_rounds = 6 + fixed_key = 0x0 + speck = SpeckBlockCipher(number_of_rounds=number_of_rounds) + block_size = speck.inputs_bit_size[0] + key_size = speck.inputs_bit_size[1] + corr = differential_linear_checker_for_block_cipher_single_key( + speck, input_difference, output_mask, number_of_samples, block_size, key_size, fixed_key + ) import math - print("Correlation:", corr, "Exponent of 2", math.log(abs(corr), 2)) + abs_corr = abs(corr) + assert abs(math.log(abs_corr, 2)) < 8 -def test_diff_lin_chacha(): +def test_diff_lin_aradi(): """ - # input_difference = 0x00000000000000000000000000000000000000000000000000000000000000000000000000000001 - # output_mask = 0x00000000000000000000000000000000000000000000000000000100000000000000002000000000 + This test is verifying experimentally the test test_differential_linear_trail_with_fixed_weight_4_rounds_aradi """ - - input_difference = 0x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000000000000000000000000 - output_mask = 0x00010000000100010000000100030003000000800000008000000000000001800000000000000001000000010000000201000101010000000000010103000101 + input_difference = 0x00000000000080000000000000008000 + output_mask = 0x90900120800000011010002000000000 number_of_samples = 2 ** 12 - start_building_time = time.time() - rng = np.random.default_rng() - input_difference_data = repeat_input_difference(input_difference, number_of_samples, 64) - end_building_time = time.time() - sat_time = end_building_time - start_building_time - nr = 6 - gaston = ChachaPermutation(number_of_rounds=nr) - plaintext1 = rng.integers(low=0, high=256, size=(64, number_of_samples), dtype=np.uint8) - plaintext2 = plaintext1 ^ input_difference_data - start_building_time = time.time() - ciphertext1 = gaston.evaluate_vectorized([plaintext1]) - sat_time = end_building_time - start_building_time - ciphertext2 = gaston.evaluate_vectorized([plaintext2]) - ciphertext3 = ciphertext1[0] ^ ciphertext2[0] - bit_positions_ciphertext = extract_bit_positions(output_mask) - ccc = extract_bits(ciphertext3.T, bit_positions_ciphertext) - count = 0 - for i in range(number_of_samples): - c_xor = np.bitwise_xor.reduce(ccc.T[i]) - if c_xor == 0: - count += 1 - corr = 2*count/number_of_samples*1.0-1 + number_of_rounds = 4 + fixed_key = 0x90900120800000011010002000000000 + speck = AradiBlockCipherSBox(number_of_rounds=number_of_rounds) + block_size = speck.inputs_bit_size[0] + key_size = speck.inputs_bit_size[1] + corr = differential_linear_checker_for_block_cipher_single_key( + speck, input_difference, output_mask, number_of_samples, block_size, key_size, fixed_key + ) import math - print("Correlation:", corr, "Exponent of 2", math.log(abs(corr), 2)) \ No newline at end of file + abs_corr = abs(corr) + print(corr, abs_corr, abs(math.log(abs_corr, 2))) + assert abs(math.log(abs_corr, 2)) < 8