Sat differential linear model

class SatDifferentialLinearModel(cipher, list_of_components, middle_part_model='sat_bitwise_deterministic_truncated_xor_differential_constraints')

Bases: SatModel

Model that combines concrete XOR differential model with bitwise deterministic truncated differential model and linear model to create a differential-linear model.

build_generic_sat_model_from_dictionary(component_and_model_types)
build_xor_differential_linear_model(weight=- 1, num_unknown_vars=None, unknown_window_size_configuration=None)

Constructs a model to search for differential-linear trails. This model is a combination of the concrete XOR differential model, the bitwise truncated deterministic model, and the linear XOR differential model.

INPUT: - weight – integer (default: -1); specifies the maximum probability weight. If set to a non-negative integer, it constrains the search to trails with the fixed probability weight. - number_of_unknown_variables – int (default: None); specifies the upper limit on the number of unknown variables allowed in the differential trail.

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_differential_linear_model import SatDifferentialLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=6)
sage: component_model_types = []
sage: middle_part_components = []
sage: bottom_part_components = []
sage: for round_number in range(2, 3):
....:     middle_part_components += [component.id for component in speck.get_components_in_round(round_number)]
sage: for round_number in range(3, 6):
....:     bottom_part_components += [component.id for component in speck.get_components_in_round(round_number)]
sage: component_model_list = {
....:     'middle_part_components': middle_part_components,
....:     'bottom_part_components': bottom_part_components
....: }
sage: sat = SatDifferentialLinearModel(speck, component_model_list)
sage: sat.build_xor_differential_linear_model()
...
calculate_component_weight(component, out_suffix, output_values_dict)
property cipher

Returns the cipher instance associated with the model.

RETURN: - object; The cipher object being used in this model.

property cipher_id
find_lowest_weight_xor_differential_linear_trail(fixed_values=[], solver_name='CRYPTOMINISAT_EXT', num_unknown_vars=1)

Finds the differential-linear trail with the lowest weight.

INPUT: - fixed_values – list (default: []); specifies a list of variables that should be fixed to specific values. Each entry in the list should be a dictionary representing constraints for specific components, written in the CLAASP constraining syntax. - solver_name – str (default: solvers.SOLVER_DEFAULT); The SAT solver to use. - num_unknown_vars – int (default: 1); number of unknown variables in the output of the middle round

RETURN: - dict; Solution with the trail and metadata (weight, time, memory usage).

find_one_differential_linear_trail_with_fixed_weight(weight, num_unknown_vars=None, fixed_values=[], solver_name='CRYPTOMINISAT_EXT', unknown_window_size_configuration=None)

Finds one XOR differential-linear trail with a fixed weight. The weight must be the sum of the probability weight of the top part (differential part) and the correlation weight of the bottom part (linear part).

INPUT: - weight – int; Maximum probability weight for the regular XOR differential part. - num_unknown_vars – int (default: None); Upper limit on the number of unknown variables allowed. - fixed_values – list (default: []); specifies a list of variables that should be fixed to specific values. Each entry in the list should be a dictionary representing constraints for specific components, written in the CLAASP constraining syntax. - solver_name – str (default: solvers.SOLVER_DEFAULT); The name of the SAT solver to use.

RETURN: - dict; Solution returned by the solver, including the trail and additional information.

EXAMPLES::

sage: from claasp.cipher_modules.models.sat.sat_models.sat_differential_linear_model import SatDifferentialLinearModel sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher sage: import itertools sage: speck = SpeckBlockCipher(number_of_rounds=6) sage: middle_part_components = [] sage: bottom_part_components = [] sage: for round_number in range(2, 3): ….: middle_part_components.append(speck.get_components_in_round(round_number)) sage: for round_number in range(3, 6): ….: bottom_part_components.append(speck.get_components_in_round(round_number)) sage: middle_part_components = list(itertools.chain(*middle_part_components)) sage: bottom_part_components = list(itertools.chain(*bottom_part_components)) sage: middle_part_components = [component.id for component in middle_part_components] sage: bottom_part_components = [component.id for component in bottom_part_components] sage: plaintext = set_fixed_variables( ….: component_id=’plaintext’, ….: constraint_type=’equal’, ….: bit_positions=range(32), ….: bit_values=integer_to_bit_list(0x05020402, 32, ‘big’) ….: ) sage: key = set_fixed_variables( ….: component_id=’key’, ….: constraint_type=’equal’, ….: bit_positions=range(64), ….: bit_values=(0,) * 64 ….: ) sage: ciphertext_difference = set_fixed_variables( ….: component_id=’cipher_output_5_12’, ….: constraint_type=’equal’, ….: bit_positions=range(32), ….: bit_values=integer_to_bit_list(0x00040004, 32, ‘big’) ….: ) sage: component_model_list = { ….: ‘middle_part_components’: middle_part_components, ….: ‘bottom_part_components’: bottom_part_components ….: } sage: sat_heterogeneous_model = SatDifferentialLinearModel(speck, component_model_list) sage: trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight( ….: weight=10, ….: fixed_values=[key, plaintext, ciphertext_difference], ….: solver_name=”CADICAL_EXT”, ….: num_unknown_vars=2 ….: ) sage: trail[“status”] == ‘SATISFIABLE’ True

static fix_variables_value_constraints(fixed_variables, regular_components=None, truncated_components=None, linear_components=None)

Imposes fixed value constraints on variables within differential, truncated, and linear components.

INPUT: - fixed_variables – list (default: []); specifies a list of variables that should be fixed to specific values. Each entry in the list should be a dictionary representing constraints for specific components, written in the CLAASP constraining syntax. - regular_components – list (default: None); list of regular components. - truncated_components – list (default: None); list of truncated components. - linear_components – list (default: None); list of linear components.

RETURN: - list; A list of constraints for the model.

property model_constraints

Return the model specified by model_type.

If the key refers to one of the available solver, Otherwise will raise a KeyError exception.

INPUT:

  • model_type – string; the model to retrieve

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.sat_model import SatModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: sat = SatModel(speck)
sage: sat.model_constraints('xor_differential')
Traceback (most recent call last):
...
ValueError: No model generated
property sboxes_ddt_templates
property sboxes_lat_templates
solve(model_type, solver_name='CRYPTOMINISAT_EXT', options=None)

Return the solution of the model using the solver_name SAT solver.

Note

Two types of solvers can be chosen: external or internal. In the following list of inputs, allowed SAT solvers are listed. Those ending with _sage will not create a subprocess nor additional files and will work completely embedded in Sage. Remaining solvers are allowed, but they need to be installed in the system.

INPUT:

  • model_type – string; the model for which we want a solution. Available values are:

    • 'cipher'

    • 'xor_differential'

    • 'xor_linear'

  • solver_name – string (default: cryptominisat); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_cipher_model import SatCipherModel
sage: from claasp.ciphers.block_ciphers.tea_block_cipher import TeaBlockCipher
sage: tea = TeaBlockCipher(number_of_rounds=32)
sage: sat = SatCipherModel(tea)
sage: sat.build_cipher_model()
sage: sat.solve('cipher') # random
{'cipher_id': 'tea_p64_k128_o64_r32',
 'model_type': 'tea_p64_k128_o64_r32',
 'solver_name': 'CRYPTOMINISAT_EXT',
 ...
  'intermediate_output_31_15': {'value': '8ca8d5de0906f08e', 'weight': 0, 'sign': 1},
  'cipher_output_31_16': {'value': '8ca8d5de0906f08e', 'weight': 0, 'sign': 1}},
 'total_weight': 0,
 'status': 'SATISFIABLE'}}
weight_constraints(weight)

Return lists of variables and constraints that fix the total weight of the trail to a specific value.

INPUT:

  • weight – integer; the total weight of the trail

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorDifferentialModel(speck)
sage: sat.build_xor_differential_trail_model()
sage: sat.weight_constraints(7)
(['dummy_hw_0_0_0',
  'dummy_hw_0_0_1',
  'dummy_hw_0_0_2',
  ...
  '-dummy_hw_0_77_6 dummy_hw_0_78_6',
  '-hw_modadd_2_7_14 -dummy_hw_0_77_6',
  '-hw_modadd_2_7_15 -dummy_hw_0_78_6'])