Skip to content

Commit

Permalink
FEATURE/Add: Fully automatic MILP search of xor differential impossib…
Browse files Browse the repository at this point in the history
…le trails at component level
p-huynh committed Dec 9, 2023
1 parent 15696a0 commit 5c9776c
Showing 5 changed files with 111 additions and 39 deletions.
2 changes: 1 addition & 1 deletion claasp/cipher_modules/inverse_cipher.py
Original file line number Diff line number Diff line change
@@ -833,7 +833,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)
Original file line number Diff line number Diff line change
@@ -16,13 +16,15 @@
# ****************************************************************************

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.name_mappings import CIPHER_OUTPUT, INPUT_KEY
from claasp.cipher_modules.models.milp.utils import utils as milp_utils


@@ -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,8 +187,10 @@ 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)


@@ -205,9 +208,14 @@ 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)]

# 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]]

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]
@@ -222,7 +230,7 @@ def add_constraints_to_build_in_sage_milp_class_with_chosen_incompatible_compone
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]))

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 +240,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 +254,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)
@@ -265,17 +275,31 @@ def add_constraints_to_build_fully_automatic_model_in_sage_milp_class(self, fixe
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]
backward_components = [c for c in self._backward_cipher.get_all_components() if
c.description == ['round_output'] and set(c.input_id_links) != {
forward_output.id + MILP_BACKWARD_SUFFIX}]

key_flow = set(get_key_schedule_component_ids(self._cipher)) - {INPUT_KEY}
backward_key_flow = [f'{id}{MILP_BACKWARD_SUFFIX}' for id in key_flow]

if include_all_components:
backward_components = set(self._backward_cipher.get_all_components()) - set(self._backward_cipher.get_component_from_id(key_flow_id) for key_flow_id in backward_key_flow)

for backward_component in backward_components:
output_bit_size = backward_component.output_bit_size
input_ids, output_ids = backward_component._get_input_output_variables()

if include_all_components:
# for multiple input components such as the XOR, ensures compatibility occurs on the correct branch
inputs_to_be_kept = []
for index, input_id in enumerate(["_".join(i.split("_")[:-1]) for i in set(backward_component.input_id_links)]):
if f'{INPUT_KEY}' not in input_id and [link+MILP_BACKWARD_SUFFIX for link in self._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]
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)]
inconsistent_vars = [x[f"{backward_component.id}_inconsistent_{_}"] for _ in range(output_bit_size)]
all_inconsistent_vars += inconsistent_vars

for inconsistent_index in range(output_bit_size):
@@ -414,7 +438,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 +449,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 +483,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)
Loading

0 comments on commit 5c9776c

Please sign in to comment.