cascada.smt.chsearch module

Search for characteristics by modeling the search as a sequence of SMT problems.

`INCREMENT_NUM_ROUNDS`	Message to increase the current number of rounds by one (see `round_based_ch_search`)
`ChModelAssertType`	Represent the options available for the type of constraints of the characteristic model.
`PrintingMode`	Represent the options available for the information to print.
`MissingVarWarning`	The class of warnings when a variable from an additional constraint is missing in the SMT problem (see `ChFinder`).
`ChFinder`	Search for characteristics by modeling the search as a sequence of SMT problems.
`CipherChFinder`	Search for cipher characteristics by modeling the search as a sequence of SMT problems.
`round_based_ch_search`	Search for characteristics of round-based functions over multiple number of rounds.
`round_based_cipher_ch_search`	Search for characteristics of iterated ciphers over multiple number of rounds.

cascada.smt.chsearch.INCREMENT_NUM_ROUNDS = 'increment_num_rounds': Message to increase the current number of rounds by one (see round_based_ch_search)

class cascada.smt.chsearch.ChModelAssertType(value)[source]

Bases: enum.Enum

Represent the options available for the type of constraints of the characteristic model.

ValidityAndWeight: consider abstractproperty.chmodel.ChModel.validity_assertions and abstractproperty.chmodel.ChModel.weight_assertions

ProbabilityOne: only consider abstractproperty.chmodel.ChModel.pr_one_assertions

Validity: only consider abstractproperty.chmodel.ChModel.validity_assertions

class cascada.smt.chsearch.PrintingMode(value)[source]

Bases: enum.Enum

Represent the options available for the information to print.

Silent: nothing is printed

WeightsAndSrepr: prints every time the target weight is increased or the final weight is modified, and prints the abstractproperty.characteristic.Characteristic.srepr method of all non-returned characteristics (together with the current time)

WeightsAndVrepr: similar as WeightsAndSrepr, but the abstractproperty.characteristic.Characteristic.vrepr method is printed instead.

Debug: similar as WeightsAndSrepr, but also prints all the constraints generated during the search

exception cascada.smt.chsearch.MissingVarWarning[source]

Bases: UserWarning

The class of warnings when a variable from an additional constraint is missing in the SMT problem (see ChFinder).

class cascada.smt.chsearch.ChFinder(ch_model, assert_type, solver_name, initial_constraints=None, exclude_zero_input_prop=False, var_prop2ct_prop=None, raise_exception_missing_var=True, printing_mode=PrintingMode.Silent, filename=None, weight_prefix='w', solver_seed=None, env=None)[source]

Bases: object

Search for characteristics by modeling the search as a sequence of SMT problems.

Given a characteristic model (abstractproperty.chmodel.ChModel o abstractproperty.chmodel.EncryptionChModel) defined for a particular Property (e.g., XorDiff or LinearMask), this class finds characteristics (abstractproperty.characteristic.Characteristic o abstractproperty.characteristic.EncryptionCharacteristic) satisfying the characteristic model by modelling the search as a sequence of SMT problems in the bit-vector theory.

Depending on assert_type, the SMT problems contain the validity, probability-one and/or weight assertions from the abstractproperty.chmodel.ChModel. They might also contain a constraint fixing the characteristic weight variable to a constant value (in the case of find_next_ch_increasing_weight) or additional constraints provided in initial_constraints or derived from var2ct_prop or exclude_zero_input_prop.

Note

The optional initialization argument var2ct_prop is a collections.OrderedDict mapping symbolic properties of the characteristic model to constant values. From each (sp, cp) pair in var2ct_prop, where sp is a symbolic Property and cp a constant Property, the constraint sp == cp is added to initial_constraints. The dictionary var2ct_prop can also be filled with pairs of symbolic Term and Constant objects; in this case, they are first automatically converted to Property objects.

If exclude_zero_input_prop is True, and additional constraint is added preventing the input property to be zero.

By defaut, an exception is raised if an additional constraint (one of the constraint from initial_constraints or one of the constraints derived from var2ct_prop or exclude_zero_input_prop) contains a variable that does not appear in the SMT problem (i.e., chmodel_asserts). If the initialization argument raise_exception_missing_var is False, a warning with category MissingVarWarning is printed instead of raising an exception.

Note

If ch_model is an algebraic characteristic model (defined for the property BitValue or WordValue), the assertion type ValidityAndWeight in assert_type is not supported (and Validity and ProbabilityOne are equivalent due to the definition of characteristic probability, see also algebraic.chmodel.ChModel).

If the algebraic characteristic model does not contain external variables and a ciphertext value is provided in var2ct_prop or initial_constraints, then the search for algebraic characteristics is equivalent to the search for preimages of the given ciphertext value. On the other hand, if the algebraic characteristic model contains external variables (e.g., round keys) and a plaintext-ciphertext pair is provided in var2ct_prop or initial_constraints, then the search for algebraic characteristics is equivalent to the search for the external values (e.g., round keys) that make the underlying bit-vector function maps the given plaintext to the given ciphertext.

The SMT problems are solved through pySMT, which calls an off-the-shelf SMT solver supported by pySMT given by solver_name (e.g., solver_name='btor' sets Boolector as the SMT solver). The pySMT documentation explains how to install an SMT solver.

This class provides three methods to search for characteristics: find_next_ch, find_next_ch_increasing_weight and find_next_ch_increasing_weight_fixed_in_out. These methods are Python generator functions, returning an iterator that yields the abstractproperty.characteristic.Characteristic objects found in the search (see also this). The characteristics returned are defined for the Property of the characteristic model.

Note

The characteristics can be obtained in a for-loop over the iterator or retrieved one at a time with the next function, that is,

[...]
ch_finder = ChFinder(...)
iterator = ch_finder.search_all()
first_ch_found = next(iterator)
for next_ch_found in iterator:
    [...]

If next is used but not characteristic is found, an StopIteration exception is raised.

>>> # example of SMT problem of XorDiff-EncryptionCharacteristic of Speck32
>>> from cascada.bitvector.core import Variable
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.chsearch import ChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = EncryptionChModel(Speck32, XorDiff)
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> ch_finder = ChFinder(ch_model, assert_type, "btor", exclude_zero_input_prop=True, solver_seed=0)
>>> ch_finder.formula_size()
801
>>> print(ch_finder.hrepr(full_repr=False))  
; initial constraints
assert ~((dp0 :: dp1) == 0x00000000)
; characteristic model assertions
assert ((~(... << ...) ^ (dp1 << 0x0001)) & (~(... << ...) ^ (dx1 << 0x0001)) &
    ((... >>> ...) ^ dp1 ^ dx1 ^ ((dp0 >>> 7) << 0x0001))) == 0x0000
assert ((~(... << ...) ^ ((... ^ ...) << 0x0001)) & (~(... << ...) ^ (dx6 << 0x0001)) &
    ((... >>> ...) ^ ... ^ ... ^ dx6 ^ ((dx1 >>> 7) << 0x0001))) == 0x0000
assert dx6 == dx7_out
assert ((((dp1 <<< 2) ^ dx1) <<< 2) ^ dx6) == dx9_out
assert w0 == PopCount(~((~... ^ dp1) & (~... ^ dx1))[14:])
assert w1 == PopCount(~((~... ^ ... ^ ...) & (~... ^ dx6))[14:])
assert w2 == 0b0
assert w3 == 0b0
assert w == ((0b0 :: w0) + (0b0 :: w1))

>>> # example of SMT problem of LinearMask-Characteristic of Speck32.key_schedule
>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.smt.chsearch import ChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> v2c = {ch_model.input_mask[2]: core.Constant(0, 16)}  # setting input_mask[2] to 0
>>> at = ChModelAssertType.ProbabilityOne
>>> ch_finder = ChFinder(ch_model, at, "btor", var_prop2ct_prop=v2c, solver_seed=0)
>>> ch_finder.formula_size()
80
>>> print(ch_finder.hrepr(full_repr=False))  
; initial constraints
assert mk2 == 0x0000
; characteristic model assertions
assert (~((mx1 ^ (... >>> ...)) | (mx1 ^ mk2__0)) == 0xffff) &
    (((mx1 ^ (mk1 >>> 7) ^ mk2__0)[:1]) == 0b000000000000000)
assert ((mk2__1 <<< 2) == mx1) & ((mk2__1 <<< 2) == mx3)
assert (~((mx5 ^ (... >>> ...)) | (mx5 ^ mx3__0)) == 0xffff) &
    (((mx5 ^ (mk0 >>> 7) ^ mx3__0)[:1]) == 0b000000000000000)
assert ((mx3__1 <<< 2) == mx5) & ((mx3__1 <<< 2) == mx8)
assert (mk2 ^ mk2__0 ^ mk2__1) == mk2_out
assert (mx3 ^ mx3__0 ^ mx3__1) == mx3_out
assert mx8 == mx8_out

ch_model: the underlying characteristic model (a subclass of abstractproperty.chmodel.ChModel or abstractproperty.chmodel.EncryptionChModel)

assert_type: the type of assertions (an element from ChModelAssertType)

solver_name: the pySMT solver name

initial_constraints: the list of additional constraints (given as Term) to add to the SMT problems (by default an empty list)

printing_mode: the information to print (an element of PrintingMode, by default PrintingMode.Silent)

filename: the filename where the messages will be printed (by default the standard output is used)

weight_prefix: the prefix to label the weight variables

solver_seed: the seed for the SMT solver

env: the associated pysmt.environment.Environment (by default a new one is created)

chmodel_asserts: the list containing the main assertions (Term objects) common to the SMT problems

find_next_ch(yield_assignment=False)[source]

Return an iterator that yields the characteristics found in the SMT-based search.

Note

This method requires that assert_type is either Validity or ProbabilityOne (and not ValidityAndWeight).

This method searches for characteristic using SMT solvers. The decision problem of whether there exists a characteristic (following the characteristic model ch_model) is encoded as an SMT problem and given to the SMT solver, which checks its satisfiability.

If the SMT solver finds the first problem satisfiable, an assignment of the variables that makes the problem satisfiable is obtained, and a abstractproperty.characteristic.Characteristic object is created and yielded.

Note

If yield_assignment is True, the assignment (as a dictionary mapping Variable to Constant objects) is yielded instead of the characteristic.

Afterwards, an additional constraint is added to the SMT problem to exclude the characteristic yielded and this procedure is repeated until all characteristics are found.

>>> # example of search for LinearMask-Characteristic of Speck32.key_schedule
>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.smt.chsearch import ChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> v2c = {ch_model.input_mask[2]: core.Constant(0, 16)}  # setting input_mask[2] to 0
>>> at = ChModelAssertType.ProbabilityOne
>>> ch_finder = ChFinder(ch_model, at, "btor", var_prop2ct_prop=v2c, solver_seed=0)
>>> for ch in ch_finder.find_next_ch(): print(ch.srepr()) # all 2-rounds probability-one trails
Ch(w=0, id=0000 0000 0000, od=0000 0000 0000)
Ch(w=0, id=0080 0080 0000, od=4001 4000 0001)
Ch(w=0, id=0080 0000 0000, od=0000 4001 0001)
Ch(w=0, id=0000 0080 0000, od=4001 0001 0000)
>>> # example of search for BitValue-EncryptionCharacteristic of Speck32
>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.chmodel import EncryptionChModel
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = EncryptionChModel(Speck32, BitValue)
>>> input_output_vals = ch_model.input_val + ch_model.output_val
>>> # setting each input and output word to 0x0001
>>> v2c = {v: core.Constant(1, 16) for v in input_output_vals}
>>> at = ChModelAssertType.Validity
>>> ch_finder = ChFinder(ch_model, at, "btor", var_prop2ct_prop=v2c, solver_seed=0)
>>> found_ch = next(ch_finder.find_next_ch())
>>> round_sep = found_ch.get_round_separators()
>>> for round_ch in found_ch.split(round_sep): print(round_ch)  
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0],
    input_val=[0x0001, 0x0001], output_val=[0x0004, 0x0000], external_vals=[0x0205],
    assign_outval_list=[0x0201, 0x0004, 0x0000])
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0],
    input_val=[0x0004, 0x0000], output_val=[0x0001, 0x0001], external_vals=[0x0801],
    assign_outval_list=[0x0800, 0x0001, 0x0001])

find_next_ch_increasing_weight(initial_weight, final_weight=None, empirical_weight_options=None, stop_after_optimal=True, yield_weight=False)[source]

Return an iterator that yields the characteristics found in the SMT-based search with increasing weight order.

Note

This method requires that assert_type is ValidityAndWeight (and not Validity nor ProbabilityOne).

This method searches for optimal characteristics (with optimal probability) using SMT solvers as follows.

First, the probability space is decomposed into many intervals \(I_w = (2^{-w-1}, 2^{-w}]\), where w = initial_weight, initial_weight + 1, ..., final_weight. For each interval, the decision problem of whether there exists a characteristic (following the characteristic model ch_model) with probability \(p \in I_w\) is encoded as an SMT problem. Note that a characteristic has probability \(p \in I_w\) if and only if its integer weight (the integer part of the weight) is equal to \(w\).

Note

See abstractproperty.characteristic.Characteristic for the characteristic probability and weight considered here.

The SMT problems are provided to the SMT solver, which checks their satisfiability in increasing weight order. When the SMT solver finds the first satisfiable problem, an assignment of the variables that makes the problem satisfiable is obtained, and a abstractproperty.characteristic.Characteristic object is created and yielded.

Note

If yield_weight is True, a tuple is yielded instead, containing the target weight \(w\) and the characteristic.

If empirical_weight_options is provided, before yielding the characteristic, the empirical weight of the characteristic is computed by calling the method abstractproperty.characteristic.Characteristic.compute_empirical_ch_weight with the given options as arguments (see below for an explanation of empirical_weight_options). Importantly, if the empirical weight computed is math.inf, this characteristic is NOT yielded and the search continues. If empirical_weight_options is not provided, all characteristics found are yielded.

If the error bound of the associated characteristic model (see abstractproperty.chmodel.ChModel.error) is zero, the first characteristic yielded is optimal in the sense that there are no characteristics with integer weight strictly smaller, and the search finishes (if stop_after_optimal is True, otherwise it continues until all characteristics are found).

Note

Note the first characteristic yielded is optimal for the characteristic probability here considered, which might be an approximation of the actual characteristic probability (e.g., see differential.characteristic.Characteristic or linear.characteristic.Characteristic).

Let \(\hat{w}\) the weight of the first characteristic yielded. If the error bound of the associated characteristic model is \(e > 0\), then the search continues yielding all characteristics with weights between \(\hat{w}\) and \(\hat{w} + e\). After all these characteristics have been yielded, the optimal characteristic (the characteristic among all yielded characteristics with the lowest abstractproperty.characteristic.Characteristic.ch_weight) is yielded again and the search finishes (if stop_after_optimal is True, otherwise it continues until all characteristics are found).

Note

After the iterator is exhausted, the last characteristic yielded is always the optimal, but the optimal characteristic is only yielded twice if it is different from the previous characteristic yielded.

Moreoever, if yield_weight is True, the second time the optimal characteristic is yielded a tuple is also yielded, but the first entry in the tuple contains None (the target weight of the optimal characteristic is yielded the first time the optimal characteristic is yielded).

>>> # example of search for XorDiff-EncryptionCharacteristic of Speck32
>>> from cascada.bitvector.core import Variable
>>> from cascada.differential.difference import XorDiff, RXDiff
>>> from cascada.differential.chmodel import ChModel, EncryptionChModel
>>> from cascada.smt.chsearch import ChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = EncryptionChModel(Speck32, XorDiff)
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> ch_finder = ChFinder(ch_model, assert_type, "btor", solver_seed=0)
>>> # no need to exclude the input zero XOR difference if initial_weight != 0
>>> ewo = {"seed": 0}  # no need to specify all args
>>> next(ch_finder.find_next_ch_increasing_weight(1, empirical_weight_options=ewo))  
EncryptionCharacteristic(ch_weight=1, empirical_ch_weight=1.027020213933709037746664618,
    assignment_weights=[1, 0, 0, 0],
    input_diff=[0x0010, 0x2000], output_diff=[0x8000, 0x8002], external_diffs=[0x0000, 0x0000],
    assign_outdiff_list=[0x0000, 0x8000, 0x8000, 0x8002])
>>> # example of search for RXDiff-Characteristic of Speck32.key_schedule
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, RXDiff, ["dmk0", "dmk1", "dmk2"])
>>> dmk0, dmk1 = ch_model.input_diff[:2]
>>> v2c = {dmk0: core.Constant(0, 16), dmk1: core.Constant(0, 16)}
>>> ch_finder = ChFinder(ch_model, assert_type, "btor", var_prop2ct_prop=v2c, solver_seed=0)
>>> for ch in ch_finder.find_next_ch_increasing_weight(1): print(ch.srepr())  
Ch(w=2.830, id=0000 0000 0000, od=0000 0001 0007)
...
Ch(w=3.830, id=0000 0000 8000, od=8000 8002 800b)
...
Ch(w=4.830, id=0000 0000 0001, od=0001 0005 001b)
...
Ch(w=4.830, id=0000 0000 8000, od=8000 8002 800e)
Ch(w=2.830, id=0000 0000 0000, od=0000 0001 0007)

Parameters

initial_weight – the initial weight to start the search
final_weight – the last weight to consider in the search (by default math.inf)
empirical_weight_options – (optional) a dictionary containing the arguments of abstractproperty.characteristic.Characteristic.compute_empirical_ch_weight (used similar as **kwargs, that is, compute_empirical_ch_weight(**empirical_weight_options)
yield_weight – if True, the target weight of the SMT problem is also yielded (default False)

find_next_ch_increasing_weight_fixed_in_out(input_prop, output_prop, initial_weight, final_weight=None, empirical_weight_options=None, use_empirical_weight=False)[source]

Return an iterator that yields the characteristics found in the SMT-based search with increasing weight order and with fixed input and output properties.

This method is similar as find_next_ch_increasing_weight with three differences:

This method only finds characteristics with input and output properties (Characteristic.input_prop and Characteristic.output_prop) equal to the input and output properties given by input_prop and output_prop (lists containing Constant objects or constant Property objects).

When the SMT solver finds a satisfiable problem, a tuple of two elements is yielded: the first element is the cumulative weight and the second element is the characteristic found (as a abstractproperty.characteristic.Characteristic object). The cumulative weight is the weight (-log2) of the sum of the probabilities of all characteristics found in the search (including the characteristic just found).

After all these characteristics have been yielded, the optimal characteristic is NOT yielded again.

By default, the cumulative weight is computed by taking the decimal weights (see Characteristic.ch_weight) of the found characteristic, transforming the decimal weights into probabitlies, then summing these probabilities and finally transforming the probability sum into a weight. However, if the argument empirical_weight_options is given (see find_next_ch_increasing_weight) and the argument use_empirical_weight is True, then the empirical weights are used instead of the decimal weights.

Note

For the Difference/LinearMask property types, the cumulative weight estimates the weight of the probability of the differential/hull with the given input and output differences/masks.

>>> # example of search for XorDiff-EncryptionCharacteristic of Speck32 with fixed input/output difference
>>> from cascada.bitvector.core import Constant
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.chsearch import ChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(4)
>>> ch_model = EncryptionChModel(Speck32, XorDiff)
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> ch_finder = ChFinder(ch_model, assert_type, "btor", solver_seed=0)
>>> best_ch = next(ch_finder.find_next_ch_increasing_weight(1))
>>> best_ch  
EncryptionCharacteristic(ch_weight=5, assignment_weights=[2, 0, 1, 2, 0, 0],
    input_diff=[0x2800, 0x0010], output_diff=[0x8000, 0x840a], external_diffs=[0x0000, 0x0000, 0x0000, 0x0000],
    assign_outdiff_list=[0x0040, 0x8000, 0x8100, 0x8000, 0x8000, 0x840a])
>>> iterator = ch_finder.find_next_ch_increasing_weight_fixed_in_out
>>> # using the input and output differences of the best 5-round characteristic
>>> for w, ch in iterator(best_ch.input_prop, best_ch.output_prop, 0): print(w, "|", ch)  
5 | EncryptionCharacteristic(ch_weight=5, assignment_weights=[2, 0, 1, 2, 0, 0],
    input_diff=[0x2800, 0x0010], output_diff=[0x8000, 0x840a], external_diffs=[0x0000, 0x0000, 0x0000, 0x0000],
    assign_outdiff_list=[0x0040, 0x8000, 0x8100, 0x8000, 0x8000, 0x840a])
4.999999999916024096260838242 | EncryptionCharacteristic(ch_weight=39, assignment_weights=[6, 13, 11, 9, 0, 0],
    input_diff=[0x2800, 0x0010], output_diff=[0x8000, 0x840a], external_diffs=[0x0000, 0x0000, 0x0000, 0x0000],
    assign_outdiff_list=[0x03a0, 0x4f1f, 0x837f, 0x8000, 0x8000, 0x840a])
...
4.999999999894210043141894841 | EncryptionCharacteristic(ch_weight=49, assignment_weights=[10, 15, 10, 14, 0, 0],
    input_diff=[0x2800, 0x0010], output_diff=[0x8000, 0x840a], external_diffs=[0x0000, 0x0000, 0x0000, 0x0000],
    assign_outdiff_list=[0x3fa0, 0xa00f, 0xff3f, 0x8000, 0x8000, 0x840a])
>>> print(w)  # weight of differential
4.999999999894210043141894841

formula_size(measure=None)[source]

Return the size of the underlying SMT problem.

See pysmt.oracles.SizeOracle for choosing measure.

hrepr(full_repr=False)[source]

Return a human-readable representation of the base SMT problem.

The base SMT problem is the SMT problem containing the validity, probability-one and/or weight assertions (depending on assert_type) and the additional constraints from initial_constraints, but excluding constraints created during the search such as the constraints fixing the characteristic weight variable to a constant value in find_next_ch_increasing_weight or the constraints fixing the input and output properties in find_next_ch_increasing_weight_fixed_in_out.

If full_repr is False, the short string representation srepr is used.

class cascada.smt.chsearch.CipherChFinder(ch_model, ks_assert_type, enc_assert_type, solver_name, initial_constraints=None, ks_exclude_zero_input_prop=False, enc_exclude_zero_input_prop=False, var_prop2ct_prop=None, raise_exception_missing_var=True, printing_mode=PrintingMode.Silent, filename=None, ks_weight_prefix='wk', enc_weight_prefix='we', solver_seed=None, env=None)[source]

Bases: cascada.smt.chsearch.ChFinder

Search for cipher characteristics by modeling the search as a sequence of SMT problems.

Given a characteristic model of a Cipher (abstractproperty.chmodel.CipherChModel) defined for a particular Property (e.g., XorDiff or BitValue), this class finds characteristics (abstractproperty.characteristic.CipherCharacteristic) satisfying the characteristic model by modelling the search as a sequence of SMT problems in the bit-vector theory.

To initialize a CipherChFinder object, first two auxiliary instances of ChFinder are created:

ks_finder: a ChFinder with arguments ch_model.ks_ch_model, ks_assert_type ks_exclude_zero_input_prop and ks_weight_prefix
enc_finder: a ChFinder with arguments ch_model.enc_ch_model, enc_assert_type, enc_exclude_zero_input_prop amd enc_weight_prefix

Both ks_finder and enc_finder (together with the CipherChFinder object) share the arguments solver_name, printing_mode, filename, solver_seed and env.

Then, these two auxiliary ChFinder objects are merged into a CipherChFinder (which is also an instance of ChFinder) as follows:

solver_name, printing_mode, filename, solver_seed env are the same as the ones from ks_finder and enc_finder
ch_model is set to the characteristic model of the cipher (a subclass of abstractproperty.chmodel.CipherChModel)
assert_type is set as the largest assertion type, following the order ValidityAndWeight > Validity > ProbabilityOne
initial_constraints contains all initial constraints (including the ones derived from ks_exclude_zero_input_prop, enc_exclude_zero_input_prop and var_prop2ct_prop)
chmodel_asserts is the union of chmodel_asserts of ks_finder and enc_finder

See also ChFinder.find_next_ch.

>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.chmodel import CipherChModel
>>> from cascada.smt.chsearch import CipherChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = CipherChModel(Speck32, BitValue)
>>> input_output_vals = ch_model.enc_ch_model.input_val + ch_model.enc_ch_model.output_val
>>> # setting each input and output plaintext word to 0x0001
>>> v2c = {v: core.Constant(1, 16) for v in input_output_vals}
>>> assert_type = ChModelAssertType.Validity
>>> ch_finder = CipherChFinder(ch_model, assert_type, assert_type, "btor",
...                            var_prop2ct_prop=v2c, solver_seed=0)
>>> found_enc_ch = next(ch_finder.find_next_ch()).enc_characteristic
>>> round_sep = found_enc_ch.get_round_separators()
>>> for round_enc_ch in found_enc_ch.split(round_sep): print(round_enc_ch)  
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0],
    input_val=[0x0001, 0x0001], output_val=[0x0004, 0x0000], external_vals=[0x0205],
    assign_outval_list=[0x0201, 0x0004, 0x0000])
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0],
    input_val=[0x0004, 0x0000], output_val=[0x0001, 0x0001], external_vals=[0x0801],
    assign_outval_list=[0x0800, 0x0001, 0x0001])

fix_key_schedule_ch_weight(integer_weight)[source]: Add the constraint that fixes the key-schedule weight to the given integer weight.

fix_encryption_ch_weight(integer_weight)[source]: Add the constraint that fixes the encryption weight to the given integer weight.

find_next_ch_increasing_weight(initial_weight, final_weight=None, ks_empirical_weight_options=None, enc_empirical_weight_options=None, stop_after_optimal=True, yield_weight=False)[source]

Return an iterator that yields the characteristics found in the SMT-based search.

This method searches for optimal characteristics (with optimal probability) using SMT solvers (see ChFinder).

In particular, the search creates decision problems of whether there exists a characteristic with probability \(p \in I_w\), where a characteristic has probability \(p \in I_w\) if and only if its integer weight (the integer part of the weight) is equal to \(w\).

The main difference between ChFinder.find_next_ch_increasing_weight and this method is that this method defined the weight of a CipherCharacteristic depending on the type of the assertions.

If both ks_assert_type and enc_assert_type are ValidityAndWeight, then the weight of a CipherCharacteristic is defined as the sum of the weight of the key-schedule characteristic and the weight of the encryption characteristic.
If only ks_assert_type is ValidityAndWeight, then the weight is defined as the weight of the key-schedule characteristic.
If only enc_assert_type is ValidityAndWeight, then the weight is defined as the weight of the encryption characteristic.

Note

For example, if only enc_assert_type is ValidityAndWeight, the search starts finding characteristics where the integer weight of the encryption characteristic is equal to the initial weight.

The argument ks_empirical_weight_options (resp. enc_empirical_weight_options) specifies the options for the computation of the empirical weight over the key-schedule (resp. encryption) characteristic. If only one of them is given (and the other one is None), then only one of the empirical weights is computed and used to determine whether to yield the characteristic found.

>>> # example of search for RXDiff-CipherCharacteristic of Speck32
>>> from cascada.differential.difference import RXDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.chsearch import CipherChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = CipherChModel(Speck32, RXDiff)
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> ch_finder = CipherChFinder(ch_model, assert_type, assert_type, "btor", solver_seed=0)
>>> iterator = ch_finder.find_next_ch_increasing_weight(1)
>>> print(next(iterator).srepr())
Ch(ks_ch=Ch(w=1.415, id=0000 0000, od=0000 0000), enc_ch=Ch(w=2.830, id=0000 0000, od=0000 0000))
>>> print(next(iterator).srepr())
Ch(ks_ch=Ch(w=1.415, id=0000 8000, od=8000 8002), enc_ch=Ch(w=2.830, id=0040 0000, od=8003 8003))

find_next_ch_increasing_weight_fixed_in_out(ks_input_prop, enc_input_prop, enc_output_prop, initial_weight, final_weight=None, ks_empirical_weight_options=None, enc_empirical_weight_options=None, use_empirical_weight=False)[source]

Return an iterator that yields the characteristics found in the SMT-based search with increasing weight order and with fixed input and output properties.

Note

This method requires that both``ks_assert_type`` and enc_assert_type are ValidityAndWeight.

This method is similar to ChFinder.find_next_ch_increasing_weight_fixed_in_out, but internally CipherChFinder.find_next_ch_increasing_weight is used instead of ChFinder.find_next_ch_increasing_weight.

In particular, this method finds cipher characteristics with the key-schedule input property, the encryption input property and the encryption output property equal to the properties given by ks_input_prop, enc_input_prop and enc_output_prop (lists containing Constant objects or constant Property objects).

Note that the cumulative weight is the weight (-log2) of the sum of the probabilities of all cipher characteristics found in the search (including the characteristic just found), where the probability of a cipher characteristic here considered is the product of the probabilities of the key-schedule and encryption characteristics. In other words, the cumulative weight is computed as in ChFinder.find_next_ch_increasing_weight_fixed_in_out, but the decimal weight of a cipher characteristic is taken as the sum of the decimal weights of the key-schedule and the encryption characteristics.

Note

For the Difference property types, the cumulative weight estimates the weight of the probability of the related-key differential with given masterkey difference, plaintext difference and ciphertext difference.

>>> # example of search for RXDiff-CipherCharacteristic of Speck32 with fixed input/output difference
>>> from cascada.differential.difference import RXDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.chsearch import CipherChFinder, ChModelAssertType
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = CipherChModel(Speck32, RXDiff)
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> ch_finder = CipherChFinder(ch_model, assert_type, assert_type, "btor", solver_seed=0)
>>> best_ch = next(ch_finder.find_next_ch_increasing_weight(1))
>>> best_ch.ks_characteristic.ch_weight + best_ch.enc_characteristic.ch_weight
Decimal('4.244980417176049505485850841')
>>> best_ch  
CipherCharacteristic(ks_characteristic=Characteristic(ch_weight=1.414993472392016501828616947,
    assignment_weights=[1.414993472392016501828616947, 0, 0],
    input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000],
    assign_outdiff_list=[0x0000, 0x0000, 0x0000]),
enc_characteristic=Characteristic(ch_weight=2.829986944784033003657233894,
    assignment_weights=[1.414993472392016501828616947, 1.414993472392016501828616947, 0, 0],
    input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000], external_diffs=[0x0000, 0x0000],
    assign_outdiff_list=[0x0000, 0x0000, 0x0000, 0x0000]))
>>> iterator = ch_finder.find_next_ch_increasing_weight_fixed_in_out
>>> # using the input and output differences of the best 2-round characteristic
>>> ks_ip = best_ch.ks_characteristic.input_prop
>>> enc_ip, enc_op = best_ch.enc_characteristic.input_prop, best_ch.enc_characteristic.output_prop
>>> for w, ch in iterator(ks_ip, enc_ip, enc_op, 1): print(w, "|", ch)  
4.244980417176049505485850841 | CipherCharacteristic(ks_characteristic=Characteristic(ch_weight=1.414993472392016501828616947,
        assignment_weights=[1.414993472392016501828616947, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000],
        assign_outdiff_list=[0x0000, 0x0000, 0x0000]),
    enc_characteristic=Characteristic(ch_weight=2.829986944784033003657233894,
        assignment_weights=[1.414993472392016501828616947, 1.414993472392016501828616947, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000], external_diffs=[0x0000, 0x0000],
        assign_outdiff_list=[0x0000, 0x0000, 0x0000, 0x0000]))
3.244980417176049505485850840 | CipherCharacteristic(ks_characteristic=Characteristic(ch_weight=1.414993472392016501828616947,
        assignment_weights=[1.414993472392016501828616947, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0001],
        assign_outdiff_list=[0x0001, 0x0000, 0x0001]),
    enc_characteristic=Characteristic(ch_weight=2.829986944784033003657233894,
        assignment_weights=[1.414993472392016501828616947, 1.414993472392016501828616947, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000], external_diffs=[0x0000, 0x0001],
        assign_outdiff_list=[0x0000, 0x0001, 0x0000, 0x0000]))
...
3.192516141583136911276041810 | CipherCharacteristic(ks_characteristic=Characteristic(ch_weight=17,
        assignment_weights=[17, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x7fff],
        assign_outdiff_list=[0x7fff, 0x0000, 0x7fff]),
    enc_characteristic=Characteristic(ch_weight=18.41499347239201650182861695,
        assignment_weights=[1.414993472392016501828616947, 17, 0, 0],
        input_diff=[0x0000, 0x0000], output_diff=[0x0000, 0x0000], external_diffs=[0x0000, 0x7fff],
        assign_outdiff_list=[0x0000, 0x7fff, 0x0000, 0x0000]))
>>> print(w)  # weight (sum of the key and encryption weights) of the related-key differential
3.192516141583136911276041810

cascada.smt.chsearch.round_based_ch_search(func, initial_num_rounds, final_num_rounds, prop_type, assert_type, solver_name, extra_chmodel_args=None, extra_chfinder_args=None, extra_findnextchweight_args=None, **kwargs)[source]

Search for characteristics of round-based functions over multiple number of rounds.

This function searches for characteristics of func (a RoundBasedFunction) by modelling the search as a sequence of SMT problems (using ChFinder), but the search is perfomed iteratively over the number of rounds of func. That is, first characteristics covering initial_num_rounds rounds are searched, then initial_num_rounds + 1, until final_num_rounds.

This function proceed as follows:

Set the number of rounds of func to initial_num_rounds.
Create a abstractproperty.chmodel.ChModel (resp. abstractproperty.chmodel.EncryptionChModel) object using as arguments func, prop_type and extra_chmodel_args.
Create a ChFinder object with arguments the characteristic model created in step 2, assert_type, solver_name and extra_chfinder_args.
Loop over the generator ChFinder.find_next_ch or ChFinder.find_next_ch_increasing_weight (depending on assert_type), and yield all characteristics from the generator (together with the current number of rounds).
After the generator has been exhausted, the search is finished if the current number of rounds is final_num_rounds. Otherwise, increase the number of rounds by one, set func to this number of rounds, and go to step 2.

In particular, this function is a Python generator function (see ChFinder), returning an iterator that yields tuples containing the current number of rounds and the last characteristic (an abstractproperty.characteristic.Characteristic if func is a RoundBasedFunction object, or a abstractproperty.characteristic.EncryptionCharacteristic if func is a RoundBasedFunction-encryption function of a Cipher) found in the search.

The argument prop_type is a particular Property such as XorDiff or LinearMask. For assert_type and solver_name, see ChFinder. The optional arguments extra_chmodel_args, extra_chfinder_args and extra_findnextchweight_args can be given as dictionaries (in the form of **kwargs) containing additional arguments for ChModel/EncryptionChModel, ChFinder and ChFinder.find_next_ch_increasing_weight calls respectively.

It is possible to abort the current search for the current number of rounds and start the search with one more round by passing the value INCREMENT_NUM_ROUNDS to the generator iterator with generator.send.

Note

In other words, step 4 in the previous description can be early aborted as follows

[...]
iterator = round_based_ch_search(...)
n1, ch_found = next(iterator)
iterator.send(INCREMENT_NUM_ROUNDS)
n2, ch_found = next(iterator)  # n2 > n1
[...]

Although generator.send yields a new value of the iteration, this function does not yield anything meaningful in the send calls.

The function round_based_ch_search is mostly meant to be used with ChModelAssertType.ValidityAndWeight, as the minimum weight obtain in one round is used as the initial weight for the next round. In other words, if all the characteristics covering \(r\) number of rounds were found with SMT problems for integer weights (see ChFinder.find_next_ch_increasing_weight) larger than \(w\), then \(w\) is set as the initial weight for the search for characteristics covering \(r+1\) rounds.

Note

All SMT problems modelling a characteristic covering \(r+1\) rounds for integer weights less or equal than \(r - 1\) are unsatisfiable due to our definition of characteristic weight (see abstractproperty.characteristic.Characteristic and differential.characteristic.Characteristic or linear.characteristic.Characteristic for some examples)

>>> # example of searching for XorDiff Characteristic over a BvFunction
>>> from cascada.differential.difference import XorDiff
>>> from cascada.smt.chsearch import ChModelAssertType, round_based_ch_search, INCREMENT_NUM_ROUNDS
>>> from cascada.primitives import speck
>>> Speck32_ks = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> assert_type = ChModelAssertType.ValidityAndWeight
>>> iterator = round_based_ch_search(Speck32_ks, 2, 5, XorDiff, assert_type, "btor",
...     extra_chfinder_args={"exclude_zero_input_prop": True, "solver_seed":0},
...     extra_findnextchweight_args={"initial_weight": 0})
>>> for (num_rounds, ch) in iterator:
...     print(num_rounds, ":", ch.srepr())
2 : Ch(w=0, id=0040 0000 0000, od=0000 0000 8000)
3 : Ch(w=0, id=0040 0000 0000 0000, od=0000 0000 0000 8000)
4 : Ch(w=0, id=0040 0000 0000 0000, od=0000 0000 0000 8000 8002)
5 : Ch(w=1, id=0040 0000 0000 0000, od=0000 0000 0000 8000 8002 8008)
>>> # example of searching for LinearMask EncryptionCharacteristic over a Cipher
>>> from cascada.linear.mask import LinearMask
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> assert_type = ChModelAssertType.ProbabilityOne
>>> iterator = round_based_ch_search(Speck32, 2, 3, LinearMask, assert_type, "btor",
...     extra_chfinder_args={"solver_seed":0})
>>> num_rounds, ch = next(iterator)
>>> print(num_rounds, ":", ch.srepr())
2 : Ch(w=0, id=0000 0000, od=0000 0000)
>>> num_rounds, ch = next(iterator)
>>> print(num_rounds, ":", ch.srepr())
2 : Ch(w=0, id=0080 4021, od=0201 0200)
>>> iterator.send(INCREMENT_NUM_ROUNDS)  # stop current num_rounds and increment by 1
>>> num_rounds, ch = next(iterator)
>>> print(num_rounds, ":", ch.srepr())
3 : Ch(w=0, id=0000 0000, od=0000 0000)

cascada.smt.chsearch.round_based_cipher_ch_search(cipher, initial_num_rounds, final_num_rounds, prop_type, ks_assert_type, enc_assert_type, solver_name, extra_cipherchmodel_args=None, extra_cipherchfinder_args=None, extra_findnextchweight_args=None)[source]

Search for characteristics of iterated ciphers over multiple number of rounds.

This function is similar to round_based_cipher_ch_search but searching for abstractproperty.characteristic.CipherCharacteristic instead of abstractproperty.characteristic.Characteristic.

In particular, this function creates an abstractproperty.chmodel.CipherChModel and an CipherChFinder objects instead of an abstractproperty.chmodel.ChModel and an ChFinder objects.

>>> from cascada.differential.difference import XorDiff
>>> from cascada.smt.chsearch import ChModelAssertType, round_based_cipher_ch_search
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> at = ChModelAssertType.ValidityAndWeight
>>> iterator = round_based_cipher_ch_search(Speck32, 2, 5, XorDiff, at, at, "btor",
...     extra_cipherchfinder_args={"ks_exclude_zero_input_prop": True, "solver_seed": 0},
...     extra_findnextchweight_args={"initial_weight": 0})
>>> for (num_rounds, ch) in iterator:
...     print(num_rounds, ":", ch.srepr())  
2 : Ch(ks_ch=Ch(w=0, id=0040 0000, od=0000 8000),
      enc_ch=Ch(w=0, id=0000 0000, od=8000 8000))
3 : Ch(ks_ch=Ch(w=0, id=0040 0000 0000, od=0000 0000 8000),
      enc_ch=Ch(w=0, id=0000 0000, od=8000 8000))
4 : Ch(ks_ch=Ch(w=0, id=0040 0000 0000 0000, od=0000 0000 0000 8000),
      enc_ch=Ch(w=0, id=0000 0000, od=8000 8000))
5 : Ch(ks_ch=Ch(w=0, id=0040 0000 0000 0000, od=0000 0000 0000 8000 8002),
      enc_ch=Ch(w=1, id=0000 0000, od=0102 0100))