Sat cipher model

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

Bases: SatModel

build_cipher_model(fixed_variables=[])

Build the sat model.

INPUT:

  • 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_cipher_model import SatCipherModel
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: sat = SatCipherModel(speck)
sage: sat.build_cipher_model()
build_generic_sat_model_from_dictionary(fixed_variables, component_and_model_types)
calculate_component_weight(component, out_suffix, output_values_dict)
property cipher_id
find_missing_bits(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return the solution representing a generic flow of the cipher from plaintext and key to ciphertext.

INPUT:

  • fixed_values – list (default: []); can be created using set_fixed_variables method

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

See also

SAT Solvers

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: from claasp.cipher_modules.models.sat.sat_models.sat_cipher_model import SatCipherModel
sage: sat = SatCipherModel(speck)
sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
sage: ciphertext = set_fixed_variables(
....:         component_id=speck.get_all_components_ids()[-1],
....:         constraint_type='equal',
....:         bit_positions=range(32),
....:         bit_values=integer_to_bit_list(endianness='big', list_length=32, int_value=0xaffec7ed))
sage: sat.find_missing_bits(fixed_values=[ciphertext]) # random
{'cipher_id': 'speck_p32_k64_o32_r22',
 'model_type': 'cipher',
 'solver_name': 'CRYPTOMINISAT_EXT',
 ...
  'intermediate_output_21_11': {'value': '1411'},
  'cipher_output_21_12': {'value': 'affec7ed'}},
 'total_weight': None,
 'status': 'SATISFIABLE',
 'building_time_seconds': 0.019376516342163086}
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
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'])