Smt cipher model

class SmtCipherModel(cipher, counter='sequential')

Bases: SmtModel

build_cipher_model(fixed_variables=[])

Build the cipher model.

INPUT:

  • 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_cipher_model import SmtCipherModel
sage: speck = SpeckBlockCipher(number_of_rounds=1)
sage: smt = SmtCipherModel(speck)
sage: smt.build_cipher_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_missing_bits(fixed_values=[], solver_name='Z3_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: z3); the name of the solver

See also

SMT standard of Cipher

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.smt.smt_models.smt_cipher_model import SmtCipherModel
sage: smt = SmtCipherModel(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: smt.find_missing_bits(fixed_values=[ciphertext]) # random
{'cipher_id': 'speck_k64_p32_o32_r22',
 'model_type': 'speck_k64_p32_o32_r22',
 'solver_name': 'Z3_EXT',
 ...
  'intermediate_output_21_11': {'value': '90fe', 'weight': 0},
  'cipher_output_21_12': {'value': 'affec7ed', 'weight': 0}},
 'total_weight': None}
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_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