diff --git a/.github/workflows/build-develop-image.yaml b/.github/workflows/build-develop-image.yaml new file mode 100644 index 00000000..31449ad0 --- /dev/null +++ b/.github/workflows/build-develop-image.yaml @@ -0,0 +1,60 @@ +name: Build and push image from develop +on: + pull_request: + types: [ closed ] + branches: + - main + +jobs: + build-image: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v3 + with: + persist-credentials: false + fetch-depth: 0 + + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v2 + + - name: Cache Docker layers + uses: actions/cache@v3 + with: + path: /tmp/.buildx-cache + key: ${{ runner.os }}-buildx-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-buildx- + + + - name: Login dockerhub + uses: docker/login-action@v3 + with: + username: ${{ secrets.DOCKER_REGISTRY_USER }} + password: ${{ secrets.DOCKER_REGISTRY_PASSWORD }} + + - name: Build & Push + uses: docker/build-push-action@v4 + id: built-image + with: + context: . + file: ./docker/Dockerfile + push: true + tags: tiicrc/claasp-lib:latest + cache-from: type=local,src=/tmp/.buildx-cache + cache-to: type=local,dest=/tmp/.buildx-cache-new,mode=max + + - name: Move cache + run: | + rm -rf /tmp/.buildx-cache + mv /tmp/.buildx-cache-new /tmp/.buildx-cache + + - name: Get current commit information + run: | + git clone ${{ secrets.DEPLOYMENT_REPOSITORY }} deployment-repo + git config --global user.name 'Github' + git config --global user.email ${{ secrets.DEPLOYMENT_REPOSITORY_EMAIL }} + cd deployment-repo && echo "Date: $(date) Commit: $(git rev-parse HEAD)" >> claasp-dev.log + git add claasp-dev.log + git commit -m "Updating deployment-repo from github" + git push origin master diff --git a/Makefile b/Makefile index 0076acb6..9e525fe5 100644 --- a/Makefile +++ b/Makefile @@ -18,14 +18,14 @@ all: install fi builddocker: - docker build -f docker/Dockerfile -t $(DOCKER_IMG_NAME) . + docker build -f docker/Dockerfile --target claasp-base -t $(DOCKER_IMG_NAME) . rundocker: builddocker docker run -i -p 8887:8887 --mount type=bind,source=`pwd`,target=/home/sage/tii-claasp -t $(DOCKER_IMG_NAME) \ sh -c "cd /home/sage/tii-claasp && make install && cd /home/sage/tii-claasp && exec /bin/bash" builddocker-m1: - docker build --build-arg="GUROBI_ARCH=armlinux64" -f docker/Dockerfile --platform linux/aarch64 -t $(DOCKER_IMG_NAME) . + docker build --build-arg="GUROBI_ARCH=armlinux64" -f docker/Dockerfile --platform linux/aarch64 --target claasp-base -t $(DOCKER_IMG_NAME) . rundocker-m1: builddocker-m1 docker run -i -p 8888:8888 --mount type=bind,source=`pwd`,target=/home/sage/tii-claasp -t $(DOCKER_IMG_NAME) \ diff --git a/claasp/cipher.py b/claasp/cipher.py index f2a433da..1d5fa216 100644 --- a/claasp/cipher.py +++ b/claasp/cipher.py @@ -1068,7 +1068,7 @@ def get_partial_cipher(self, start_round=None, end_round=None, keep_key_schedule end_round, keep_key_schedule) if start_round > 0: - for input_type in set(self.inputs) - {INPUT_KEY}: + for input_type in set([input for input in self.inputs if INPUT_KEY not in input]): removed_components_ids.append(input_type) input_index = partial_cipher.inputs.index(input_type) partial_cipher.inputs.pop(input_index) @@ -1145,8 +1145,8 @@ def cipher_partial_inverse(self, start_round=None, end_round=None, keep_key_sche partial_cipher_inverse = partial_cipher.cipher_inverse() key_schedule_component_ids = get_key_schedule_component_ids(partial_cipher_inverse) - key_schedule_components = [partial_cipher_inverse.get_component_from_id(id) for id in - key_schedule_component_ids[1:]] + key_schedule_components = [partial_cipher_inverse.get_component_from_id(id) for id in key_schedule_component_ids if + INPUT_KEY not in id] if not keep_key_schedule: for current_round in partial_cipher_inverse.rounds_as_list: diff --git a/claasp/cipher_modules/code_generator.py b/claasp/cipher_modules/code_generator.py index b15fc2b0..ca6bbfde 100644 --- a/claasp/cipher_modules/code_generator.py +++ b/claasp/cipher_modules/code_generator.py @@ -248,7 +248,6 @@ def generate_bit_based_vectorized_python_code_string(cipher, store_intermediate_ code.extend([f' {cipher.inputs[i]}=input[{i}]' for i in range(len(cipher.inputs))]) for component in cipher.get_all_components(): - start = time.time() params = prepare_input_bit_based_vectorized_python_code_string(component) component_types_allowed = ['constant', 'linear_layer', 'concatenate', 'mix_column', 'sbox', 'cipher_output', 'intermediate_output', 'fsr'] @@ -260,8 +259,6 @@ def generate_bit_based_vectorized_python_code_string(cipher, store_intermediate_ name = component.id if verbosity and component.type != 'constant': code.append(f' bit_vector_print_as_hex_values("{name}_output", {name})') - end=time.time() - print(f'{component.id} time = {end-start}') if store_intermediate_outputs: code.append(' return intermediateOutputs') elif CIPHER_INVERSE_SUFFIX in cipher.id: @@ -319,7 +316,6 @@ def generate_byte_based_vectorized_python_code_string(cipher, store_intermediate code.append(f' {cipher.inputs[i]}=input[{i}]') bit_sizes[cipher.inputs[i]] = cipher.inputs_bit_size[i] for component in cipher.get_all_components(): - start = time.time() params = prepare_input_byte_based_vectorized_python_code_string(bit_sizes, component) bit_sizes[component.id] = component.output_bit_size component_types_allowed = ['constant', 'linear_layer', 'concatenate', 'mix_column', @@ -335,8 +331,6 @@ def generate_byte_based_vectorized_python_code_string(cipher, store_intermediate if verbosity and component.type != 'constant': code.append(f' byte_vector_print_as_hex_values("{name}_input", {params})') code.append(f' byte_vector_print_as_hex_values("{name}_output", {name})') - end=time.time() - print(f'{component.id} time = {end-start}') if store_intermediate_outputs: code.append(' return intermediateOutputs') elif CIPHER_INVERSE_SUFFIX in cipher.id: @@ -648,7 +642,7 @@ def build_function_call(component): elif component.type == FSR: registers_info = component.description[0] bits_inside_word = component.description[1] - if len(component.description) is 2: + if len(component.description) == 2: number_of_clocks = 1 else: number_of_clocks = component.description[2] diff --git a/claasp/cipher_modules/evaluator.py b/claasp/cipher_modules/evaluator.py index 7c0b1814..e4e5a1be 100644 --- a/claasp/cipher_modules/evaluator.py +++ b/claasp/cipher_modules/evaluator.py @@ -26,7 +26,7 @@ def evaluate(cipher, cipher_input, intermediate_output=False, verbosity=False): python_code_string = code_generator.generate_python_code_string(cipher, verbosity) - + f_module = ModuleType("evaluate") exec(python_code_string, f_module.__dict__) diff --git a/claasp/cipher_modules/inverse_cipher.py b/claasp/cipher_modules/inverse_cipher.py index 70af71a2..5b07a564 100644 --- a/claasp/cipher_modules/inverse_cipher.py +++ b/claasp/cipher_modules/inverse_cipher.py @@ -17,7 +17,11 @@ def get_cipher_components(self): setattr(c, 'round', int(c.id.split("_")[-2])) # build input components for index, input_id in enumerate(self.inputs): - input_component = Component(input_id, "cipher_input", Input(0, [[]], [[]]), self.inputs_bit_size[index], [input_id]) + if INPUT_KEY in input_id: + input_component = Component(input_id, "cipher_input", Input(0, [[]], [[]]), self.inputs_bit_size[index], + [INPUT_KEY]) + else: + input_component = Component(input_id, "cipher_input", Input(0, [[]], [[]]), self.inputs_bit_size[index], [input_id]) setattr(input_component, 'round', -1) component_list.append(input_component) return component_list @@ -673,7 +677,7 @@ def _add_output_bit_equivalences(id, bit_positions, component, all_equivalent_bi flag_is_intersection_of_input_id_links_null, input_bit_positions = is_intersection_of_input_id_links_null( inverse_component, component) - if (component.id == INPUT_KEY) or (component.type == CONSTANT): + if (component.description == [INPUT_KEY]) or (component.type == CONSTANT): for i in range(component.output_bit_size): output_bit_name_updated = id + "_" + str(i) + "_output_updated" bit = { @@ -821,7 +825,7 @@ def component_inverse(component, available_bits, all_equivalent_bits, key_schedu component.output_bit_size, [component.id]) inverse_component.__class__ = cipher_output_component.CipherOutput setattr(inverse_component, "round", component.round) - elif component.type == CIPHER_INPUT and (component.id == INPUT_KEY or component.id == INPUT_TWEAK): + elif component.type == CIPHER_INPUT and (component.description == [INPUT_KEY] or component.id == INPUT_TWEAK): inverse_component = Component(component.id, CIPHER_INPUT, Input(0, [[]], [[]]), component.output_bit_size, [component.id]) @@ -833,7 +837,7 @@ def component_inverse(component, available_bits, all_equivalent_bits, key_schedu component, available_output_components, all_equivalent_bits, self) inverse_component = Component(component.id, INTERMEDIATE_OUTPUT, Input(component.output_bit_size, input_id_links, input_bit_positions), - component.output_bit_size, [component.id]) + component.output_bit_size, component.description) inverse_component.__class__ = intermediate_output_component.IntermediateOutput setattr(inverse_component, "round", component.round) update_output_bits(inverse_component, self, all_equivalent_bits, available_bits) @@ -941,7 +945,7 @@ def get_component_from_id(component_id, self): def get_key_schedule_component_ids(self): - key_schedule_component_ids = [INPUT_KEY] + key_schedule_component_ids = [input for input in self.inputs if INPUT_KEY in input] component_list = self.get_all_components() for c in component_list: flag_belong_to_key_schedule = True @@ -1248,7 +1252,7 @@ def sort_cipher_graph(cipher): def remove_components_from_rounds(cipher, start_round, end_round, keep_key_schedule): list_of_rounds = cipher.rounds_as_list[:start_round] + cipher.rounds_as_list[end_round + 1:] key_schedule_component_ids = get_key_schedule_component_ids(cipher) - key_schedule_components = [cipher.get_component_from_id(id) for id in key_schedule_component_ids[1:]] + key_schedule_components = [cipher.get_component_from_id(id) for id in key_schedule_component_ids if INPUT_KEY not in id] if not keep_key_schedule: for current_round in cipher.rounds_as_list: 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 5da86d79..93d85e4d 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 @@ -16,14 +16,16 @@ # **************************************************************************** import time + +from claasp.cipher_modules.inverse_cipher import get_key_schedule_component_ids from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT from claasp.cipher_modules.models.milp.milp_model import verbose_print from claasp.cipher_modules.models.milp.milp_models.milp_bitwise_deterministic_truncated_xor_differential_model import \ MilpBitwiseDeterministicTruncatedXorDifferentialModel 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 -from claasp.cipher_modules.models.milp.utils import utils as milp_utils +from claasp.name_mappings import CIPHER_OUTPUT, INPUT_KEY +from claasp.cipher_modules.models.milp.utils import utils as milp_utils, milp_truncated_utils class MilpBitwiseImpossibleXorDifferentialModel(MilpBitwiseDeterministicTruncatedXorDifferentialModel): @@ -155,7 +157,7 @@ def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_compone sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2) sage: milp = MilpBitwiseImpossibleXorDifferentialModel(speck) sage: milp.init_model_in_sage_milp_class() - sage: milp.add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_components(["rot_1_4"]) + sage: milp.add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_components(["rot_1_6"]) """ @@ -167,8 +169,7 @@ def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_compone if component_id_list == None: return self.add_constraints_to_build_in_sage_milp_class(fixed_variables=fixed_variables) - - assert set(component_id_list) <= set(self._cipher.get_all_components_ids()) + assert set(component_id_list) <= set(self._cipher.get_all_components_ids()) - set(get_key_schedule_component_ids(self._cipher)) middle_round_numbers = [self._cipher.get_round_from_component_id(id) for id in component_id_list] @@ -186,16 +187,16 @@ def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_compone self._incompatible_components = component_id_list backward_last_round_components = set(backward_cipher._rounds.round_at(self._cipher.number_of_rounds - 1 - middle_round_number).get_components_ids() + [backward_cipher.get_all_components_ids()[-1]]) - self._backward_cipher = backward_cipher.add_suffix_to_components(MILP_BACKWARD_SUFFIX, backward_last_round_components) - + input_id_links_of_chosen_components = [_ for c in [backward_cipher.get_component_from_id(id) for id in component_id_list] for _ in c.input_id_links] + round_input_id_links_of_chosen_components = [backward_cipher.get_round_from_component_id(id) for id in input_id_links_of_chosen_components] + links_round = [_ for r in round_input_id_links_of_chosen_components for _ in backward_cipher._rounds.round_at(r).get_components_ids()] + self._backward_cipher = backward_cipher.add_suffix_to_components(MILP_BACKWARD_SUFFIX, backward_last_round_components | set(links_round)) self.build_bitwise_impossible_xor_differential_trail_model(fixed_variables) - for index, constraint in enumerate(self._model_constraints): - mip.add_constraint(constraint) # finding incompatibility - constraints = [] + incompatibility_constraints = [] for id in component_id_list: forward_component = self._cipher.get_component_from_id(id) @@ -205,24 +206,28 @@ def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_compone backward_component = self._backward_cipher.get_component_from_id(id + f"{MILP_BACKWARD_SUFFIX}") input_ids, _ = backward_component._get_input_output_variables() - backward_vars = [x_class[id] for id in input_ids] + backward_vars = [x_class[id] for id in input_ids if INPUT_KEY not in id] inconsistent_vars = [x[f"{forward_component.id}_inconsistent_{_}"] for _ in range(output_bit_size)] - constraints.extend([sum(inconsistent_vars) == 1]) + # for multiple input components such as the XOR, ensures compatibility occurs on the correct branch + for index, input_id in enumerate(["_".join(i.split("_")[:-1]) if MILP_BACKWARD_SUFFIX in i else i for i in backward_component.input_id_links]): + if INPUT_KEY not in input_id and self._cipher.get_component_from_id(input_id).input_id_links == [id]: + backward_vars = [x_class[f'{input_id}_{pos}'] for pos in backward_component.input_bit_positions[index]] + + incompatibility_constraints.extend([sum(inconsistent_vars) == 1]) for inconsistent_index in range(output_bit_size): incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] == 1] - constraints.extend( + incompatibility_constraints.extend( milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, self._model.get_max(x_class) * 2)) - for constraint in constraints: - mip.add_constraint(constraint) - _, forward_output_id_tuples = forward_component._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])) + optimization_constraint = [p["number_of_unknown_patterns"] == sum( + x[output_msb] for output_msb in [id[0] for id in forward_output_id_tuples])] + for constraint in self._model_constraints + incompatibility_constraints + optimization_constraint: + mip.add_constraint(constraint) - def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixed_variables=[]): + def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixed_variables=[], include_all_components=False): """ Take the constraints contained in self._model_constraints and add them to the build-in sage class. @@ -232,6 +237,8 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe - ``model_type`` -- **string**; the model to solve - ``fixed_variables`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard format + - ``include_all_components`` -- **boolean** (default: `False`); when set to `True`, every component output can be a source + of incompatibility; otherwise, only round outputs are considered .. SEEALSO:: @@ -244,7 +251,7 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2) sage: milp = MilpBitwiseImpossibleXorDifferentialModel(speck) sage: milp.init_model_in_sage_milp_class() - sage: milp.aadd_constraints_to_build_fully_automatic_model_in_sage_milp_class() + sage: milp.add_constraints_to_build_fully_automatic_model_in_sage_milp_class() """ verbose_print(MILP_BUILDING_MESSAGE) @@ -262,33 +269,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_round_outputs = [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}] - - for backward_round_output in backward_round_outputs: - output_bit_size = backward_round_output.output_bit_size - _, output_ids = backward_round_output._get_input_output_variables() - - backward_vars = [x_class[id] for id in output_ids] - forward_vars = [x_class["_".join(id.split("_")[:-2] + [id.split("_")[-1]])] for id in output_ids] - inconsistent_vars = [x[f"{backward_round_output.id}_inconsistent_{_}"] for _ in range(output_bit_size)] - all_inconsistent_vars += inconsistent_vars - - for inconsistent_index in range(output_bit_size): - incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] == 1] - constraints.extend( - milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, - self._model.get_max(x_class) * 2)) - - 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])) @@ -414,7 +400,7 @@ def find_one_bitwise_impossible_xor_differential_trail_with_chosen_incompatible_ return solution - def find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic_model(self, fixed_values=[], + def find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic_model(self, fixed_values=[], include_all_components=False, solver_name=SOLVER_DEFAULT, external_solver_name=None): """ Returns one bitwise impossible XOR differential trail. @@ -425,6 +411,8 @@ def find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic_mode - ``middle_round`` -- **integer**; the round number for which the incompatibility occurs - ``fixed_values`` -- *list of dict*, the variables to be fixed in standard format (see :py:meth:`~GenericModel.set_fixed_variables`) + - ``include_all_components`` -- **boolean** (default: `False`); when set to `True`, every component output can be a source + of incompatibility; otherwise, only round outputs are considered - ``external_solver_name`` -- **string** (default: None); if specified, the library will write the internal Sagemath MILP model as a .lp file and solve it outside of Sagemath, using the external solver. EXAMPLES:: @@ -457,7 +445,7 @@ def find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic_mode verbose_print(f"Solver used : {solver_name} (Choose Gurobi for Better performance)") mip = self._model mip.set_objective(None) - self.add_constraints_to_build_fully_automatic_model_in_sage_milp_class(fixed_values) + self.add_constraints_to_build_fully_automatic_model_in_sage_milp_class(fixed_variables=fixed_values, include_all_components=include_all_components) end = time.time() building_time = end - start solution = self.solve(MILP_BITWISE_IMPOSSIBLE_AUTO, solver_name, external_solver_name) 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..4856ba6e 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) @@ -38,7 +40,7 @@ class MilpWordwiseDeterministicTruncatedXorDifferentialModel(MilpModel): def __init__(self, cipher, n_window_heuristic=None): super().__init__(cipher, n_window_heuristic) self._trunc_wordvar = None - self._word_size = 1 + self._word_size = 4 if self._cipher.is_spn(): for component in self._cipher.get_all_components(): if SBOX in component.type: @@ -156,7 +158,7 @@ def build_wordwise_deterministic_truncated_xor_differential_trail_model(self, fi operation = component.description[0] operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'XOR'] - if component.type in component_types and (component.type != WORD_OPERATION or operation in operation_types): + if component.type in component_types or operation in operation_types: variables, constraints = component.milp_wordwise_deterministic_truncated_xor_differential_constraints(self) else: print(f'{component.id} not yet implemented') 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 b4fd9349..7bc4f7b8 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 @@ -16,6 +16,8 @@ # **************************************************************************** import time + +from claasp.cipher_modules.inverse_cipher import get_key_schedule_component_ids from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT from claasp.cipher_modules.models.milp.milp_model import verbose_print from claasp.cipher_modules.models.milp.milp_models.milp_wordwise_deterministic_truncated_xor_differential_model import MilpWordwiseDeterministicTruncatedXorDifferentialModel @@ -26,8 +28,8 @@ MILP_WORDWISE_IMPOSSIBLE, MILP_BACKWARD_SUFFIX, MILP_BUILDING_MESSAGE 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 -from claasp.cipher_modules.models.milp.utils import utils as milp_utils +from claasp.name_mappings import CIPHER_OUTPUT, INPUT_KEY +from claasp.cipher_modules.models.milp.utils import utils as milp_utils, milp_truncated_utils class MilpWordwiseImpossibleXorDifferentialModel(MilpWordwiseDeterministicTruncatedXorDifferentialModel): @@ -129,13 +131,16 @@ def add_constraints_to_build_in_sage_milp_class(self, middle_round=None, fixed_b constraints.extend([sum(inconsistent_vars) == 1]) for inconsistent_index in range(output_size): - incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] - constraints.extend(milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, self._model.get_max(x_class) * 2)) + incompatibility_constraints = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] + dummy = x[f'dummy_incompatibility_{x[forward_vars[inconsistent_index]]}_or_{x[backward_vars[inconsistent_index]]}_is_0'] + incompatibility_constraints += [forward_vars[inconsistent_index] <= self._model.get_max(x_class) * (1 - dummy)] + incompatibility_constraints += [backward_vars[inconsistent_index] <= self._model.get_max(x_class) * dummy] + constraints.extend(milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraints, self._model.get_max(x_class) * 2)) # output is fixed cipher_output = [c for c in self._cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] _, cipher_output_ids = cipher_output._get_wordwise_input_output_linked_class(self) - constraints.extend([x_class[id] <= 1 for id in cipher_output_ids] + [sum([x_class[id] for id in cipher_output_ids]) >= 1]) + constraints.extend([x_class[id] <= 2 for id in cipher_output_ids] + [sum([x_class[id] for id in cipher_output_ids]) >= 1]) for constraint in constraints: mip.add_constraint(constraint) @@ -146,7 +151,7 @@ def add_constraints_to_build_in_sage_milp_class(self, middle_round=None, fixed_b p["number_of_unknown_patterns"] == sum(x[output_msb] for output_msb in [id[0] for id in forward_output_id_tuple])) - def add_constraints_to_build_in_sage_milp_class_with_fixed_components(self, component_id_list=None, fixed_bits=[], fixed_words=[]): + def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_components(self, component_id_list=None, fixed_bits=[], fixed_words=[]): """ Take the constraints contained in self._model_constraints and add them to the build-in sage class. @@ -182,7 +187,7 @@ def add_constraints_to_build_in_sage_milp_class_with_fixed_components(self, comp if component_id_list == None: return self.add_constraints_to_build_in_sage_milp_class(fixed_bits=fixed_bits, fixed_words=fixed_words) - assert set(component_id_list) <= set(self._cipher.get_all_components_ids()) + assert set(component_id_list) <= set(self._cipher.get_all_components_ids()) - set(get_key_schedule_component_ids(self._cipher)) middle_round_numbers = [self._cipher.get_round_from_component_id(id) for id in component_id_list] @@ -199,15 +204,22 @@ def add_constraints_to_build_in_sage_milp_class_with_fixed_components(self, comp self._incompatible_components = component_id_list backward_last_round_components = set(backward_cipher._rounds.round_at(self._cipher.number_of_rounds - 1 - middle_round_number).get_components_ids() + [backward_cipher.get_all_components_ids()[-1]]) - self._backward_cipher = backward_cipher.add_suffix_to_components(MILP_BACKWARD_SUFFIX, backward_last_round_components) + input_id_links_of_chosen_components = [_ for c in + [backward_cipher.get_component_from_id(id) for id in component_id_list] + for _ in c.input_id_links] + round_input_id_links_of_chosen_components = [backward_cipher.get_round_from_component_id(id) for id in + input_id_links_of_chosen_components] + links_round = [_ for r in round_input_id_links_of_chosen_components for _ in + backward_cipher._rounds.round_at(r).get_components_ids()] + self._backward_cipher = backward_cipher.add_suffix_to_components(MILP_BACKWARD_SUFFIX, + backward_last_round_components | set( + links_round)) self.build_wordwise_impossible_xor_differential_trail_model(fixed_bits, fixed_words) - for index, constraint in enumerate(self._model_constraints): - mip.add_constraint(constraint) # finding incompatibility - constraints = [] + incompatibility_constraints = [] for id in component_id_list: forward_component = self._cipher.get_component_from_id(id) @@ -217,29 +229,33 @@ def add_constraints_to_build_in_sage_milp_class_with_fixed_components(self, comp backward_component = self._backward_cipher.get_component_from_id(id + f"{MILP_BACKWARD_SUFFIX}") input_ids, _ = backward_component._get_wordwise_input_output_linked_class(self) - backward_vars = [x_class[id] for id in input_ids] + backward_vars = [x_class[id] for id in input_ids if INPUT_KEY not in id] inconsistent_vars = [x[f"{forward_component.id}_inconsistent_{_}"] for _ in range(output_size)] - constraints.extend([sum(inconsistent_vars) == 1]) + # for multiple input components such as the XOR, ensures compatibility occurs on the correct branch + for index, input_id in enumerate(["_".join(i.split("_")[:-1]) if MILP_BACKWARD_SUFFIX in i else i for i in + backward_component.input_id_links]): + if INPUT_KEY not in input_id and self._cipher.get_component_from_id(input_id).input_id_links == [id]: + backward_vars = [x_class[f'{input_id}_{pos}'] for pos in + backward_component.input_bit_positions[index]] + + incompatibility_constraints.extend([sum(inconsistent_vars) == 1]) for inconsistent_index in range(output_size): incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] - constraints.extend(milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, self._model.get_max(x_class) * 2)) + incompatibility_constraints.extend(milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, self._model.get_max(x_class) * 2)) # output is fixed cipher_output = [c for c in self._cipher.get_all_components() if c.type == CIPHER_OUTPUT][0] _, cipher_output_ids = cipher_output._get_wordwise_input_output_linked_class(self) - constraints.extend([x_class[id] <= 1 for id in cipher_output_ids] + [sum([x_class[id] for id in cipher_output_ids]) >= 1]) - - for constraint in constraints: - mip.add_constraint(constraint) + incompatibility_constraints.extend([x_class[id] <= 1 for id in cipher_output_ids] + [sum([x_class[id] for id in cipher_output_ids]) >= 1]) # unknown patterns are tuples of the form (1,x) (i.e pattern = 2 or 3) _, forward_output_id_tuple = forward_component._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])) - + optimization_constraint = [p["number_of_unknown_patterns"] == sum(x[output_msb] for output_msb in [id[0] for id in forward_output_id_tuple])] - def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixed_bits=[], fixed_words=[]): + for constraint in self._model_constraints + incompatibility_constraints + optimization_constraint: + mip.add_constraint(constraint) + def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixed_bits=[], fixed_words=[], include_all_components=False): """ Take the constraints contained in self._model_constraints and add them to the build-in sage class. @@ -248,6 +264,8 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe - ``model_type`` -- **string**; the model to solve - ``fixed_bits`` -- *list of dict*, the bit variables to be fixed in standard format - ``fixed_words`` -- *list of dict*, the word variables to be fixed in standard format + - ``include_all_components`` -- **boolean** (default: `False`); when set to `True`, every component output can be a source + of incompatibility; otherwise, only round outputs are considered .. SEEALSO:: @@ -279,36 +297,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_round_outputs = [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}] - - for backward_round_output in backward_round_outputs: - output_size = backward_round_output.output_bit_size // self.word_size - _, output_ids = backward_round_output._get_wordwise_input_output_linked_class(self) - - backward_vars = [x_class[id] for id in output_ids] - forward_vars = [x_class["_".join(id.split("_")[:-4] + id.split("_")[-3:])] for id in output_ids] - inconsistent_vars = [x[f"{backward_round_output.id}_inconsistent_{_}"] for _ in range(output_size)] - all_inconsistent_vars += inconsistent_vars - - for inconsistent_index in range(output_size): - incompatibility_constraint = [forward_vars[inconsistent_index] + backward_vars[inconsistent_index] <= 2] - constraints.extend(milp_utils.milp_if_then(inconsistent_vars[inconsistent_index], incompatibility_constraint, self._model.get_max(x_class) * 2)) + 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])) @@ -376,7 +375,8 @@ def find_one_wordwise_impossible_xor_differential_trail_with_chosen_components(s verbose_print(f"Solver used : {solver_name} (Choose Gurobi for Better performance)") mip = self._model mip.set_objective(None) - self.add_constraints_to_build_in_sage_milp_class_with_fixed_components(component_id_list, fixed_bits, fixed_words) + self.add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_components(component_id_list, + fixed_bits, fixed_words) end = time.time() building_time = end - start solution = self.solve(MILP_WORDWISE_IMPOSSIBLE, solver_name, external_solver_name) @@ -384,7 +384,7 @@ def find_one_wordwise_impossible_xor_differential_trail_with_chosen_components(s return solution - def find_one_wordwise_impossible_xor_differential_trail_with_fully_automatic_model(self, fixed_bits=[], fixed_words=[], solver_name=SOLVER_DEFAULT, external_solver_name=None): + def find_one_wordwise_impossible_xor_differential_trail_with_fully_automatic_model(self, fixed_bits=[], fixed_words=[], include_all_components=False, solver_name=SOLVER_DEFAULT, external_solver_name=None): """ Returns one wordwise impossible XOR differential trail. @@ -393,6 +393,8 @@ def find_one_wordwise_impossible_xor_differential_trail_with_fully_automatic_mod - ``solver_name`` -- *str*, the solver to call - ``fixed_bits`` -- *list of dict*, the bit variables to be fixed in standard format - ``fixed_words`` -- *list of dict*, the word variables to be fixed in standard format + - ``include_all_components`` -- **boolean** (default: `False`); when set to `True`, every component output can be a source + of incompatibility; otherwise, only round outputs are considered - ``external_solver_name`` -- **string** (default: None); if specified, the library will write the internal Sagemath MILP model as a .lp file and solve it outside of Sagemath, using the external solver. EXAMPLE:: @@ -410,7 +412,7 @@ def find_one_wordwise_impossible_xor_differential_trail_with_fully_automatic_mod verbose_print(f"Solver used : {solver_name} (Choose Gurobi for Better performance)") mip = self._model mip.set_objective(None) - self.add_constraints_to_build_fully_automatic_model_in_sage_milp_class(fixed_bits, fixed_words) + self.add_constraints_to_build_fully_automatic_model_in_sage_milp_class(fixed_bits, fixed_words, include_all_components=include_all_components) end = time.time() building_time = end - start solution = self.solve(MILP_WORDWISE_IMPOSSIBLE_AUTO, solver_name, external_solver_name) 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..0a0b6e83 --- /dev/null +++ b/claasp/cipher_modules/models/milp/utils/milp_truncated_utils.py @@ -0,0 +1,122 @@ +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() + forward_vars = [x_class["_".join(id.split("_")[:-2] + [id.split("_")[-1]])] for id in output_ids] + else: + output_size = backward_component.output_bit_size // model.word_size + input_ids, output_ids = backward_component._get_wordwise_input_output_linked_class(model) + forward_vars = [x_class["_".join(id.split("_")[:-4] + id.split("_")[-3:])] for id in output_ids] + + 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] + + 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: + constraints.extend( + _generate_value_exclusion_constraints(milp_model, model_variables, fixed_variable, prefix, suffix)) + + return constraints + + +def _generate_value_exclusion_constraints(milp_model, model_variables, fixed_variable, prefix, suffix): + constraints = [] + 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 cd8ce989..d5463f2e 100644 --- a/claasp/cipher_modules/models/milp/utils/utils.py +++ b/claasp/cipher_modules/models/milp/utils/utils.py @@ -69,6 +69,7 @@ def _parse_external_solver_output(model, model_type, solver_name, solver_process status = 'UNSATISFIABLE' objective_value = None + components_values = None if solver_specs['unsat_condition'] not in str(solver_process): status = 'SATISFIABLE' @@ -645,42 +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 ### -------------------------Solution parser ------------------------- ### def _get_component_values_for_impossible_models(model, objective_variables, components_variables): @@ -703,7 +668,7 @@ def _get_component_values_for_impossible_models(model, objective_variables, comp for id in model._incompatible_components: backward_incompatible_component = model._backward_cipher.get_component_from_id(id + f"{MILP_BACKWARD_SUFFIX}") input_ids, _ = backward_incompatible_component._get_input_output_variables() - renamed_input_ids = set(["_".join(id.split("_")[:-2]) for id in input_ids]) + renamed_input_ids = set(["_".join(id.split("_")[:-2]) if MILP_BACKWARD_SUFFIX in id else "_".join(id.split("_")[:-1]) for id in input_ids]) indices += sorted(indices + [full_cipher_components.index(c) for c in renamed_input_ids]) updated_cipher_components = full_cipher_components[:indices[0]] + [ diff --git a/claasp/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/sat/cms_models/cms_bitwise_deterministic_truncated_xor_differential_model.py similarity index 89% rename from claasp/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model.py rename to claasp/cipher_modules/models/sat/cms_models/cms_bitwise_deterministic_truncated_xor_differential_model.py index 1b3e422f..3d63170d 100644 --- a/claasp/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model.py +++ b/claasp/cipher_modules/models/sat/cms_models/cms_bitwise_deterministic_truncated_xor_differential_model.py @@ -43,15 +43,18 @@ For any further information, visit `CryptoMiniSat - XOR clauses `_. """ -from claasp.cipher_modules.models.sat.sat_models.sat_deterministic_truncated_xor_differential_model import \ - SatDeterministicTruncatedXorDifferentialModel -class CmsSatDeterministicTruncatedXorDifferentialModel(SatDeterministicTruncatedXorDifferentialModel): +from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import \ + SatBitwiseDeterministicTruncatedXorDifferentialModel + + +class CmsSatDeterministicTruncatedXorDifferentialModel(SatBitwiseDeterministicTruncatedXorDifferentialModel): def __init__(self, cipher, window_size_weight_pr_vars=-1, counter='sequential', compact=False): super().__init__(cipher, window_size_weight_pr_vars, counter, compact) + print("\n*** WARNING ***\n" "At the best of the authors knowldege, deterministic truncated XOR differential model " "cannot take any advantage of CryptoMiniSat. Therefore, the implementation is the same " diff --git a/claasp/cipher_modules/models/sat/sat_model.py b/claasp/cipher_modules/models/sat/sat_model.py index 270c3eb0..c32fbd2e 100644 --- a/claasp/cipher_modules/models/sat/sat_model.py +++ b/claasp/cipher_modules/models/sat/sat_model.py @@ -153,6 +153,22 @@ def _get_cipher_inputs_components_solutions(self, out_suffix, variable2value): return components_solutions + def _get_cipher_inputs_components_solutions_double_ids(self, variable2value): + components_solutions = {} + for cipher_input, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size): + values = [] + for i in range(bit_size): + value = 0 + if f'{cipher_input}_{i}_0' in variable2value: + value ^= variable2value[f'{cipher_input}_{i}_0'] << 1 + 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).replace('2', '?').replace('3', '?')) + components_solutions[cipher_input] = component_solution + + return components_solutions + def _get_component_hex_value(self, component, out_suffix, variable2value): output_bit_size = component.output_bit_size value = 0 @@ -165,6 +181,20 @@ def _get_component_hex_value(self, component, out_suffix, variable2value): return hex_value + def _get_component_value_double_ids(self, component, variable2value): + output_bit_size = component.output_bit_size + values = [] + for i in range(output_bit_size): + variable_value = 0 + if f'{component.id}_{i}_0' in variable2value: + variable_value ^= variable2value[f'{component.id}_{i}_0'] << 1 + if f'{component.id}_{i}_1' in variable2value: + variable_value ^= variable2value[f'{component.id}_{i}_1'] + values.append(f'{variable_value}') + value = ''.join(values).replace('2', '?').replace('3', '?') + + return value + def _get_solver_solution_parsed(self, variable2number, values): variable2value = {} for i, variable in enumerate(variable2number): diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model.py new file mode 100644 index 00000000..dd8c86b4 --- /dev/null +++ b/claasp/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model.py @@ -0,0 +1,284 @@ + +# **************************************************************************** +# Copyright 2023 Technology Innovation Institute +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . +# **************************************************************************** + + +import time + +from claasp.cipher_modules.models.sat.sat_model import SatModel +from claasp.cipher_modules.models.utils import set_component_solution +from claasp.name_mappings import (CIPHER_OUTPUT, CONSTANT, DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, + INTERMEDIATE_OUTPUT, INPUT_PLAINTEXT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION) + + +class SatBitwiseDeterministicTruncatedXorDifferentialModel(SatModel): + def __init__(self, cipher, window_size_weight_pr_vars=-1, counter='sequential', compact=False): + super().__init__(cipher, window_size_weight_pr_vars, counter, compact) + + def build_bitwise_deterministic_truncated_xor_differential_trail_model(self, number_of_unknown_variables=None, fixed_variables=[]): + """ + Build the model for the search of deterministic truncated XOR DIFFERENTIAL trails. + + INPUT: + + - ``number_of_unknown_variables`` -- **int** (default: None); the number + of unknown variables that we want to have in the trail + - ``fixed_variables`` -- **list** (default: `[]`); the variables to be + fixed in standard format + + .. SEEALSO:: + + :py:meth:`~cipher_modules.models.utils.set_fixed_variables` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=22) + sage: sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: sat.build_bitwise_deterministic_truncated_xor_differential_trail_model() + ... + """ + variables = [] + constraints = self.fix_variables_value_constraints(fixed_variables) + self._variables_list = [] + self._model_constraints = constraints + component_types = (CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION) + operation_types = ('AND', 'MODADD', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'XOR') + + for component in self._cipher.get_all_components(): + operation = component.description[0] + if component.type in component_types and (component.type != WORD_OPERATION or operation in operation_types): + variables, constraints = component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + else: + print(f'{component.id} not yet implemented') + + self._variables_list.extend(variables) + self._model_constraints.extend(constraints) + + if number_of_unknown_variables is not None: + variables, constraints = self.weight_constraints(number_of_unknown_variables) + self._variables_list.extend(variables) + self._model_constraints.extend(constraints) + + def fix_variables_value_constraints(self, fixed_variables=[]): + """ + Return constraints for fixed variables + + Return lists of variables and clauses for fixing variables in bitwise + deterministic truncated XOR differential model. + + .. SEEALSO:: + + :py:meth:`~cipher_modules.models.utils.set_fixed_variables` + + INPUT: + + - ``fixed_variables`` -- **list** (default: `[]`); variables in default format + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: fixed_variables = [{ + ....: 'component_id': 'plaintext', + ....: 'constraint_type': 'equal', + ....: 'bit_positions': [0, 1, 2, 3], + ....: 'bit_values': [1, 0, 1, 1] + ....: }, { + ....: 'component_id': 'ciphertext', + ....: 'constraint_type': 'not_equal', + ....: 'bit_positions': [0, 1, 2, 3], + ....: 'bit_values': [2, 1, 1, 0] + ....: }] + sage: sat.fix_variables_value_constraints(fixed_variables) + ['-plaintext_0_0', + 'plaintext_0_1', + '-plaintext_1_0', + '-plaintext_1_1', + '-plaintext_2_0', + 'plaintext_2_1', + '-plaintext_3_0', + 'plaintext_3_1', + '-ciphertext_0_0 ciphertext_1_0 -ciphertext_1_1 ciphertext_2_0 -ciphertext_2_1 ciphertext_3_0 ciphertext_3_1'] + """ + constraints = [] + for variable in fixed_variables: + component_id = variable['component_id'] + is_equal = (variable['constraint_type'] == 'equal') + bit_positions = variable['bit_positions'] + bit_values = variable['bit_values'] + variables_ids = [] + for position, value in zip(bit_positions, bit_values): + false_sign = '-' * is_equal + true_sign = '-' * (not is_equal) + if value == 0: + variables_ids.append(f'{false_sign}{component_id}_{position}_0') + variables_ids.append(f'{false_sign}{component_id}_{position}_1') + elif value == 1: + variables_ids.append(f'{false_sign}{component_id}_{position}_0') + variables_ids.append(f'{true_sign}{component_id}_{position}_1') + elif value == 2: + variables_ids.append(f'{true_sign}{component_id}_{position}_0') + if is_equal: + constraints.extend(variables_ids) + else: + constraints.append(' '.join(variables_ids)) + + return constraints + + def find_one_bitwise_deterministic_truncated_xor_differential_trail(self, fixed_values=[], + solver_name='cryptominisat'): + """ + Returns one deterministic truncated XOR differential trail. + + INPUTS: + + - ``fixed_values`` -- *list of dict*, the variables to be fixed in + standard format (see :py:meth:`~GenericModel.set_fixed_variables`) + - ``solver_name`` -- *str*, the solver to call + + EXAMPLE:: + + sage: from claasp.cipher_modules.models.utils import integer_to_bit_list, set_fixed_variables + 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=2) + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: M = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: plaintext = set_fixed_variables(component_id='plaintext', constraint_type='equal', bit_positions=range(32), bit_values=[0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) + sage: key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=[0]*64) + sage: trail = M.find_one_bitwise_deterministic_truncated_xor_differential_trail(fixed_values=[plaintext, key]) + ... + + sage: from claasp.cipher_modules.models.utils import integer_to_bit_list, set_fixed_variables + 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=3) + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: M = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: plaintext = set_fixed_variables(component_id='plaintext', constraint_type='equal', bit_positions=range(32), bit_values=[0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) + sage: key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=[0]*64) + sage: out = set_fixed_variables(component_id='cipher_output_2_12', constraint_type='equal', bit_positions=range(32), bit_values=[2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2]) + sage: trail = M.find_one_bitwise_deterministic_truncated_xor_differential_trail(fixed_values=[plaintext, key, out]) # doctest: +SKIP + ... + + sage: from claasp.cipher_modules.models.utils import integer_to_bit_list, set_fixed_variables + sage: from claasp.ciphers.block_ciphers.present_block_cipher import PresentBlockCipher + sage: present = PresentBlockCipher(number_of_rounds=1) + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(present) + sage: key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(80), bit_values=[0]*80) + sage: plaintext = set_fixed_variables(component_id='plaintext', constraint_type='equal', bit_positions=range(64), bit_values=[2,0,0,0] + [1,0,0,1] + [0,0,0,1] + [1,0,0,0] + [0] * 48) + sage: trail = sat.find_one_bitwise_deterministic_truncated_xor_differential_trail(fixed_values=[plaintext, key]) # doctest: +SKIP + ... + + """ + start_building_time = time.time() + self.build_bitwise_deterministic_truncated_xor_differential_trail_model(fixed_variables=fixed_values) + end_building_time = time.time() + solution = self.solve(DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, solver_name=solver_name) + solution['building_time_seconds'] = end_building_time - start_building_time + + return solution + + def find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential_trail(self, fixed_values=[], solver_name='cryptominisat'): + """ + Return the solution representing a differential trail with the lowest number of unknown variables. + + INPUTS: + + - ``fixed_values`` -- *list of dict*, the variables to be fixed in + standard format (see :py:meth:`~GenericModel.set_fixed_variables`) + - ``solver_name`` -- *str*, the solver to call + + EXAMPLE:: + + sage: from claasp.cipher_modules.models.utils import get_single_key_scenario_format_for_fixed_values + 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=2) + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: S = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: trail = S.find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential_trail(get_single_key_scenario_format_for_fixed_values(speck)) + sage: trail['status'] + 'SATISFIABLE' + """ + current_unknowns_count = 1 + start_building_time = time.time() + self.build_bitwise_deterministic_truncated_xor_differential_trail_model( + number_of_unknown_variables=current_unknowns_count, fixed_variables=fixed_values) + end_building_time = time.time() + solution = self.solve(DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, solver_name=solver_name) + solution['building_time_seconds'] = end_building_time - start_building_time + total_time = solution['solving_time_seconds'] + max_memory = solution['memory_megabytes'] + while solution['status'] != 'SATISFIABLE': + current_unknowns_count += 1 + start_building_time = time.time() + self.build_bitwise_deterministic_truncated_xor_differential_trail_model( + number_of_unknown_variables=current_unknowns_count, fixed_variables=fixed_values) + end_building_time = time.time() + solution = self.solve(DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, solver_name=solver_name) + solution['building_time_seconds'] = end_building_time - start_building_time + total_time += solution['solving_time_seconds'] + max_memory = max((max_memory, solution['memory_megabytes'])) + solution['solving_time_seconds'] = total_time + solution['memory_megabytes'] = max_memory + + return solution + + def weight_constraints(self, number_of_unknown_variables): + """ + Return lists of variables and constraints that fix the number of unknown + variables of the input and the output of the trail to a specific value. + + INPUT: + + - ``number_of_unknown_variables`` -- **int**; the number of the unknown variables + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sage: sat.build_bitwise_deterministic_truncated_xor_differential_trail_model() + sage: sat.weight_constraints(4) + (['dummy_hw_0_0_0', + 'dummy_hw_0_0_1', + 'dummy_hw_0_0_2', + ... + '-dummy_hw_0_61_3 dummy_hw_0_62_3', + '-cipher_output_2_12_30_0 -dummy_hw_0_61_3', + '-cipher_output_2_12_31_0 -dummy_hw_0_62_3']) + """ + cipher_output_id = self._cipher.get_all_components_ids()[-1] + set_to_be_minimized = [f"{INPUT_PLAINTEXT}_{i}_0" + for i in range(self._cipher.inputs_bit_size[self._cipher.inputs.index(INPUT_PLAINTEXT)])] + set_to_be_minimized.extend([bit_id for bit_id in self._variables_list + if bit_id.startswith(cipher_output_id) and bit_id.endswith("_0")]) + + return self._counter(set_to_be_minimized, number_of_unknown_variables) + + def _parse_solver_output(self, variable2value): + components_solutions = self._get_cipher_inputs_components_solutions_double_ids(variable2value) + for component in self._cipher.get_all_components(): + value = self._get_component_value_double_ids(component, variable2value) + component_solution = set_component_solution(value) + components_solutions[f'{component.id}'] = component_solution + + return components_solutions, None diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model.py deleted file mode 100644 index 6299d1c4..00000000 --- a/claasp/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model.py +++ /dev/null @@ -1,66 +0,0 @@ - -# **************************************************************************** -# Copyright 2023 Technology Innovation Institute -# -# This program is free software: you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . -# **************************************************************************** - - -from claasp.cipher_modules.models.sat.sat_model import SatModel -from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, WORD_OPERATION) - - -class SatDeterministicTruncatedXorDifferentialModel(SatModel): - def __init__(self, cipher, window_size_weight_pr_vars=-1, - counter='sequential', compact=False): - super().__init__(cipher, window_size_weight_pr_vars, counter, compact) - - def build_deterministic_truncated_xor_differential_trail_model(self, fixed_variables=[]): - """ - Build the model for the search of deterministic truncated XOR DIFFERENTIAL trails. - - INPUT: - - - ``fixed_variables`` -- **list** (default: `[]`); the variables to be fixed in standard format - - .. SEEALSO:: - - :py:meth:`~cipher_modules.models.utils.set_fixed_variables` - - EXAMPLES:: - - sage: from claasp.cipher_modules.models.sat.sat_models.sat_deterministic_truncated_xor_differential_model import SatDeterministicTruncatedXorDifferentialModel - sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher - sage: speck = SpeckBlockCipher(number_of_rounds=22) - sage: sat = SatDeterministicTruncatedXorDifferentialModel(speck) - sage: sat.build_deterministic_truncated_xor_differential_trail_model() - ... - """ - variables = [] - constraints = self.fix_variables_value_constraints(fixed_variables) - self._variables_list = [] - self._model_constraints = constraints - - for component in self._cipher.get_all_components(): - component_types = [CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, WORD_OPERATION] - operation = component.description[0] - operation_types = ["ROTATE", "SHIFT"] - - if component.type in component_types and (component.type != WORD_OPERATION or operation in operation_types): - variables, constraints = component.sat_deterministic_truncated_xor_differential_trail_constraints() - else: - print(f'{component.id} not yet implemented') - - self._variables_list.extend(variables) - self._model_constraints.extend(constraints) diff --git a/claasp/cipher_modules/models/sat/utils/utils.py b/claasp/cipher_modules/models/sat/utils/utils.py index f5973a26..861df1ca 100644 --- a/claasp/cipher_modules/models/sat/utils/utils.py +++ b/claasp/cipher_modules/models/sat/utils/utils.py @@ -563,6 +563,138 @@ def cnf_and_linear(mask_in_0, mask_in_1, mask_out, hw): f'-{mask_out} {hw}', f'{mask_out} -{hw}') + +def 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'] + """ + return [f'{result[0]} -{variable_0[0]}', + f'{result[0]} -{variable_1[0]}', + f'{variable_0[0]} {variable_1[0]} -{result[0]}', + f'{variable_0[1]} {variable_1[1]} {result[0]} -{result[1]}', + f'{variable_0[1]} {result[0]} {result[1]} -{variable_1[1]}', + f'{variable_1[1]} {result[0]} {result[1]} -{variable_0[1]}', + f'{result[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}'] + + +def 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. + + .. SEEALSO:: + + :py:meth:`~cipher_modules.models.sat.utils.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'] + """ + model = cnf_xor_truncated(results[0], variables[0], variables[1]) + for i in range(1, len(results)): + model.extend(cnf_xor_truncated(results[i], results[i - 1], variables[i + 1])) + + return model + + +def modadd_truncated_lsb(result, variable_0, variable_1, next_carry): + return [f'{next_carry[0]} -{next_carry[1]}', + f'{next_carry[0]} -{variable_1[1]}', + f'{next_carry[0]} -{result[0]}', + f'{next_carry[0]} -{result[1]}', + f'{result[0]} -{variable_0[0]}', + f'{result[0]} -{variable_1[0]}', + f'{variable_0[0]} {variable_1[0]} -{result[0]}', + f'{variable_0[1]} {variable_1[1]} {result[0]} -{next_carry[0]}', + f'{variable_0[1]} {result[0]} {result[1]} -{variable_1[1]}', + f'{variable_1[1]} {result[0]} {result[1]} -{variable_0[1]}', + f'{result[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}'] + + +def modadd_truncated(result, variable_0, variable_1, carry, next_carry): + return [f'{next_carry[0]} -{next_carry[1]}', + f'{next_carry[0]} -{variable_1[1]}', + f'{next_carry[0]} -{result[0]}', + f'{next_carry[0]} -{result[1]}', + f'{result[0]} -{carry[0]}', + f'{result[0]} -{carry[1]}', + f'{result[0]} -{variable_0[0]}', + f'{result[0]} -{variable_1[0]}', + f'{variable_0[1]} {variable_1[1]} {result[0]} -{next_carry[0]}', + f'{variable_0[1]} {result[0]} {result[1]} -{variable_1[1]}', + f'{variable_1[1]} {result[0]} {result[1]} -{variable_0[1]}', + f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{result[0]}', + f'{result[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}'] + + +def modadd_truncated_msb(result, variable_0, variable_1, carry): + return [f'{result[0]} -{carry[0]}', + f'{result[0]} -{carry[1]}', + f'{result[0]} -{variable_0[0]}', + f'{result[0]} -{variable_1[0]}', + f'{variable_0[1]} {variable_1[1]} {result[0]} -{result[1]}', + f'{variable_0[1]} {result[0]} {result[1]} -{variable_1[1]}', + f'{variable_1[1]} {result[0]} {result[1]} -{variable_0[1]}', + f'{carry[0]} {carry[1]} {variable_0[0]} {variable_1[0]} -{result[0]}', + f'{result[0]} -{variable_0[1]} -{variable_1[1]} -{result[1]}'] + + # ---------------------------- # # - Running SAT solver - # # ---------------------------- # diff --git a/claasp/cipher_modules/neural_network_tests.py b/claasp/cipher_modules/neural_network_tests.py index 40ecbf35..c3a50abc 100644 --- a/claasp/cipher_modules/neural_network_tests.py +++ b/claasp/cipher_modules/neural_network_tests.py @@ -313,7 +313,7 @@ def train_neural_distinguisher(cipher, data_generator, starting_round, neural_ne bs = 5000 x, y = data_generator(samples=training_samples, nr=starting_round) x_eval, y_eval = data_generator(samples=testing_samples, nr=starting_round) - h = neural_network.fit(x, y, epochs=num_epochs, batch_size=bs, validation_data=(x_eval, y_eval)) + h = neural_network.fit(x, y, epochs=int(num_epochs), batch_size=bs, validation_data=(x_eval, y_eval)) acc = np.max(h.history["val_acc"]) print(f'Validation accuracy at {starting_round} rounds :{acc}') return acc diff --git a/claasp/ciphers/block_ciphers/qarmav2_block_cipher.py b/claasp/ciphers/block_ciphers/qarmav2_block_cipher.py index 64eaa1fa..8961a5d8 100644 --- a/claasp/ciphers/block_ciphers/qarmav2_block_cipher.py +++ b/claasp/ciphers/block_ciphers/qarmav2_block_cipher.py @@ -37,7 +37,7 @@ class QARMAv2BlockCipher(Cipher): EXAMPLES:: sage: from claasp.ciphers.block_ciphers.qarmav2_block_cipher import QARMAv2BlockCipher - sage: qarmav2 = QARMAv2BlockCipher(number_of_rounds = 4) + sage: qarmav2 = QARMAv2WordwiseBlockCipher(number_of_rounds = 4) sage: key = 0x0123456789abcdeffedcba9876543210 sage: tweak = 0x7e5c3a18f6d4b2901eb852fc9630da74 sage: plaintext = 0x0000000000000000 @@ -69,6 +69,7 @@ def __init__(self, number_of_rounds=10, number_of_layers=1, key_bit_size=128, tw self.NUM_SBOXES = self.LAYER_SBOXES * number_of_layers self.NUM_ROWS = 4 self.ROW_SIZE = 4 + self.number_of_layers = number_of_layers super().__init__(family_name="qarmav2_block_cipher", cipher_type="block_cipher", @@ -133,331 +134,373 @@ def __init__(self, number_of_rounds=10, number_of_layers=1, key_bit_size=128, tw lfsr_matrix[44][0] = 1 lfsr_matrix[63][0] = 1 - inverse_state_permutation = [] + state_permutation = [] for i in self.state_shuffle: - inverse_state_permutation += list(range(4*i, 4*i + 4)) - state_permutation = [inverse_state_permutation.index(i) for i in range(self.LAYER_BLOCK_SIZE)] + state_permutation += list(range(4*i, 4*i + 4)) + inverse_state_permutation = [state_permutation.index(i) for i in range(self.LAYER_BLOCK_SIZE)] tweak_permutation = [] - inverse_permutation=[] + inverse_permutation = [] for i in self.tweak_permutations[number_of_layers]: inverse_permutation += list(range(4*i, 4*i + 4)) direct_permutation = [inverse_permutation.index(i) for i in range(self.TWEAK_BLOCK_SIZE)] - tweak_permutation = [inverse_permutation, direct_permutation] + tweak_permutation = [direct_permutation, inverse_permutation] + self.exchange_rows_shuffle = list(range(16, 24)) + list(range(8, 16)) + list(range(8)) + list(range(24, 32)) + exchange_rows_permutation = list(range(64,96)) + list(range(32, 64)) + list(range(32)) + list(range(96, 128)) - - #First round different from others + self.add_round() - + + #Key initialization + key_state = self.key_initialization(key_bit_size) + #Tweak initialization - tweak_0 = self.add_permutation_component([INPUT_TWEAK], - [[i for i in range(self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - tweak_permutation[1]) - for j in range(1, number_of_rounds-1): - perm_tweak = self.add_permutation_component([tweak_0.id], - [[i for i in range(self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - tweak_permutation[1]) - tweak_0 = perm_tweak - if tweak_bit_size == self.TWEAK_BLOCK_SIZE: - tweak_1 = self.add_permutation_component([INPUT_TWEAK], - [[i for i in range(self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - tweak_permutation[1]) - else: - tweak_1 = self.add_permutation_component([INPUT_TWEAK], - [[i for i in range(self.TWEAK_BLOCK_SIZE, 2*self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - [i for i in range(self.TWEAK_BLOCK_SIZE)]) - tweak_state = [tweak_0, tweak_1] + tweak_state = self.tweak_initialization(tweak_permutation, tweak_bit_size) + + #Round constants initialization + constants_states = self.constants_initialization() + + #First round different from others + state = self.first_round_start(key_state) + #Direct encryption + for round_number in range(1, number_of_rounds+1): + state, tweak_state = self.direct_round(state, key_state, tweak_state, tweak_permutation, constants_states, round_number) + self.add_round() + + #Reflector + state, key_state = self.reflector(state, key_state, tweak_state, constants_states) + + #Inverse encryption + for round_number in list(range(1, number_of_rounds+1))[::-1]: + self.add_round() + state, tweak_state = self.inverse_round(state, key_state, tweak_state, tweak_permutation, constants_states, round_number) + + #Last round different from others + state = self.last_round_end(state, key_state, tweak_state, constants_states) + + def key_initialization(self, key_bit_size): #Key initialization - key_0 = self.add_permutation_component([INPUT_KEY], - [[i for i in range(self.KEY_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE, - [i for i in range(self.KEY_BLOCK_SIZE)]) + key_0 = [[INPUT_KEY], [list(range(self.KEY_BLOCK_SIZE))]] if key_bit_size == 2*self.KEY_BLOCK_SIZE: - key_1 = self.add_permutation_component([INPUT_KEY], - [[i for i in range(self.KEY_BLOCK_SIZE, 2*self.KEY_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE, - [i for i in range(self.KEY_BLOCK_SIZE)]) + key_1 = [[INPUT_KEY], [list(range(self.KEY_BLOCK_SIZE, 2*self.KEY_BLOCK_SIZE))]] elif key_bit_size == self.KEY_BLOCK_SIZE: key_1 = key_0 else: - key_1 = self.add_permutation_component([INPUT_KEY, majority_function(INPUT_KEY).id], - [[i for i in range(self.KEY_BLOCK_SIZE, 3*self.KEY_BLOCK_SIZE//2)], [i for i in range(self.KEY_BLOCK_SIZE//2)]], - self.KEY_BLOCK_SIZE, - [i for i in range(self.KEY_BLOCK_SIZE)]) + key_1 = [[INPUT_KEY, majority_function(INPUT_KEY).id], + [list(range(self.KEY_BLOCK_SIZE, 3*self.KEY_BLOCK_SIZE//2)), list(range(self.KEY_BLOCK_SIZE//2))]] key_state = [key_0, key_1] + return key_state + + def tweak_initialization(self, tweak_permutation, tweak_bit_size): + #Tweak initialization + tweak_0 = [[INPUT_TWEAK],[tweak_permutation[1]]] + for j in range(1, self.NROUNDS-1): + perm_tweak = [tweak_0[1][0][i] for i in tweak_permutation[1]] + tweak_0[1][0] = perm_tweak + if tweak_bit_size == self.TWEAK_BLOCK_SIZE: + tweak_1 = [[INPUT_TWEAK], [tweak_permutation[1]]] + else: + tweak_1 = [[INPUT_TWEAK], [list(range(self.TWEAK_BLOCK_SIZE, 2*self.TWEAK_BLOCK_SIZE))]] + tweak_state = [tweak_0, tweak_1] + + return tweak_state + + def constants_initialization(self): #Round constants initialization - round_constant = [self.add_constant_component(self.LAYER_BLOCK_SIZE, 0)] - if number_of_layers == 2: - round_constant.append(self.add_constant_component(self.LAYER_BLOCK_SIZE, 0)) - round_constant_0 = self.add_constant_component(self.LAYER_BLOCK_SIZE, 0x243F6A8885A308D3) + round_constant = [self.add_constant_component(self.LAYER_BLOCK_SIZE, 0).id] + if self.number_of_layers == 2: + round_constant.append(self.add_constant_component(self.LAYER_BLOCK_SIZE, 0).id) + round_constant_0 = self.add_constant_component(self.LAYER_BLOCK_SIZE, 0x243F6A8885A308D3).id round_constant.append(round_constant_0) - if number_of_layers == 2: - round_constant_1 = self.update_constants(round_constant_0) + if self.number_of_layers == 2: + round_constant_1 = self.update_single_constant(round_constant_0) round_constant.append(round_constant_1) - for i in range(2, number_of_rounds): - round_constant_0 = self.update_constants(round_constant[-1]) + for i in range(2, self.NROUNDS): + round_constant_0 = self.update_single_constant(round_constant[-1]) round_constant.append(round_constant_0) - if number_of_layers == 2: - round_constant_1 = self.update_constants(round_constant_0) + if self.number_of_layers == 2: + round_constant_1 = self.update_single_constant(round_constant_0) round_constant.append(round_constant_1) - first_round_add_round_key = self.add_XOR_component([key_state[0].id, INPUT_PLAINTEXT], - [[i for i in range(self.KEY_BLOCK_SIZE)], - list(range(self.CIPHER_BLOCK_SIZE))[::-1]], - self.CIPHER_BLOCK_SIZE) - - first_round_sboxes = [] - for sb in range(self.NUM_SBOXES): - sbox = self.add_SBOX_component([first_round_add_round_key.id], - [[i for i in range(4*sb, 4*sb + 4)]], - self.SBOX_BIT_SIZE, - self.sbox) - first_round_sboxes.append(sbox) - - round_output = self.add_permutation_component([first_round_sboxes[i].id for i in range(self.NUM_SBOXES)], - [[i for i in range(self.SBOX_BIT_SIZE)] for j in range(self.NUM_SBOXES)], - self.CIPHER_BLOCK_SIZE, - [i for i in range(self.CIPHER_BLOCK_SIZE)]) - - #Direct encryption - for round_number in range(1, number_of_rounds+1): - - round_key_shuffle = [] - for l in range(number_of_layers): - xor = self.add_XOR_component([round_output.id, - key_state[round_number%2].id, - tweak_state[round_number%2].id, - round_constant[(round_number - 1)*number_of_layers + l].id], - [[i for i in range(64*l, 64*l + 64)], - [i for i in range(64*l, 64*l + 64)], - [i for i in range(64*l, 64*l + 64)], - [i for i in range(64)]], - self.LAYER_BLOCK_SIZE) - round_key_shuffle.append(xor) - - tweak_state[round_number%2] = self.add_permutation_component([tweak_state[round_number%2].id], - [[i for i in range(self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - tweak_permutation[round_number%2]) - - round_state_shuffle = [] - for l in range(number_of_layers): - shuffled_state = self.add_permutation_component([round_key_shuffle[l].id], - [[i for i in range(self.LAYER_BLOCK_SIZE)]], - self.LAYER_BLOCK_SIZE, - state_permutation) - round_state_shuffle.append(shuffled_state) - - round_state_rotate = [] - for l in range(number_of_layers): - for col in range(4): - round_state_rotate.extend(self.M_function([round_state_shuffle[l].id for i in range(4)], [[i for i in range(4*col+16*j, 4*col+16*j+4)] for j in range(4)])) - - round_sboxes = [] - for l in range(number_of_layers): - for sb in range(self.LAYER_SBOXES): - sbox = self.add_SBOX_component([round_state_rotate[int(sb/4)+4*(sb%4)+16*l]], - [[i for i in range(4)]], - self.SBOX_BIT_SIZE, - self.sbox) - round_sboxes.append(sbox) - - if number_of_layers == 2 and (number_of_rounds - round_number)%2 == 0: - exchanging_rows = self.add_permutation_component([round_sboxes[i].id for i in range(self.NUM_SBOXES)], - [[i for i in range(self.SBOX_BIT_SIZE)] for j in range(self.NUM_SBOXES)], - self.CIPHER_BLOCK_SIZE, - exchange_rows_permutation) - - round_output = self.add_round_output_component([exchanging_rows.id], - [[i for i in range(self.CIPHER_BLOCK_SIZE)]], - self.CIPHER_BLOCK_SIZE) + return round_constant + + def first_round_start(self, key_state): + #First round different from others + id_links = [key_state[0][0]+[INPUT_PLAINTEXT]] + bit_positions = [[key_state[0][1][0], list(range(64*self.number_of_layers))[::-1]]] + masked_state = self.state_masking(id_links, bit_positions) + + id_links = [masked_state for _ in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES)] + sboxed_state = self.state_sboxing(id_links, bit_positions, self.sbox) + + return sboxed_state + + def direct_round(self, state, key_state, tweak_state, tweak_permutation, constants_states, round_number): + #Direct encryption + if round_number != 1: + if len(key_state[round_number%2][0]) == 1: + id_links = [[state, + key_state[round_number%2][0][0], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//16]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4*i, 4*i + 4)), + key_state[round_number%2][1][0][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*i:4*i + 4], + list(range(4*(i % 16), 4*(i % 16) + 4))] for i in range(self.NUM_SBOXES)] else: - round_output = self.add_round_output_component([round_sboxes[i].id for i in range(self.NUM_SBOXES)], - [[i for i in range(self.SBOX_BIT_SIZE)] for j in range(self.NUM_SBOXES)], - self.CIPHER_BLOCK_SIZE) - - self.add_round() - + id_links = [[state, + key_state[round_number%2][0][0], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//64]] for i in range(self.NUM_SBOXES//2)] + id_links.extend([[state, + key_state[round_number%2][0][1], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//64]] for i in range(self.NUM_SBOXES//2, self.NUM_SBOXES)]) + bit_positions = [[list(range(4*i, 4*i + 4)), + key_state[round_number%2][1][0][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*i:4*i + 4], + list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES//2)] + bit_positions.extend([[list(range(4*(i + 16), 4*(i + 16) + 4)), + key_state[round_number%2][1][1][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*(i + 16):4*(i + 16) + 4], + list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES//2)]) + else: + if len(key_state[round_number%2][0]) == 1: + id_links = [[state[i], + key_state[round_number%2][0][0], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//16]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4)), + key_state[round_number%2][1][0][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*i:4*i + 4], + list(range(4*(i % 16), 4*(i % 16) + 4))] for i in range(self.NUM_SBOXES)] + else: + id_links = [[state[i], + key_state[round_number%2][0][0], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//64]] for i in range(self.NUM_SBOXES//2)] + id_links.extend([[state[i], + key_state[round_number%2][0][1], + tweak_state[round_number%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//64]] for i in range(self.NUM_SBOXES//2, self.NUM_SBOXES)]) + bit_positions = [[list(range(4)), + key_state[round_number%2][1][0][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*i:4*i + 4], + list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES//2)] + bit_positions.extend([[list(range(4)), + key_state[round_number%2][1][1][4*i:4*i + 4], + tweak_state[round_number%2][1][0][4*(i + 16):4*(i + 16) + 4], + list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES//2)]) + masked_state = self.state_masking(id_links, bit_positions) + + bit_positions = tweak_state[round_number%2][1][0] + tweak_shuffle = tweak_permutation[round_number%2] + tweak_state[round_number%2][1][0] = self.tweak_update(bit_positions, tweak_shuffle) + + shuffled_state = [masked_state[i] for i in self.state_shuffle] + if self.number_of_layers == 2: + shuffled_state += [masked_state[16 + i] for i in self.state_shuffle] + + id_links = shuffled_state + rotated_state = self.state_rotation(id_links) + + id_links = [[rotated_state[(4*i + (i//4)%4)%16 + 16*(i//16)]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4))] for _ in range(self.NUM_SBOXES)] + sboxed_state = self.state_sboxing(id_links, bit_positions, self.sbox) + + if self.number_of_layers == 2 and (self.NROUNDS - round_number)%2 == 0: + round_output = self.add_round_output_component([sboxed_state[i] for i in self.exchange_rows_shuffle], + [list(range(4)) for _ in range(self.NUM_SBOXES)], + self.CIPHER_BLOCK_SIZE).id + else: + round_output = self.add_round_output_component(sboxed_state, + [list(range(4)) for _ in range(self.NUM_SBOXES)], + self.CIPHER_BLOCK_SIZE).id + + return round_output, tweak_state + + def reflector(self, state, key_state, tweak_state, constants_states): #Reflector new_keys = self.o_function(key_state) key_state = new_keys W = self.o_function(new_keys) - alpha_0 = self.add_constant_component(self.LAYER_BLOCK_SIZE, 0x13198A2E03707344) - alpha = [alpha_0] - if number_of_layers == 2: - alpha_1 = self.update_constants(alpha[0]) - alpha.append(alpha_1) - beta_0 = self.update_constants(alpha[-1]) - beta = [beta_0] - if number_of_layers == 2: - beta_1 = self.update_constants(beta_0) - beta.append(beta_1) - if number_of_layers == 2: - key_state[0] = self.add_XOR_component([key_state[0].id, alpha[0].id, alpha[1].id], - [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE) - key_state[1] = self.add_XOR_component([key_state[1].id, beta[0].id, beta[1].id], - [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE) + alpha, beta = self.constants_update() + + key_state = self.key_update(key_state) + + id_links = [[state, W[(self.NROUNDS + 1)%2][0][0]] for _ in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4*self.state_shuffle[i%16] + 64*(i//16), 4*self.state_shuffle[i%16] + 4 + 64*(i//16))), list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES)] + masked_state = self.state_masking(id_links, bit_positions) + + id_links = masked_state + rotated_state = self.state_rotation(id_links) + + id_links = [[rotated_state[((i//4)%4 + 4*i)%16 + 16*(i//16)], W[(self.NROUNDS)%2][0][0]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4)), list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES)] + masked_state = self.state_masking(id_links, bit_positions) + + round_output = self.add_round_output_component([masked_state[self.state_shuffle.index(i%16) + 16*(i//16)] for i in range(self.NUM_SBOXES)], + [list(range(4)) for i in range(self.NUM_SBOXES)], + self.CIPHER_BLOCK_SIZE).id + + return round_output, key_state + + def inverse_round(self, state, key_state, tweak_state, tweak_permutation, constants_states, round_number): + #Inverse encryption + if self.number_of_layers == 2 and (self.NROUNDS - round_number)%2 == 0: + exchanging_rows = self.exchange_rows_shuffle else: - key_state[0] = self.add_XOR_component([key_state[0].id, alpha[0].id], - [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE) - key_state[1] = self.add_XOR_component([key_state[1].id, beta[0].id], - [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.LAYER_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE) - + exchanging_rows = list(range(self.NUM_SBOXES)) + + id_links = [[state] for _ in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4*exchanging_rows[i], 4*exchanging_rows[i] + 4))] for i in range(self.NUM_SBOXES)] + sboxed_state = self.state_sboxing(id_links, bit_positions, self.inverse_sbox) - round_state_shuffle = [] - for l in range(number_of_layers): - shuffled_state = self.add_permutation_component([round_output.id], - [[i for i in range(64*l, 64*l + 64)]], - self.LAYER_BLOCK_SIZE, - state_permutation) - mixed_shuffled_state = self.add_XOR_component([shuffled_state.id, W[(number_of_rounds + 1)%2].id], - [[i for i in range(self.LAYER_BLOCK_SIZE)], [i for i in range(64*l, 64*l + 64)]], - self.LAYER_BLOCK_SIZE) - round_state_shuffle.append(mixed_shuffled_state) - - round_state_rotate = [] - for l in range(number_of_layers): - for col in range(4): - round_state_rotate.extend(self.M_function([round_state_shuffle[l].id for i in range(4)], [[i for i in range(4*col+16*j, 4*col+16*j+4)] for j in range(4)])) - - central_keyed_state = [] - for l in range(number_of_layers): - for w in range(16): - central_xor = self.add_XOR_component([round_state_rotate[int(w/4)+4*(w%4)+16*l], W[(number_of_rounds)%2].id], - [[i for i in range(4)], [i for i in range(64*l + 4*w, 64*l + 4*w + 4)]], - self.WORD_SIZE) - central_keyed_state.append(central_xor) - - central_shuffled_state = [] - for l in range(number_of_layers): - shuffled_state = self.add_permutation_component([central_keyed_state[16*l + i].id for i in range(16)], - [[i for i in range(4)] for j in range(16)], - self.LAYER_BLOCK_SIZE, - inverse_state_permutation) - central_shuffled_state.append(shuffled_state) + id_links = sboxed_state + rotated_state = self.state_rotation(id_links) + + if round_number == 1: + id_links = [[rotated_state[(4*self.state_shuffle.index(i%16) + (self.state_shuffle.index(i%16)//4)%4)%16 + 16*(i//16)], + key_state[(round_number + 1)%2][0][0], + INPUT_TWEAK, + constants_states[i//16]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4)), + key_state[(round_number + 1)%2][1][0][4*i:4*i + 4], + list(range(4*i, 4*i + 4)), + list(range(4*(i%16), 4*(i%16) + 4))] for i in range(self.NUM_SBOXES)] + masked_state = self.state_masking(id_links, bit_positions) + else: + id_links = [[rotated_state[(4*self.state_shuffle.index(i%16) + (self.state_shuffle.index(i%16)//4)%4)%16 + 16*(i//16)], + key_state[(round_number + 1)%2][0][0], + tweak_state[(round_number + 1)%2][0][0], + constants_states[(round_number - 1)*self.number_of_layers + i//16]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4)), + key_state[(round_number + 1)%2][1][0][4*i:4*i + 4], + tweak_state[(round_number + 1)%2][1][0][4*i:4*i + 4], + list(range(4*(i%16), 4*(i%16) + 4))] for i in range(self.NUM_SBOXES)] + masked_state = self.state_masking(id_links, bit_positions) - round_output = self.add_round_output_component([central_shuffled_state[i].id for i in range(number_of_layers)], - [[i for i in range(self.LAYER_BLOCK_SIZE)] for j in range(number_of_layers)], - self.CIPHER_BLOCK_SIZE) - - #Inverse encryption - for round_number in list(range(1, number_of_rounds+1))[::-1]: - - if number_of_layers == 2 and (number_of_rounds - round_number)%2 == 0: - exchanging_rows = self.add_permutation_component([round_output.id], - [[i for i in range(self.CIPHER_BLOCK_SIZE)]], - self.CIPHER_BLOCK_SIZE, - exchange_rows_permutation) - else: - exchanging_rows = round_output - - round_sboxes = [] - for sb in range(self.NUM_SBOXES): - sbox = self.add_SBOX_component([exchanging_rows.id], - [[i for i in range(4*sb, 4*sb + 4)]], - self.SBOX_BIT_SIZE, - self.inverse_sbox) - round_sboxes.append(sbox) - - round_state_rotate = [] - for l in range(number_of_layers): - for col in range(4): - round_state_rotate.extend(self.M_function([round_sboxes[col+4*i+16*l].id for i in range(4)], [[i for i in range(4)] for j in range(4)])) - - round_state_shuffle = [] - for l in range(number_of_layers): - shuffled_state = self.add_permutation_component([round_state_rotate[int(i/4)+4*(i%4)+16*l] for i in range(16)], - [[i for i in range(4)] for j in range(16)], - self.LAYER_BLOCK_SIZE, - inverse_state_permutation) - round_state_shuffle.append(shuffled_state) - - round_key_shuffle = [] - if round_number == 1: - for l in range(number_of_layers): - xor = self.add_XOR_component([round_state_shuffle[l].id, - key_state[(round_number + 1)%2].id, - INPUT_TWEAK, - round_constant[(round_number - 1)*number_of_layers + l].id], - [[i for i in range(self.LAYER_BLOCK_SIZE)], - [i for i in range(64*l, 64*l + 64)], - [i for i in range((self.LAYER_BLOCK_SIZE)*l, (self.LAYER_BLOCK_SIZE)*(l+1))], - [i for i in range(64)]], - self.LAYER_BLOCK_SIZE) - round_key_shuffle.append(xor) - else: - for l in range(number_of_layers): - xor = self.add_XOR_component([round_state_shuffle[l].id, - key_state[(round_number + 1)%2].id, - tweak_state[(round_number + 1)%2].id, - round_constant[(round_number - 1)*number_of_layers + l].id], - [[i for i in range(self.LAYER_BLOCK_SIZE)], - [i for i in range(64*l, 64*l + 64)], - [i for i in range(64*l, 64*l + 64)], - [i for i in range(64)]], - self.LAYER_BLOCK_SIZE) - round_key_shuffle.append(xor) - - tweak_state[(round_number + 1)%2] = self.add_permutation_component([tweak_state[(round_number + 1)%2].id], - [[i for i in range(self.TWEAK_BLOCK_SIZE)]], - self.TWEAK_BLOCK_SIZE, - tweak_permutation[(round_number + 1)%2]) - if round_number != 1: - round_output = self.add_round_output_component([round_key_shuffle[i].id for i in range(number_of_layers)], - [[i for i in range(self.LAYER_BLOCK_SIZE)] for j in range(number_of_layers)], - self.CIPHER_BLOCK_SIZE) + bit_positions = tweak_state[(round_number + 1)%2][1][0] + tweak_shuffle = tweak_permutation[(round_number + 1)%2] + tweak_state[(round_number + 1)%2][1][0] = self.tweak_update(bit_positions, tweak_shuffle) + + if round_number != 1: + round_output = self.add_round_output_component(masked_state, + [list(range(4)) for i in range(self.NUM_SBOXES)], + self.CIPHER_BLOCK_SIZE).id - self.add_round() - else: - round_output = self.add_permutation_component([round_key_shuffle[i].id for i in range(number_of_layers)], - [[i for i in range(self.LAYER_BLOCK_SIZE)] for j in range(number_of_layers)], - self.CIPHER_BLOCK_SIZE, - [i for i in range(self.CIPHER_BLOCK_SIZE)]) - - #Last round different from others - last_round_sboxes = [] - for sb in range(self.NUM_SBOXES): - sbox = self.add_SBOX_component( - [round_output.id], - [[i for i in range(4*sb, 4*sb + 4)]], - self.SBOX_BIT_SIZE, - self.inverse_sbox) - last_round_sboxes.append(sbox) - - last_round_add_round_key = [] - for sb in range(self.NUM_SBOXES): - add_round_key = self.add_XOR_component([key_state[1].id, last_round_sboxes[sb].id], - [[i for i in range(4*sb, 4*sb + 4)], - [i for i in range(self.SBOX_BIT_SIZE)]], - self.SBOX_BIT_SIZE) - last_round_add_round_key.append(add_round_key) - - round_output = self.add_round_output_component([last_round_add_round_key[i].id for i in range(self.NUM_SBOXES)], + else: + round_output = masked_state + + return round_output, tweak_state + + def last_round_end(self, state, key_state, tweak_state, constants_states): + #Last round different from others + id_links = [[state[i]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4))] for _ in range(self.NUM_SBOXES)] + sboxed_state = self.state_sboxing(id_links, bit_positions, self.inverse_sbox) + + id_links = [[sboxed_state[i], key_state[1][0][0]] for i in range(self.NUM_SBOXES)] + bit_positions = [[list(range(4)), list(range(4*i, 4*i + 4))] for i in range(self.NUM_SBOXES)] + masked_state = self.state_masking(id_links, bit_positions) + + round_output = self.add_round_output_component([masked_state[i] for i in range(self.NUM_SBOXES)], [[i for i in range(self.SBOX_BIT_SIZE)] for j in range(self.NUM_SBOXES)], self.CIPHER_BLOCK_SIZE) cipher_output = self.add_cipher_output_component([round_output.id], [[i for i in range(self.CIPHER_BLOCK_SIZE)]], self.CIPHER_BLOCK_SIZE) - - def update_constants(self, constant): - spill = self.add_SHIFT_component([constant.id], + + return cipher_output + + + + + + + + #-------------------------------------TOTALS-------------------------------------# + + def state_masking(self, id_links, bit_positions): + masked_state = [] + for l in range(len(id_links)): + masked_state.append(self.add_XOR_component(id_links[l], + bit_positions[l], + len(bit_positions[l][0])).id) + + return masked_state + + def state_sboxing(self, id_links, bit_positions, sbox): + sboxed_state = [] + for l in range(len(id_links)): + sboxed_state.append(self.add_SBOX_component(id_links[l], + bit_positions[l], + self.WORD_SIZE, + sbox).id) + + return sboxed_state + + def tweak_update(self, bit_positions, tweak_shuffle): #direct encryption + perm_tweak = [bit_positions[i] for i in tweak_shuffle] + + return perm_tweak + + def state_rotation(self, id_links): + round_state_rotate = [] + for l in range(self.number_of_layers): + for col in range(4): + round_state_rotate.extend(self.M_function([id_links[col+4*i+16*l] for i in range(4)], [list(range(4)) for j in range(4)])) + + return round_state_rotate + + def key_update(self, key_state): + alpha, beta = self.constants_update() + + if self.number_of_layers == 2: + key_state[0] = [[self.add_XOR_component(key_state[0][0]+[alpha[0], alpha[1]], + key_state[0][1]+[list(range(self.LAYER_BLOCK_SIZE)), list(range(self.LAYER_BLOCK_SIZE))], + self.KEY_BLOCK_SIZE).id], [list(range(self.KEY_BLOCK_SIZE))]] + key_state[1] = [[self.add_XOR_component(key_state[1][0]+[beta[0], beta[1]], + key_state[1][1]+[list(range(self.LAYER_BLOCK_SIZE)), list(range(self.LAYER_BLOCK_SIZE))], + self.KEY_BLOCK_SIZE).id], [list(range(self.KEY_BLOCK_SIZE))]] + else: + key_state[0] = [[self.add_XOR_component(key_state[0][0]+[alpha[0]], + key_state[0][1]+[list(range(self.LAYER_BLOCK_SIZE))], + self.KEY_BLOCK_SIZE).id], [list(range(self.KEY_BLOCK_SIZE))]] + key_state[1] = [[self.add_XOR_component(key_state[1][0]+[beta[0]], + key_state[1][1]+[list(range(self.LAYER_BLOCK_SIZE))], + self.KEY_BLOCK_SIZE).id], [list(range(self.KEY_BLOCK_SIZE))]] + + return key_state + + def constants_update(self): + alpha_0 = self.add_constant_component(self.LAYER_BLOCK_SIZE, 0x13198A2E03707344).id + alpha = [alpha_0] + if self.number_of_layers == 2: + alpha_1 = self.update_single_constant(alpha[0]) + alpha.append(alpha_1) + beta_0 = self.update_single_constant(alpha[-1]) + beta = [beta_0] + if self.number_of_layers == 2: + beta_1 = self.update_single_constant(beta_0) + beta.append(beta_1) + + return alpha, beta + + #--------------------------------------------------------------------------------# + + def update_single_constant(self, constant): + spill = self.add_SHIFT_component([constant], [[i for i in range(self.LAYER_BLOCK_SIZE)]], self.LAYER_BLOCK_SIZE, 51) - tmp_0 = self.add_SHIFT_component([constant.id], + tmp_0 = self.add_SHIFT_component([constant], [[i for i in range(self.LAYER_BLOCK_SIZE)]], self.LAYER_BLOCK_SIZE, -13) @@ -499,37 +542,37 @@ def update_constants(self, constant): tmp = self.add_XOR_component([tmp_0.id, tmp_1.id, tmp_2.id, tmp_3.id, spill.id], [[i for i in range(self.LAYER_BLOCK_SIZE)] for j in range(5)], self.LAYER_BLOCK_SIZE) - return tmp + return tmp.id def o_function(self, key): - key_new = [] - key_rot_0 = self.add_rotate_component([key[0].id], - [[i for i in range(self.KEY_BLOCK_SIZE)]], + key_rot_0 = self.add_rotate_component(key[0][0], + key[0][1], self.KEY_BLOCK_SIZE, 1) - key_shift_0 = self.add_SHIFT_component([key[0].id], - [[i for i in range(self.KEY_BLOCK_SIZE)]], + key_shift_0 = self.add_SHIFT_component(key[0][0], + key[0][1], self.KEY_BLOCK_SIZE, self.KEY_BLOCK_SIZE-1) - key_new.append(self.add_XOR_component([key_rot_0.id, key_shift_0.id], + key_1 = [[self.add_XOR_component([key_rot_0.id, key_shift_0.id], [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.KEY_BLOCK_SIZE)]], - self.KEY_BLOCK_SIZE)) + self.KEY_BLOCK_SIZE).id], [list(range(self.KEY_BLOCK_SIZE))]] - key_lshift_1 = self.add_SHIFT_component([key[1].id], - [[i for i in range(self.KEY_BLOCK_SIZE)]], + key_lshift_1 = self.add_SHIFT_component(key[1][0], + key[1][1], self.KEY_BLOCK_SIZE, -1) key_rshift_1 = self.add_SHIFT_component([key_lshift_1.id], [[i for i in range(self.KEY_BLOCK_SIZE)]], self.KEY_BLOCK_SIZE, self.KEY_BLOCK_SIZE-1) - key_rotated_1 = self.add_XOR_component([key[1].id, key_rshift_1.id], - [[i for i in range(self.KEY_BLOCK_SIZE)], [i for i in range(self.KEY_BLOCK_SIZE)]], + key_rotated_1 = self.add_XOR_component(key[1][0]+[key_rshift_1.id], + key[1][1]+[[i for i in range(self.KEY_BLOCK_SIZE)]], self.KEY_BLOCK_SIZE) - key_new.append(self.add_rotate_component([key_rotated_1.id], + key_2 = [[self.add_rotate_component([key_rotated_1.id], [[i for i in range(self.KEY_BLOCK_SIZE)]], self.KEY_BLOCK_SIZE, - -1)) + -1).id], [list(range(self.KEY_BLOCK_SIZE))]] + key_new = [key_1, key_2] return(key_new) def M_function(self, input_ids, input_pos): diff --git a/claasp/component.py b/claasp/component.py index 297f936f..301ac360 100644 --- a/claasp/component.py +++ b/claasp/component.py @@ -145,6 +145,12 @@ def _generate_input_ids(self, suffix=''): return self.input_bit_size, input_bit_ids + def _generate_input_double_ids(self): + _, in_ids_0 = self._generate_input_ids(suffix='_0') + _, in_ids_1 = self._generate_input_ids(suffix='_1') + + return in_ids_0, in_ids_1 + def _generate_output_ids(self, suffix=''): output_id_link = self.id output_bit_size = self.output_bit_size @@ -152,6 +158,12 @@ def _generate_output_ids(self, suffix=''): return output_bit_size, output_bit_ids + def _generate_output_double_ids(self): + out_len, out_ids_0 = self._generate_output_ids(suffix='_0') + _, out_ids_1 = self._generate_output_ids(suffix='_1') + + return out_len, out_ids_0, out_ids_1 + def _get_independent_input_output_variables(self): """ Return a list of 2 lists containing the name of each input/output bit. @@ -322,10 +334,8 @@ def _get_wordwise_input_output_linked_class(self, model): input_class_ids = [] for index, link in enumerate(self.input_id_links): - for pos in range(len(self.input_bit_positions[index]) // model.word_size): - input_class_ids.append(link + '_word_' + str( - (pos * model.word_size + self.input_bit_positions[index][ - 0]) // model.word_size) + '_class') + for pos in self.input_bit_positions[index][::model.word_size]: + input_class_ids.append(link + '_word_' + str(pos // model.word_size) + '_class') return input_class_ids, output_class_ids diff --git a/claasp/components/and_component.py b/claasp/components/and_component.py index bc24342c..2e55e41b 100644 --- a/claasp/components/and_component.py +++ b/claasp/components/and_component.py @@ -17,6 +17,7 @@ # **************************************************************************** +from claasp.cipher_modules.models.sat.utils import utils as sat_utils 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.components.multi_input_non_linear_logical_operator_component import MultiInputNonlinearLogicalOperator @@ -376,6 +377,42 @@ def get_bit_based_vectorized_python_code(self, params, convert_output_to_bytes): def get_byte_based_vectorized_python_code(self, params): return [f' {self.id} =byte_vector_AND({params})'] + def sat_constraints(self): + """ + Return a list of variables and a list of clauses for AND operation in SAT CIPHER model. + + This method support AND operation using more than two operands. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher + sage: fancy = FancyBlockCipher(number_of_rounds=3) + sage: and_component = fancy.component_from(0, 8) + sage: and_component.sat_constraints() + (['and_0_8_0', + 'and_0_8_1', + 'and_0_8_2', + ... + '-and_0_8_11 xor_0_7_11', + '-and_0_8_11 key_23', + 'and_0_8_11 -xor_0_7_11 -key_23']) + """ + _, input_bit_ids = self._generate_input_ids() + output_bit_len, output_bit_ids = self._generate_output_ids() + constraints = [] + for i in range(output_bit_len): + constraints.extend(sat_utils.cnf_and(output_bit_ids[i], input_bit_ids[i::output_bit_len])) + + return output_bit_ids, constraints + def smt_constraints(self): """ Return a variable list and SMT-LIB list asserts representing AND operation FOR SMT CIPHER model. diff --git a/claasp/components/cipher_output_component.py b/claasp/components/cipher_output_component.py index 855381bc..b89d2420 100644 --- a/claasp/components/cipher_output_component.py +++ b/claasp/components/cipher_output_component.py @@ -481,8 +481,42 @@ def sat_constraints(self): return output_bit_ids, constraints - def sat_deterministic_truncated_xor_differential_trail_constraints(self): - return self.sat_constraints() + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for OUTPUT in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: output_component = speck.component_from(2, 12) + sage: output_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['cipher_output_2_12_0_0', + 'cipher_output_2_12_1_0', + 'cipher_output_2_12_2_0', + ... + 'xor_2_10_14_1 -cipher_output_2_12_30_1', + 'cipher_output_2_12_31_1 -xor_2_10_15_1', + 'xor_2_10_15_1 -cipher_output_2_12_31_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + _, out_ids_0, out_ids_1 = self._generate_output_double_ids() + constraints = [] + for out_id, in_id in zip(out_ids_0, in_ids_0): + constraints.extend(sat_utils.cnf_equivalent([out_id, in_id])) + for out_id, in_id in zip(out_ids_1, in_ids_1): + constraints.extend(sat_utils.cnf_equivalent([out_id, in_id])) + + return out_ids_0 + out_ids_1, constraints def sat_xor_differential_propagation_constraints(self, model): return self.sat_constraints() diff --git a/claasp/components/constant_component.py b/claasp/components/constant_component.py index 250fe854..caa9f7db 100644 --- a/claasp/components/constant_component.py +++ b/claasp/components/constant_component.py @@ -520,8 +520,36 @@ def sat_constraints(self): return output_bit_ids, constraints - def sat_deterministic_truncated_xor_differential_trail_constraints(self): - return self.sat_xor_differential_propagation_constraints() + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for CONSTANT in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: constant_component = speck.component_from(2, 0) + sage: constant_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['constant_2_0_0_0', + 'constant_2_0_1_0', + 'constant_2_0_2_0', + ... + '-constant_2_0_13_1', + '-constant_2_0_14_1', + '-constant_2_0_15_1']) + """ + _, out_ids_0, out_ids_1 = self._generate_output_double_ids() + constraints = [f'-{out_id}' for out_id in out_ids_0] + [f'-{out_id}' for out_id in out_ids_1] + return out_ids_0 + out_ids_1, constraints def sat_xor_differential_propagation_constraints(self, model=None): """ @@ -549,8 +577,8 @@ def sat_xor_differential_propagation_constraints(self, model=None): '-constant_2_0_14', '-constant_2_0_15']) """ - output_bit_len, output_bit_ids = self._generate_output_ids() - constraints = [f'-{output_bit_ids[i]}' for i in range(output_bit_len)] + _, output_bit_ids = self._generate_output_ids() + constraints = [f'-{output_bit_id}' for output_bit_id in output_bit_ids] result = output_bit_ids, constraints return result diff --git a/claasp/components/linear_layer_component.py b/claasp/components/linear_layer_component.py index c609c9aa..9ce6e4f0 100644 --- a/claasp/components/linear_layer_component.py +++ b/claasp/components/linear_layer_component.py @@ -695,6 +695,46 @@ def sat_constraints(self): return output_bit_ids, constraints + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for LINEAR LAYER in + SAT DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher + sage: fancy = FancyBlockCipher(number_of_rounds=3) + sage: linear_layer_component = fancy.component_from(0, 6) + sage: constraints = linear_layer_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + sage: constraints[1][11] + 'inter_0_linear_layer_0_6_0_1 inter_1_linear_layer_0_6_0_0 inter_1_linear_layer_0_6_0_1 -sbox_0_1_0_1' + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + _, out_ids_0, out_ids_1 = self._generate_output_double_ids() + matrix = self.description + constraints = [] + for i, out_ids_pair in enumerate(zip(out_ids_0, out_ids_1)): + operands = [in_ids_pair for j, in_ids_pair in enumerate(zip(in_ids_0, in_ids_1)) + if matrix[j][i]] + result_ids = [(f'inter_{j}_{self.id}_{i}_0', f'inter_{j}_{self.id}_{i}_1') + for j in range(len(operands) - 2)] + result_ids.append(out_ids_pair) + if len(operands) == 1: + constraints.extend(sat_utils.cnf_equivalent([result_ids[0][0], operands[0][0]])) + constraints.extend(sat_utils.cnf_equivalent([result_ids[0][1], operands[0][1]])) + else: + constraints.extend(sat_utils.cnf_xor_truncated_seq(result_ids, operands)) + + return out_ids_0 + out_ids_1, constraints + def sat_xor_differential_propagation_constraints(self, model): return self.sat_constraints() diff --git a/claasp/components/mix_column_component.py b/claasp/components/mix_column_component.py index c704ddaa..f171f14d 100644 --- a/claasp/components/mix_column_component.py +++ b/claasp/components/mix_column_component.py @@ -734,6 +734,37 @@ def sat_constraints(self): result = variables, constraints return result + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for MIX COLUMN in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.midori_block_cipher import MidoriBlockCipher + sage: midori = MidoriBlockCipher(number_of_rounds=3) + sage: mix_column_component = midori.component_from(0, 23) + sage: out_ids, constraints = mix_column_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + sage: constraints[7] + 'mix_column_0_23_0_0 -inter_0_mix_column_0_23_0_0' + """ + matrix = binary_matrix_of_linear_component(self) + matrix_transposed = [[matrix[i][j] for i in range(matrix.nrows())] + for j in range(matrix.ncols())] + original_description = deepcopy(self.description) + self.set_description(matrix_transposed) + out_ids, constraints = super().sat_bitwise_deterministic_truncated_xor_differential_constraints() + self.set_description(original_description) + return out_ids, constraints + def sat_xor_differential_propagation_constraints(self, model): return self.sat_constraints() diff --git a/claasp/components/modsub_component.py b/claasp/components/modsub_component.py index 9b84361a..2b033c86 100644 --- a/claasp/components/modsub_component.py +++ b/claasp/components/modsub_component.py @@ -139,7 +139,7 @@ def cp_constraints(self): return cp_declarations, cp_constraints - def get_bit_based_vectorized_python_code(self, params,convert_output_to_bytes): + def get_bit_based_vectorized_python_code(self, params, convert_output_to_bytes): return [f' {self.id} = bit_vector_MODSUB([{",".join(params)} ], ' f'{self.description[1]}, {self.output_bit_size})'] diff --git a/claasp/components/modular_component.py b/claasp/components/modular_component.py index a376f31e..7cc38a8c 100644 --- a/claasp/components/modular_component.py +++ b/claasp/components/modular_component.py @@ -892,6 +892,55 @@ def extend_constraints_for_window_size( result = output_bit_ids + dummy_bit_ids + hw_bit_ids, constraints return result + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for Modular Addition + in DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: modadd_component = speck.component_from(0, 1) + sage: modadd_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['modadd_0_1_0_0', + 'modadd_0_1_1_0', + 'modadd_0_1_2_0', + ... + 'rot_0_0_15_0 plaintext_31_0 -rot_0_0_15_1 -modadd_0_1_15_0', + 'rot_0_0_15_0 plaintext_31_0 -plaintext_31_1 -modadd_0_1_15_0', + 'modadd_0_1_15_0 -rot_0_0_15_1 -plaintext_31_1 -modadd_0_1_15_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + out_len, out_ids_0, out_ids_1 = self._generate_output_double_ids() + 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): """ Return a list of variables and a list of clauses for fixing variables in SAT XOR LINEAR model. diff --git a/claasp/components/multi_input_non_linear_logical_operator_component.py b/claasp/components/multi_input_non_linear_logical_operator_component.py index c93dcf8c..41edacb1 100644 --- a/claasp/components/multi_input_non_linear_logical_operator_component.py +++ b/claasp/components/multi_input_non_linear_logical_operator_component.py @@ -401,6 +401,45 @@ def sat_constraints(self): return output_bit_ids, constraints + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for AND/OR in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher + sage: fancy = FancyBlockCipher(number_of_rounds=3) + sage: and_component = fancy.component_from(0, 8) + sage: and_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['and_0_8_0_0', + 'and_0_8_1_0', + 'and_0_8_2_0', + ... + 'and_0_8_11_0 -key_23_1', + 'and_0_8_11_0 -and_0_8_11_1', + 'xor_0_7_11_0 key_23_0 xor_0_7_11_1 key_23_1 -and_0_8_11_0']) + """ + 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): + constraints.extend([f'{out_ids_0[i]} -{in_id}' for in_id in in_ids_0[i::out_len]]) + constraints.extend([f'{out_ids_0[i]} -{in_id}' for in_id in in_ids_1[i::out_len]]) + constraints.append(f'{out_ids_0[i]} -{out_ids_1[i]}') + clause = f'{" ".join(in_ids_0[i::out_len])} {" ".join(in_ids_1[i::out_len])} -{out_ids_0[i]}' + constraints.append(clause) + + return out_ids_0 + out_ids_1, constraints + def sat_xor_differential_propagation_constraints(self, model=None): """ Return a list of variables and a list of clauses for AND operation in SAT XOR DIFFERENTIAL model. diff --git a/claasp/components/not_component.py b/claasp/components/not_component.py index 918583d7..5d12d0fa 100644 --- a/claasp/components/not_component.py +++ b/claasp/components/not_component.py @@ -524,6 +524,44 @@ def sat_constraints(self): return output_bit_ids, constraints + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for NOT in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.permutations.gift_permutation import GiftPermutation + sage: gift = GiftPermutation(number_of_rounds=3) + sage: not_component = gift.component_from(0, 8) + sage: not_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['not_0_8_0_0', + 'not_0_8_1_0', + 'not_0_8_2_0', + ... + 'xor_0_6_30_0 -xor_0_6_30_1 -not_0_8_30_1', + 'xor_0_6_31_0 xor_0_6_31_1 not_0_8_31_1', + 'xor_0_6_31_0 -xor_0_6_31_1 -not_0_8_31_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + _, out_ids_0, out_ids_1 = self._generate_output_double_ids() + constraints = [] + for out_id, in_id in zip(out_ids_0, in_ids_0): + constraints.extend(sat_utils.cnf_equivalent([out_id, in_id])) + for out_id, in_id_0, in_id_1 in zip(out_ids_1, in_ids_0, in_ids_1): + constraints.append(f'{in_id_0} {in_id_1} {out_id}') + constraints.append(f'{in_id_0} -{in_id_1} -{out_id}') + + return out_ids_0 + out_ids_1, constraints + def sat_xor_differential_propagation_constraints(self, model=None): """ Return a list of variables and a list of clauses for NOT operation in SAT xor differential. diff --git a/claasp/components/or_component.py b/claasp/components/or_component.py index 90a48fab..b4d961c2 100644 --- a/claasp/components/or_component.py +++ b/claasp/components/or_component.py @@ -17,6 +17,7 @@ # **************************************************************************** +from claasp.cipher_modules.models.sat.utils import utils as sat_utils from claasp.cipher_modules.models.smt.utils import utils as smt_utils from claasp.components.multi_input_non_linear_logical_operator_component import MultiInputNonlinearLogicalOperator @@ -211,6 +212,42 @@ def get_bit_based_vectorized_python_code(self, params, convert_output_to_bytes): def get_byte_based_vectorized_python_code(self, params): return [f' {self.id} = byte_vector_OR({params})'] + def sat_constraints(self): + """ + Return a list of variables and a list of clauses for OR operation in SAT CIPHER model. + + This method support AND operation using more than two operands. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.permutations.gift_permutation import GiftPermutation + sage: gift = GiftPermutation(number_of_rounds=3) + sage: or_component = gift.component_from(0, 4) + sage: or_component.sat_constraints() + (['or_0_4_0', + 'or_0_4_1', + 'or_0_4_2', + ... + 'or_0_4_31 -xor_0_3_31', + 'or_0_4_31 -xor_0_1_31', + '-or_0_4_31 xor_0_3_31 xor_0_1_31']) + """ + _, input_bit_ids = self._generate_input_ids() + output_bit_len, output_bit_ids = self._generate_output_ids() + constraints = [] + for i in range(output_bit_len): + constraints.extend(sat_utils.cnf_or(output_bit_ids[i], input_bit_ids[i::output_bit_len])) + + return output_bit_ids, constraints + def smt_constraints(self): """ Return a variable list and SMT-LIB list asserts for OR operation in SMT CIPHER model. diff --git a/claasp/components/rotate_component.py b/claasp/components/rotate_component.py index 5af915c8..a72131b7 100644 --- a/claasp/components/rotate_component.py +++ b/claasp/components/rotate_component.py @@ -674,8 +674,45 @@ def sat_constraints(self): return output_bit_ids, constraints - def sat_deterministic_truncated_xor_differential_trail_constraints(self): - return self.sat_constraints() + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for ROTATION in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: rotate_component = speck.component_from(1, 1) + sage: rotate_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['rot_1_1_0_0', + 'rot_1_1_1_0', + 'rot_1_1_2_0', + ... + 'key_39_1 -rot_1_1_14_1', + 'rot_1_1_15_1 -key_40_1', + 'key_40_1 -rot_1_1_15_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + _, out_ids_0, out_ids_1 = self._generate_output_double_ids() + rotation = self.description[1] + in_ids_0_rotated = in_ids_0[-rotation:] + in_ids_0[:-rotation] + in_ids_1_rotated = in_ids_1[-rotation:] + in_ids_1[:-rotation] + constraints = [] + for out_id, in_id in zip(out_ids_0, in_ids_0_rotated): + constraints.extend(sat_utils.cnf_equivalent([out_id, in_id])) + for out_id, in_id in zip(out_ids_1, in_ids_1_rotated): + constraints.extend(sat_utils.cnf_equivalent([out_id, in_id])) + + return out_ids_0 + out_ids_1, constraints def sat_xor_differential_propagation_constraints(self, model=None): return self.sat_constraints() diff --git a/claasp/components/sbox_component.py b/claasp/components/sbox_component.py index 660a342e..73c648be 100644 --- a/claasp/components/sbox_component.py +++ b/claasp/components/sbox_component.py @@ -173,16 +173,19 @@ def smt_get_sbox_probability_constraints(bit_ids, template): return constraints + def _to_int(bits): - return int("".join(str(x) for x in bits), 2) + return int("".join(str(bit) for bit in bits), 2) + def _combine_truncated(input_1, input_2): - return [val if val == input_2[_] else 2 for _, val in enumerate(input_1)] + return [bit_1 if bit_1 == bit_2 else 2 for bit_1, bit_2 in zip(input_1, input_2)] + def _get_truncated_output_difference(ddt_row, n): output_bits = [2] * n has_undisturbed_bits = False - list_of_delta_out = [delta_out for delta_out, proba in enumerate(ddt_row) if proba] + list_of_delta_out = [delta_out for delta_out, probability in enumerate(ddt_row) if probability] for bit in range(n): delta = [j & (1 << bit) for j in list_of_delta_out] if delta.count(delta[0]) == len(delta): @@ -234,7 +237,7 @@ def algebraic_polynomials(self, model): output_vars = list(map(ring_R, output_vars)) return S.polynomials(input_vars, output_vars) - + def get_ddt_with_undisturbed_transitions(self): """ Returns a list of all truncated input/outputs tuples that have undisturbed differential bits @@ -301,7 +304,7 @@ def get_ddt_with_undisturbed_transitions(self): inputs_to_combine = newly_combined_inputs for input_bits in set(list(product([0, 1, 2], repeat=n))).difference(set(tested_inputs)): - valid_points.append((input_bits, tuple([2] * n))) + valid_points.append((input_bits, (2,)*n)) return valid_points @@ -1404,6 +1407,55 @@ def sat_constraints(self): return output_bit_ids, constraints + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for a generic S-BOX in SAT deterministic truncated XOR DIFFERENTIAL model. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.present_block_cipher import PresentBlockCipher + sage: present = PresentBlockCipher(number_of_rounds=3) + sage: sbox_component = present.component_from(0, 2) + sage: sbox_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['sbox_0_2_0_0', + 'sbox_0_2_1_0', + 'sbox_0_2_2_0', + ... + '-xor_0_0_6_0 sbox_0_2_3_0', + '-xor_0_0_5_0 sbox_0_2_3_0', + '-xor_0_0_4_0 sbox_0_2_3_0']) + """ + valid_transitions = self.get_ddt_with_undisturbed_transitions() + # building espresso input and run it + espresso_input_length = 2 * (len(valid_transitions[0][0]) + len(valid_transitions[0][1])) + espresso_input = [f".i {espresso_input_length}", ".o 1"] + for transition in valid_transitions: + espresso_condition = ['0'*(value == 0 or value == 1) + '1'*(value == 2) for value in transition[0]] + espresso_condition += ['0'*(value == 0) + '1'*(value == 1) + '-'*(value == 2) for value in transition[0]] + espresso_condition += ['0'*(value == 0 or value == 1) + '1'*(value == 2) for value in transition[1]] + espresso_condition += ['0'*(value == 0) + '1'*(value == 1) + '-'*(value == 2) for value in transition[1]] + espresso_input += ["".join(espresso_condition) + " 1"] + espresso_input += [".e"] + espresso_input = "\n".join(espresso_input) + espresso_process = subprocess.run(['espresso', '-epos'], input=espresso_input, capture_output=True, text=True) + espresso_output = espresso_process.stdout.splitlines() + # building constraints + input_ids_0, input_ids_1 = self._generate_input_double_ids() + _, output_ids_0, output_ids_1 = self._generate_output_double_ids() + input_ids = input_ids_0 + input_ids_1 + output_ids = output_ids_0 + output_ids_1 + ids = input_ids + output_ids + constraints = [] + for line in espresso_output[4:-1]: + literals = ['-' * int(line[i]) + ids[i] for i in range(espresso_input_length) if line[i] != '-'] + constraints.append(' '.join(literals)) + + return output_ids, constraints + def sat_xor_differential_propagation_constraints(self, model): """ Return a list of variables and a list of clauses for a generic S-BOX in SAT XOR DIFFERENTIAL model. diff --git a/claasp/components/shift_component.py b/claasp/components/shift_component.py index 219cce49..510bc048 100644 --- a/claasp/components/shift_component.py +++ b/claasp/components/shift_component.py @@ -705,8 +705,54 @@ def sat_constraints(self): return output_bit_ids, constraints - def sat_deterministic_truncated_xor_differential_trail_constraints(self): - return self.sat_constraints() + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for SHIFT in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.tea_block_cipher import TeaBlockCipher + sage: tea = TeaBlockCipher(number_of_rounds=3) + sage: shift_component = tea.component_from(0, 0) + sage: shift_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['shift_0_0_0_0', + 'shift_0_0_1_0', + 'shift_0_0_2_0', + ... + '-shift_0_0_30_1', + '-shift_0_0_31_0', + '-shift_0_0_31_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + out_len, out_ids_0, out_ids_1 = self._generate_output_double_ids() + shift_amount = self.description[1] + constraints = [] + if shift_amount < 0: + shift_amount = -shift_amount + for i in range(out_len - shift_amount): + constraints.extend(sat_utils.cnf_equivalent([out_ids_0[i], in_ids_0[i + shift_amount]])) + constraints.extend(sat_utils.cnf_equivalent([out_ids_1[i], in_ids_1[i + shift_amount]])) + for i in range(out_len - shift_amount, out_len): + constraints.append(f'-{out_ids_0[i]}') + constraints.append(f'-{out_ids_1[i]}') + else: + for i in range(shift_amount): + constraints.append(f'-{out_ids_0[i]}') + constraints.append(f'-{out_ids_1[i]}') + for i in range(shift_amount, out_len): + constraints.extend(sat_utils.cnf_equivalent([out_ids_0[i], in_ids_0[i - shift_amount]])) + constraints.extend(sat_utils.cnf_equivalent([out_ids_1[i], in_ids_1[i - shift_amount]])) + + return out_ids_0 + out_ids_1, constraints def sat_xor_differential_propagation_constraints(self, model=None): return self.sat_constraints() diff --git a/claasp/components/xor_component.py b/claasp/components/xor_component.py index 01f32fe4..30f6bcb3 100644 --- a/claasp/components/xor_component.py +++ b/claasp/components/xor_component.py @@ -1080,6 +1080,45 @@ def sat_constraints(self): return output_bit_ids, constraints + def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): + """ + Return a list of variables and a list of clauses for XOR in SAT + DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: xor_component = speck.component_from(0, 2) + sage: xor_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + (['xor_0_2_0_0', + 'xor_0_2_1_0', + 'xor_0_2_2_0', + ... + 'modadd_0_1_15_1 xor_0_2_15_0 xor_0_2_15_1 -key_63_1', + 'key_63_1 xor_0_2_15_0 xor_0_2_15_1 -modadd_0_1_15_1', + 'xor_0_2_15_0 -modadd_0_1_15_1 -key_63_1 -xor_0_2_15_1']) + """ + in_ids_0, in_ids_1 = self._generate_input_double_ids() + out_len, out_ids_0, out_ids_1 = self._generate_output_double_ids() + in_ids = [(id_0, id_1) for id_0, id_1 in zip(in_ids_0, in_ids_1)] + out_ids = [(id_0, id_1) for id_0, id_1 in zip(out_ids_0, out_ids_1)] + constraints = [] + for i, out_id in enumerate(out_ids): + result_ids = [(f'inter_{j}_{self.id}_{i}_0', f'inter_{j}_{self.id}_{i}_1') + for j in range(self.description[1] - 2)] + [out_id] + constraints.extend(sat_utils.cnf_xor_truncated_seq(result_ids, in_ids[i::out_len])) + + return out_ids_0 + out_ids_1, constraints + def sat_xor_differential_propagation_constraints(self, model=None): return self.sat_constraints() diff --git a/docker/Dockerfile b/docker/Dockerfile index 3f3636bd..eb4c0959 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -1,7 +1,9 @@ -FROM ubuntu:22.04 +FROM ubuntu:22.04 AS claasp-base ARG DEBIAN_FRONTEND=noninteractive ARG GUROBI_ARCH=linux64 +ARG COPY_CLAASP_LIBRARY=false +ARG INSTALL_CLAASP_LIBRARY=false # Install dependencies with apt-get RUN apt-get -qq update @@ -83,7 +85,9 @@ RUN sage -pip install bitstring==4.0.1 \ pytest==7.2.1 \ pytest-cov==4.0.0 \ pytest-xdist==3.2.0 \ - pytest-benchmark==4.0.0 + pytest-benchmark==4.0.0 \ + networkx==2.8.8 \ + numpy==1.24.3 # Installing nist sts COPY required_dependencies/assess.c /opt/ @@ -300,3 +304,9 @@ RUN sage -pip install plotly -U kaleido WORKDIR /home/sage/tii-claasp + +FROM claasp-base AS claasp-lib + +COPY . . + +RUN make install \ No newline at end of file diff --git a/docs/CONTRIBUTING.md b/docs/CONTRIBUTING.md index ea8c5a7a..305a50f5 100644 --- a/docs/CONTRIBUTING.md +++ b/docs/CONTRIBUTING.md @@ -11,8 +11,8 @@ To contribute to this project, please, follow the following conventions. - [Contributing to the documentation](#contributing-to-the-documentation) - [Project structure](#project-structure) - [GIT Conventions](#git-conventions) - - [Branches](#branches) - - [Pull Requests](#pull-requests) + - [Branches conventions](#branches-conventions) + - [Pull Requests conventions](#pull-requests-conventions) - [Best practices for development](#best-practices-for-development) - [Linter/Formatter](#linterformatter) - [Imports](#imports) @@ -472,7 +472,7 @@ This is the current project structure. ``` # GIT Conventions -## Branches +## Branches Conventions - `main` is the main branch. - `develop` is the branch where the latest changes are merged into. - `/` is the branch where a new feature is developed. @@ -480,7 +480,7 @@ This is the current project structure. > ⚠️ We encourage you to follow this convention when creating new branches even though branches with the naming > convention `` are allowed. ⚠️ -## Pull Requests +## Pull Requests Conventions - Pull Requests should be made from a `feature-branch` to `develop` and it should be reviewed by at least one person. - New branches to development tasks will have `develop` branch as origin. - The only allowed Pull Requests to `main` branch must come from `develop` branch. All other Pull Requests will be diff --git a/tests/unit/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model_test.py index 378ce024..27d35a78 100644 --- a/tests/unit/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model_test.py +++ b/tests/unit/cipher_modules/models/milp/milp_models/milp_bitwise_impossible_xor_differential_model_test.py @@ -47,6 +47,13 @@ def test_find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic assert trail['components_values']['intermediate_output_5_12_backward']['value'] == SIMON_INCOMPATIBLE_ROUND_OUTPUT assert trail['components_values']['cipher_output_10_13_backward']['value'] == '000000?0?00000000000000000000000' + trail = milp.find_one_bitwise_impossible_xor_differential_trail_with_fully_automatic_model( + fixed_values=[plaintext, key, key_backward, ciphertext_backward], include_all_components=True) + assert trail['status'] == 'SATISFIABLE' + assert trail['components_values']['plaintext']['value'] == '00000000000000000000000000000001' + assert trail['components_values']['intermediate_output_5_12_backward']['value'] == SIMON_INCOMPATIBLE_ROUND_OUTPUT + assert trail['components_values']['cipher_output_10_13_backward']['value'] == '000000?0?00000000000000000000000' + def test_find_one_bitwise_impossible_xor_differential_trail_with_chosen_incompatible_components(): ascon = AsconSboxSigmaPermutation(number_of_rounds=5) milp = MilpBitwiseImpossibleXorDifferentialModel(ascon) diff --git a/tests/unit/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model_test.py b/tests/unit/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model_test.py new file mode 100644 index 00000000..ac8d13f7 --- /dev/null +++ b/tests/unit/cipher_modules/models/sat/cms_models/cms_deterministic_truncated_xor_differential_model_test.py @@ -0,0 +1,9 @@ +from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher +from claasp.cipher_modules.models.sat.cms_models.cms_bitwise_deterministic_truncated_xor_differential_model import \ + CmsSatDeterministicTruncatedXorDifferentialModel + + +def test_build_bitwise_deterministic_truncated_xor_differential_trail_model(): + speck = SpeckBlockCipher(number_of_rounds=22) + cms = CmsSatDeterministicTruncatedXorDifferentialModel(speck) + cms.build_bitwise_deterministic_truncated_xor_differential_trail_model() diff --git a/tests/unit/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model_test.py b/tests/unit/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model_test.py new file mode 100644 index 00000000..7cceb6ae --- /dev/null +++ b/tests/unit/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model_test.py @@ -0,0 +1,44 @@ +from claasp.cipher_modules.models.utils import get_single_key_scenario_format_for_fixed_values, set_fixed_variables +from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher +from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import \ + SatBitwiseDeterministicTruncatedXorDifferentialModel + + +def test_build_bitwise_deterministic_truncated_xor_differential_trail_model(): + speck = SpeckBlockCipher(number_of_rounds=22) + sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + sat.build_bitwise_deterministic_truncated_xor_differential_trail_model() + constraints = sat.model_constraints + + assert len(constraints) == 28761 + assert str(constraints[0]) == 'rot_0_0_0_0 -plaintext_9_0' + assert str(constraints[1]) == 'plaintext_9_0 -rot_0_0_0_0' + assert str(constraints[-2]) == 'cipher_output_21_12_31_1 -xor_21_10_15_1' + assert str(constraints[-1]) == 'xor_21_10_15_1 -cipher_output_21_12_31_1' + + +def test_find_one_bitwise_deterministic_truncated_xor_differential_trail(): + speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2) + sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + plaintext = set_fixed_variables(component_id='plaintext', constraint_type='equal', bit_positions=range(32), + bit_values=(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0)) + key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=(0,) * 64) + trail = sat.find_one_bitwise_deterministic_truncated_xor_differential_trail(fixed_values=[plaintext, key]) + assert trail['components_values']['intermediate_output_0_6']['value'] == '????100000000000????100000000011' + + speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=3) + sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + plaintext = set_fixed_variables(component_id='plaintext', constraint_type='equal', bit_positions=range(32), + bit_values=(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0)) + key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=(0,) * 64) + trail = sat.find_one_bitwise_deterministic_truncated_xor_differential_trail(fixed_values=[plaintext, key]) + assert trail['components_values']['cipher_output_2_12']['value'] == '???????????????0????????????????' + + +def test_find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential_trail(): + speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2) + sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck) + trail = sat.find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential_trail(get_single_key_scenario_format_for_fixed_values(speck)) + assert trail['status'] == 'SATISFIABLE' diff --git a/tests/unit/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model_test.py b/tests/unit/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model_test.py deleted file mode 100644 index 3e8162ac..00000000 --- a/tests/unit/cipher_modules/models/sat/sat_models/sat_deterministic_truncated_xor_differential_model_test.py +++ /dev/null @@ -1,9 +0,0 @@ -from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher -from claasp.cipher_modules.models.sat.sat_models.sat_deterministic_truncated_xor_differential_model import \ - SatDeterministicTruncatedXorDifferentialModel - - -def test_build_deterministic_truncated_xor_differential_trail_model(): - speck = SpeckBlockCipher(number_of_rounds=22) - sat = SatDeterministicTruncatedXorDifferentialModel(speck) - sat.build_deterministic_truncated_xor_differential_trail_model() diff --git a/tests/unit/ciphers/block_ciphers/qarmav2_block_cipher_test.py b/tests/unit/ciphers/block_ciphers/qarmav2_block_cipher_test.py index da90552f..36c2dba6 100644 --- a/tests/unit/ciphers/block_ciphers/qarmav2_block_cipher_test.py +++ b/tests/unit/ciphers/block_ciphers/qarmav2_block_cipher_test.py @@ -8,9 +8,9 @@ def test_qarmav2_block_cipher(): qarmav2 = QARMAv2BlockCipher(number_of_rounds = 4) assert qarmav2.type == 'block_cipher' assert qarmav2.family_name == 'qarmav2_block_cipher' - assert qarmav2.number_of_rounds == 8 - assert qarmav2.id == 'qarmav2_block_cipher_k128_p64_i128_o64_r8' - assert qarmav2.component_from(0, 0).id == 'linear_layer_0_0' + assert qarmav2.number_of_rounds == 9 + assert qarmav2.id == 'qarmav2_block_cipher_k128_p64_i128_o64_r9' + assert qarmav2.component_from(0, 0).id == 'constant_0_0' qarmav2 = QARMAv2BlockCipher(number_of_rounds = 4) key = 0x0123456789abcdeffedcba9876543210 @@ -26,9 +26,9 @@ def test_qarmav2_block_cipher(): ciphertext = 0xd459510ab82c66fc assert qarmav2.evaluate([key, plaintext, tweak]) == ciphertext - #qarmav2 = QARMAv2BlockCipher(number_of_layers = 2, number_of_rounds = 9) - #key = 0x00102030405060708090a0b0c0d0e0f00f0e0d0c0b0a09080706050403020100 - #plaintext = 0x00000000000000000000000000000000 - #tweak = 0x7e5c3a18f6d4b290e5c3a18f6d4b29071eb852fc630da741b852fc960da741eb - #ciphertext = 0x361262e2ecf88f03f4ea898d6a4f412f - #assert qarmav2.evaluate([key, plaintext, tweak]) == ciphertext + qarmav2 = QARMAv2BlockCipher(number_of_layers = 2, number_of_rounds = 9, key_bit_size = 256, tweak_bit_size = 256) + key = 0x00102030405060708090a0b0c0d0e0f00f0e0d0c0b0a09080706050403020100 + plaintext = 0x00000000000000000000000000000000 + tweak = 0x7e5c3a18f6d4b290e5c3a18f6d4b29071eb852fc630da741b852fc960da741eb + ciphertext = 0x361262e2ecf88f03f4ea898d6a4f412f + assert qarmav2.evaluate([key, plaintext, tweak]) == ciphertext diff --git a/tests/unit/components/and_component_test.py b/tests/unit/components/and_component_test.py index 682a638f..80b7e85a 100644 --- a/tests/unit/components/and_component_test.py +++ b/tests/unit/components/and_component_test.py @@ -64,6 +64,20 @@ def test_generic_sign_linear_constraints(): assert and_component.generic_sign_linear_constraints(input_constraints, output) == 1 +def test_sat_constraints(): + fancy = FancyBlockCipher(number_of_rounds=3) + and_component = fancy.component_from(0, 8) + output_bit_ids, constraints = and_component.sat_constraints() + + assert output_bit_ids[0] == 'and_0_8_0' + assert output_bit_ids[1] == 'and_0_8_1' + assert output_bit_ids[2] == 'and_0_8_2' + + assert constraints[-3] == '-and_0_8_11 xor_0_7_11' + assert constraints[-2] == '-and_0_8_11 key_23' + assert constraints[-1] == 'and_0_8_11 -xor_0_7_11 -key_23' + + def test_smt_constraints(): fancy = FancyBlockCipher(number_of_rounds=3) and_component = fancy.component_from(0, 8) diff --git a/tests/unit/components/linear_layer_component_test.py b/tests/unit/components/linear_layer_component_test.py index 3a13febc..aa7773d8 100644 --- a/tests/unit/components/linear_layer_component_test.py +++ b/tests/unit/components/linear_layer_component_test.py @@ -192,6 +192,16 @@ def test_sat_constraints(): '-sbox_0_4_3 -sbox_0_5_1 -sbox_0_5_2 -sbox_0_5_3' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + fancy = FancyBlockCipher(number_of_rounds=3) + linear_layer_component = fancy.component_from(0, 6) + output_bit_ids, constraints = linear_layer_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert constraints[10] == 'inter_0_linear_layer_0_6_0_1 sbox_0_1_0_1 inter_1_linear_layer_0_6_0_0 -inter_1_linear_layer_0_6_0_1' + assert constraints[70] == 'inter_0_linear_layer_0_6_1_0 -sbox_0_0_1_0' + assert constraints[100] == 'inter_3_linear_layer_0_6_1_0 sbox_0_1_3_0 -inter_4_linear_layer_0_6_1_0' + + def test_sat_xor_linear_mask_propagation_constraints(): fancy = FancyBlockCipher(number_of_rounds=3) linear_layer_component = fancy.component_from(0, 6) diff --git a/tests/unit/components/mix_column_component_test.py b/tests/unit/components/mix_column_component_test.py index f2b0f88e..f0d2df5f 100644 --- a/tests/unit/components/mix_column_component_test.py +++ b/tests/unit/components/mix_column_component_test.py @@ -148,6 +148,20 @@ def test_sat_constraints(): assert constraints[-1] == 'mix_column_0_23_15 -mix_column_0_20_35 -mix_column_0_20_39 -mix_column_0_20_43' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + midori = MidoriBlockCipher(number_of_rounds=3) + mix_column_component = midori.component_from(0, 23) + output_bit_ids, constraints = mix_column_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert output_bit_ids[3] == 'mix_column_0_23_3_0' + assert output_bit_ids[9] == 'mix_column_0_23_9_0' + assert output_bit_ids[27] == 'mix_column_0_23_11_1' + + assert constraints[30] == 'mix_column_0_20_38_0 mix_column_0_20_42_0 -inter_0_mix_column_0_23_2_0' + assert constraints[60] == 'mix_column_0_20_32_1 inter_0_mix_column_0_23_4_0 inter_0_mix_column_0_23_4_1 -mix_column_0_20_40_1' + assert constraints[90] == 'inter_0_mix_column_0_23_6_0 -mix_column_0_20_34_1 -mix_column_0_20_42_1 -inter_0_mix_column_0_23_6_1' + + def test_sat_xor_linear_mask_propagation_constraints(): midori = MidoriBlockCipher(number_of_rounds=3) mix_column_component = midori.component_from(0, 23) diff --git a/tests/unit/components/multi_input_non_linear_logical_operator_component_test.py b/tests/unit/components/multi_input_non_linear_logical_operator_component_test.py index 122002fa..39c72738 100644 --- a/tests/unit/components/multi_input_non_linear_logical_operator_component_test.py +++ b/tests/unit/components/multi_input_non_linear_logical_operator_component_test.py @@ -96,6 +96,20 @@ def test_sat_constraints(): assert constraints[-1] == 'and_0_8_11 -xor_0_7_11 -key_23' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + fancy = FancyBlockCipher(number_of_rounds=3) + and_component = fancy.component_from(0, 8) + output_bit_ids, constraints = and_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert output_bit_ids[0] == 'and_0_8_0_0' + assert output_bit_ids[7] == 'and_0_8_7_0' + assert output_bit_ids[14] == 'and_0_8_2_1' + + assert constraints[-14] == 'and_0_8_9_0 -and_0_8_9_1' + assert constraints[-7] == 'xor_0_7_10_0 key_22_0 xor_0_7_10_1 key_22_1 -and_0_8_10_0' + assert constraints[-1] == 'xor_0_7_11_0 key_23_0 xor_0_7_11_1 key_23_1 -and_0_8_11_0' + + def test_sat_xor_differential_propagation_constraints(): fancy = FancyBlockCipher(number_of_rounds=3) and_component = fancy.component_from(0, 8) diff --git a/tests/unit/components/not_component_test.py b/tests/unit/components/not_component_test.py index 41716955..b390d039 100644 --- a/tests/unit/components/not_component_test.py +++ b/tests/unit/components/not_component_test.py @@ -171,6 +171,20 @@ def test_sat_constraints(): assert constraints[-1] == '-not_0_8_31 -xor_0_6_31' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + gift = GiftPermutation(number_of_rounds=3) + not_component = gift.component_from(0, 8) + output_bit_ids, constraints = not_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert output_bit_ids[0] == 'not_0_8_0_0' + assert output_bit_ids[1] == 'not_0_8_1_0' + assert output_bit_ids[2] == 'not_0_8_2_0' + + assert constraints[-3] == 'xor_0_6_30_0 -xor_0_6_30_1 -not_0_8_30_1' + assert constraints[-2] == 'xor_0_6_31_0 xor_0_6_31_1 not_0_8_31_1' + assert constraints[-1] == 'xor_0_6_31_0 -xor_0_6_31_1 -not_0_8_31_1' + + def test_sat_xor_differential_propagation_constraints(): gift = GiftPermutation(number_of_rounds=3) not_component = gift.component_from(0, 8) diff --git a/tests/unit/components/or_component_test.py b/tests/unit/components/or_component_test.py index 5eb7eb1e..d10d56b1 100644 --- a/tests/unit/components/or_component_test.py +++ b/tests/unit/components/or_component_test.py @@ -53,6 +53,20 @@ def test_generic_sign_linear_constraints(): assert or_component.generic_sign_linear_constraints(input_tert, output) == 1 +def test_sat_constraints(): + gift = GiftPermutation(number_of_rounds=3) + or_component = gift.component_from(0, 4) + output_bit_ids, constraints = or_component.sat_constraints() + + assert output_bit_ids[0] == 'or_0_4_0' + assert output_bit_ids[1] == 'or_0_4_1' + assert output_bit_ids[2] == 'or_0_4_2' + + assert constraints[-3] == 'or_0_4_31 -xor_0_3_31' + assert constraints[-2] == 'or_0_4_31 -xor_0_1_31' + assert constraints[-1] == '-or_0_4_31 xor_0_3_31 xor_0_1_31' + + def test_smt_constraints(): gift = GiftPermutation(number_of_rounds=3) or_component = gift.component_from(0, 4) diff --git a/tests/unit/components/sbox_component_test.py b/tests/unit/components/sbox_component_test.py index f37a1839..786fd08e 100644 --- a/tests/unit/components/sbox_component_test.py +++ b/tests/unit/components/sbox_component_test.py @@ -260,6 +260,20 @@ def test_sat_constraints(): assert constraints[-1] == '-xor_0_0_4 -xor_0_0_5 -xor_0_0_6 -xor_0_0_7 -sbox_0_2_3' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + present = PresentBlockCipher(number_of_rounds=3) + sbox_component = present.component_from(0, 2) + output_bit_ids, constraints = sbox_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert output_bit_ids[0] == 'sbox_0_2_0_0' + assert output_bit_ids[1] == 'sbox_0_2_1_0' + assert output_bit_ids[2] == 'sbox_0_2_2_0' + + assert constraints[-3] == '-xor_0_0_6_0 sbox_0_2_3_0' + assert constraints[-2] == '-xor_0_0_5_0 sbox_0_2_3_0' + assert constraints[-1] == '-xor_0_0_4_0 sbox_0_2_3_0' + + def test_sat_xor_differential_propagation_constraints(): present = PresentBlockCipher(number_of_rounds=3) sbox_component = present.component_from(0, 2) diff --git a/tests/unit/components/shift_component_test.py b/tests/unit/components/shift_component_test.py index 2f358220..a05be812 100644 --- a/tests/unit/components/shift_component_test.py +++ b/tests/unit/components/shift_component_test.py @@ -174,6 +174,20 @@ def test_sat_constraints(): assert constraints[-1] == '-shift_0_0_31' +def test_sat_bitwise_deterministic_truncated_xor_differential_constraints(): + tea = TeaBlockCipher(number_of_rounds=3) + shift_component = tea.component_from(0, 0) + output_bit_ids, constraints = shift_component.sat_bitwise_deterministic_truncated_xor_differential_constraints() + + assert output_bit_ids[0] == 'shift_0_0_0_0' + assert output_bit_ids[25] == 'shift_0_0_25_0' + assert output_bit_ids[50] == 'shift_0_0_18_1' + + assert constraints[0] == 'shift_0_0_0_0 -plaintext_36_0' + assert constraints[100] == 'shift_0_0_25_0 -plaintext_61_0' + assert constraints[-1] == '-shift_0_0_31_1' + + def test_sat_xor_linear_mask_propagation_constraints(): tea = TeaBlockCipher(number_of_rounds=3) shift_component = tea.component_from(0, 0)