Smt xor differential model

class SmtXorDifferentialModel(cipher, counter='sequential')

Bases: SmtModel

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

Build the model for the search of xor differential trails.

INPUT:

  • weight – integer (default: -1); if set to non-negative integer, fixes the xor trail search to a specific weight

  • fixed_variables – list (default: []); dictionaries contain name, bit_size, value (as integer) for the variables that need to be fixed to a certain value | [ | { | ‘component_id’: ‘plaintext’, | ‘constraint_type’: ‘equal’/’not_equal’ | ‘bit_positions’: [0, 1, 2, 3], | ‘binary_value’: [0, 0, 0, 0] | } | ]

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=1)
sage: smt = SmtXorDifferentialModel(speck)
sage: smt.build_xor_differential_trail_model()
calculate_component_weight(component, out_suffix, output_values_dict)
property cipher_id
cipher_input_variables()

Return the list of input variables.

INPUT:

  • None

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtModel(speck)
sage: smt.cipher_input_variables()
['plaintext_0',
 'plaintext_1',
 ...
 'key_62',
 'key_63']
find_all_xor_differential_trails_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='Z3_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 in method

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

See also

SMT standard of Cipher

EXAMPLES:

# single-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: smt = SmtXorDifferentialModel(speck)
sage: trails = smt.find_all_xor_differential_trails_with_fixed_weight(9)
sage: len(trails)
2

# related-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
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: smt = SmtXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trails = smt.find_all_xor_differential_trails_with_fixed_weight(2, fixed_values=[key])
sage: len(trails)
2
find_all_xor_differential_trails_with_weight_at_most(min_weight, max_weight, fixed_values=[], solver_name='Z3_EXT')

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

The list contains 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: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

# single-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: smt = SmtXorDifferentialModel(speck)
sage: trails = smt.find_all_xor_differential_trails_with_weight_at_most(9, 10)
sage: len(trails)
28

# related-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
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: smt = SmtXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trails = smt.find_all_xor_differential_trails_with_weight_at_most(2, 3, fixed_values=[key])
sage: len(trails)
9
find_lowest_weight_xor_differential_trail(fixed_values=[], solver_name='Z3_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: []); they can be created using set_fixed_variables method

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

See also

SMT standard of Cipher

EXAMPLES:

# single-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: smt = SmtXorDifferentialModel(speck)
sage: trail = smt.find_lowest_weight_xor_differential_trail()
sage: trail['total_weight']
9.0

# related-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
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: smt = SmtXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trail = smt.find_lowest_weight_xor_differential_trail(fixed_values=[key])
sage: trail['total_weight']
1.0
find_one_xor_differential_trail(fixed_values=[], solver_name='Z3_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: []); can be created using set_fixed_variables method

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

See also

SMT standard of Cipher

EXAMPLES:

# single-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=5)
sage: smt = SmtXorDifferentialModel(speck)
sage: smt.find_one_xor_differential_trail() # random
{'cipher_id': 'speck_p32_k64_o32_r5',
 'model_type': 'xor_differential',
 'solver_name': 'Z3_EXT',
 'solving_time_seconds': 0.05,
 'memory_megabytes': 19.28,
 ...
 'total_weight': 93,
 'building_time_seconds': 0.002946615219116211}

 # related-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
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: smt = SmtXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: smt.find_one_xor_differential_trail(fixed_values=[key]) # random
find_one_xor_differential_trail_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='Z3_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: cryptominismt); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

# single-key setting
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorDifferentialModel(speck)
sage: trail = smt.find_one_xor_differential_trail_with_fixed_weight(3)
sage: trail['total_weight']
3.0

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
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: smt = SmtXorDifferentialModel(speck)
sage: key = set_fixed_variables(
....:     component_id='key',
....:     constraint_type='not_equal',
....:     bit_positions=range(64),
....:     bit_values=[0]*64)
sage: trail = smt.find_one_xor_differential_trail_with_fixed_weight(3, fixed_values=[key])
sage: trail['total_weight']
3.0
fix_variables_value_constraints(fixed_variables=[])

Return a list of SMT-LIB asserts for fixing variables in CIPHER and XOR DIFFERENTIAL model.

INPUT:

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

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtModel(speck)
sage: smt.fix_variables_value_constraints([set_fixed_variables('plaintext', 'equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (not plaintext_0))',
 '(assert plaintext_1)',
 '(assert (not plaintext_2))',
 '(assert plaintext_3)']
sage: smt.fix_variables_value_constraints([set_fixed_variables('plaintext', 'not_equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (or plaintext_0 (not plaintext_1) plaintext_2 (not plaintext_3)))']
get_operands(solution)
get_xor_probability_constraints(bit_ids, template)
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.smt.smt_model import SmtModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: smt = SmtModel(speck)
sage: smt.model_constraints()
Traceback (most recent call last):
...
ValueError: No model generated
property sboxes_ddt_templates
property sboxes_lat_templates
solve(model_type, solver_name='Z3_EXT')

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

INPUT:

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

    • 'cipher'

    • 'xor_differential'

    • 'xor_linear'

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

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: smt = SmtModel(speck)
sage: smt.solve('xor_differential') # random
{'cipher_id': 'speck_p32_k64_o32_r4',
 'model_type': 'xor_differential',
 'solver_name': 'Z3_EXT',
 'solving_time_seconds': 0.0,
 'memory_megabytes': 0.09,
 'components_values': {},
 'total_weight': None}
update_constraints_for_equal_type(bit_positions, bit_values, component_id, constraints, out_suffix='')
update_constraints_for_not_equal_type(bit_positions, bit_values, component_id, constraints, out_suffix='')
weight_constraints(weight)

Return a variable list and SMT-LIB list asserts representing the fixing of the total weight to the input value.

INPUT:

  • weight – integer; represents the total weight of the trail