Sat truncated xor differential model

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

Bases: SatModel

build_generic_sat_model_from_dictionary(component_and_model_types)

calculate_component_weight(component, out_suffix, output_values_dict)

property cipher_id

static fix_variables_value_constraints(fixed_variables=[])

Return constraints for fixed variables

Return lists of variables and clauses for fixing variables in semi deterministic truncated XOR differential model.

See also

set_fixed_variables()

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_models.sat_semi_deterministic_truncated_xor_differential_model import SatSemiDeterministicTruncatedXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatSemiDeterministicTruncatedXorDifferentialModel(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': [2, 1, 1, 0]
....: }]
sage: list_of_constraints = SatSemiDeterministicTruncatedXorDifferentialModel.fix_variables_value_constraints(fixed_variables)
sage: expected_set_of_constraints = set(['-plaintext_0_0',
....: 'plaintext_0_1',
....: '-plaintext_1_0',
....: '-plaintext_1_1',
....: '-plaintext_2_0',
....: 'plaintext_2_1',
....: '-plaintext_3_0',
....: 'plaintext_3_1',
....: '-ciphertext_0_0 ciphertext_0_1',
....: '-ciphertext_0_0 -ciphertext_0_1',
....: 'ciphertext_1_0 -ciphertext_1_1 ciphertext_2_0 -ciphertext_2_1 ciphertext_3_0 ciphertext_3_1'])
sage: set(list_of_constraints) == expected_set_of_constraints
True

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