Sat xor linear model

class SatXorLinearModel(cipher, counter='sequential', compact=False)

Bases: SatModel

static branch_xor_linear_constraints(bindings)

Return lists of variables and clauses for branch in XOR LINEAR model.

See also

SAT standard of Cipher for the format

INPUT:

  • None

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: SatXorLinearModel.branch_xor_linear_constraints(sat.bit_bindings)
['-plaintext_0_o rot_0_0_0_i',
 'plaintext_0_o -rot_0_0_0_i',
 '-plaintext_1_o rot_0_0_1_i',
 ...
 'xor_2_10_14_o -cipher_output_2_12_30_i',
 '-xor_2_10_15_o cipher_output_2_12_31_i',
 'xor_2_10_15_o -cipher_output_2_12_31_i']
build_generic_sat_model_from_dictionary(component_and_model_types)
build_xor_linear_trail_model(weight=- 1, fixed_variables=[])

Build the linear model.

INPUT:

  • weight – integer (default: -1)

  • fixed_variables – list (default: [])

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: sat = SatXorLinearModel(speck)
sage: sat.build_xor_linear_trail_model()
calculate_component_weight(component, out_suffix, output_values_dict)
property cipher_id
find_all_xor_linear_trails_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return a list of solutions containing all the XOR linear trails having weight equal to fixed_weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail

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:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(1)
sage: len(trails) == 4
True

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key])
sage: len(trails) == 8
True
find_all_xor_linear_trails_with_weight_at_most(min_weight, max_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return a list of solutions. By default, the search removes the key schedule, if any.

The list contains all the XOR linear 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: []); can be created using set_fixed_variables method

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

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 2) # long
sage: len(trails) == 187
True

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) # long
sage: len(trails) == 73
True
find_lowest_weight_xor_linear_trail(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return the solution representing a XOR LINEAR trail with the lowest possible weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

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_linear_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:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trail = sat.find_lowest_weight_xor_linear_trail()
sage: trail['total_weight']
1.0

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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(block_bit_size=16, key_bit_size=32, number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32)
sage: trail = sat.find_lowest_weight_xor_linear_trail(fixed_values=[key])
sage: trail['total_weight']
3.0
find_one_xor_linear_trail(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return the solution representing a XOR linear trail. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

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:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: sat.find_one_xor_linear_trail() # random
{'cipher_id': 'speck_p32_k64_o32_r4',
 'model_type': 'xor_linear',
 'solver_name': 'cryptominisat',
 'solving_time_seconds': 0.01,
 'memory_megabytes': 7.2,
 ...
 'status': 'SATISFIABLE',
 'building_time_seconds': 0.010079622268676758}

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64)
sage: sat.find_one_xor_linear_trail(fixed_values=[key]) # random
find_one_xor_linear_trail_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return the solution representing a XOR linear trail whose weight is fixed_weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

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:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trail = sat.find_one_xor_linear_trail_with_fixed_weight(7)
sage: trail['total_weight']
7.0

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trail = sat.find_one_xor_linear_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']
static fix_variables_value_xor_linear_constraints(fixed_variables=[])

Return lists variables and clauses for fixing variables in XOR LINEAR model.

See also

SAT standard of Cipher for the format

INPUT:

  • fixed_variables – list (default: []); variables in default format

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(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: SatXorLinearModel.fix_variables_value_xor_linear_constraints(fixed_variables)
['plaintext_0_o',
 '-plaintext_1_o',
 'plaintext_2_o',
 'plaintext_3_o',
 '-ciphertext_0_o -ciphertext_1_o -ciphertext_2_o ciphertext_3_o']
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'])
weight_xor_linear_constraints(weight)