Sat xor differential model¶

class SatXorDifferentialModel(cipher, counter='sequential', compact=False)¶

Bases: SatModel

build_generic_sat_model_from_dictionary(component_and_model_types)¶

build_xor_differential_trail_and_checker_model_at_intermediate_output_level(weight=- 1, fixed_variables=[])¶

Build the model for the search of XOR DIFFERENTIAL trails and the model to check that there is at least one pair satisfying such trails at the intermediate output level.

INPUT:

weight – integer (default: -1); a specific weight. If set to non-negative integer, fixes the XOR trail weight
fixed_variables – list (default: []); the variables to be fixed in standard format

See also

set_fixed_variables()

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: sat = SatXorDifferentialModel(speck)
sage: sat.build_xor_differential_trail_and_checker_model_at_intermediate_output_level()

build_xor_differential_trail_model(weight=- 1, fixed_variables=[])¶

Build the model for the search of XOR DIFFERENTIAL trails.

INPUT:

weight – integer (default: -1); a specific weight. If set to non-negative integer, fixes the XOR trail weight
fixed_variables – list (default: []); the variables to be fixed in standard format

See also

set_fixed_variables()

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: sat = SatXorDifferentialModel(speck)
sage: sat.build_xor_differential_trail_model()

calculate_component_weight(component, out_suffix, output_values_dict)¶

property cipher_id¶

find_all_xor_differential_trails_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')¶

Return a list of solutions containing all the XOR differential trails having the fixed_weight weight. By default, the search is set in the single-key setting.

INPUT:

fixed_weight – integer; the weight to be fixed
fixed_values – list (default: []); they can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

# single-key setting
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=5)
sage: sat = SatXorDifferentialModel(speck)
sage: trails = sat.find_all_xor_differential_trails_with_fixed_weight(9)
sage: len(trails) == 2
True

# related-key setting
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: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: sat = SatXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trails = sat.find_all_xor_differential_trails_with_fixed_weight(2, fixed_values=[key])
sage: len(trails) == 2
True

find_all_xor_differential_trails_with_weight_at_most(min_weight, max_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')¶

Return a list of solutions. By default, the search is set in the single-key setting.

The list contain all the XOR differential trails having the weight lying in the interval [min_weight, max_weight].

INPUT:

min_weight – integer; the weight from which to start the search
max_weight – integer; the weight at which the search stops
fixed_values – list (default: []); they can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

# single-key setting
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=5)
sage: sat = SatXorDifferentialModel(speck)
sage: trails = sat.find_all_xor_differential_trails_with_weight_at_most(9, 10)
sage: len(trails) == 28
True

# related-key setting
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: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: sat = SatXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trails = sat.find_all_xor_differential_trails_with_weight_at_most(2, 3, fixed_values=[key])
sage: len(trails) == 9
True

find_lowest_weight_xor_differential_trail(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')¶

Return the solution representing a trail with the lowest weight. By default, the search is set in the single-key setting.

Note

There could be more than one trail with the lowest weight. In order to find all the lowest weight trail, run find_all_xor_differential_trails_with_fixed_weight().

INPUT:

fixed_values – list (default: []); can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

# single-key setting
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=5)
sage: sat = SatXorDifferentialModel(speck)
sage: trail = sat.find_lowest_weight_xor_differential_trail()
sage: trail['total_weight']
9.0

# related-key setting
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: sat = SatXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:         component_id='key',
....:         constraint_type='not_equal',
....:         bit_positions=range(64),
....:         bit_values=(0,)*64)
sage: trail = sat.find_lowest_weight_xor_differential_trail(fixed_values=[key])
sage: trail['total_weight']
1.0

find_one_xor_differential_trail(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')¶

Return the solution representing a XOR differential trail. By default, the search is set in the single-key setting. The solution probability is almost always lower than the one of a random guess of the longest input.

INPUT:

fixed_values – list (default: []); they can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

# single-key setting
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: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: sat = SatXorDifferentialModel(speck)
sage: sat.find_one_xor_differential_trail() # random

# related-key setting
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: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: sat = SatXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: result = sat.find_one_xor_differential_trail(fixed_values=[key])
sage: result['total_weight'] == 9.0
True

find_one_xor_differential_trail_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')¶

Return the solution representing a XOR differential trail whose probability is 2 ** fixed_weight. By default, the search is set in the single-key setting. INPUT:

fixed_weight – integer; the weight to be fixed
fixed_values – list (default: []); can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

# single-key setting
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.set_window_size_heuristic_by_round([0, 0, 0])
sage: trail = sat.find_one_xor_differential_trail_with_fixed_weight(3)
...
sage: trail['total_weight']
3.0

# related-key setting
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: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trail = sat.find_one_xor_differential_trail_with_fixed_weight(3, fixed_values=[key])
sage: trail['total_weight']
3.0

static fix_variables_value_constraints(fixed_variables=[])¶

Return lists of variables and clauses for fixing variables in CIPHER model.

See also

SAT standard of Cipher for the format.

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_model import SatModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatModel(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': [1, 1, 1, 0]
....: }]
sage: SatModel.fix_variables_value_constraints(fixed_variables)
['plaintext_0',
 '-plaintext_1',
 'plaintext_2',
 'plaintext_3',
 '-ciphertext_0 -ciphertext_1 -ciphertext_2 ciphertext_3']

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¶

set_window_size_heuristic_by_component_id(window_size_by_component_id_values, number_of_full_windows=None, full_window_operator='at_least')¶

set_window_size_heuristic_by_round(window_size_by_round_values, number_of_full_windows=None, full_window_operator='at_least')¶

set_window_size_weight_pr_vars(window_size_weight_pr_vars)¶

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'])

property window_size_by_component_id_values¶

property window_size_by_round_values¶

property window_size_full_window_vars¶

property window_size_number_of_full_window¶

property window_size_weight_pr_vars¶

Sat xor differential model¶

Previous topic

Next topic

This Page