cascada.abstractproperty.chmodel module

Manage bit-vector models of characteristics w.r.t an abstract property.

`ChModelSigType`	List of signature types for a `ChModel`.
`ChModel`	Represent bit-vector models of characteristics w.r.t some property over bit-vector functions.
`EncryptionChModel`	Represent characteristic models of encryption functions w.r.t some property.
`CipherChModel`	Represent characteristic models of ciphers w.r.t some property.

class cascada.abstractproperty.chmodel.ChModelSigType(value)[source]

Bases: enum.Enum

List of signature types for a ChModel.

Unique: the signature includes all the properties in the characteristic model needed to uniquely identity the characteristic model; this might include the input or output Property values, the non-constant external Property objects of the ChModel, or the input or output Property values of the non-trivial assignments.

InputOutput: the signature only includes the input and output Property values of the ChModel

class cascada.abstractproperty.chmodel.ChModel(func, prop_type, input_prop_names, prefix='px', external_var2prop=None, op_model_class2options=None)[source]

Bases: object

Represent bit-vector models of characteristics w.r.t some property over bit-vector functions.

A (bit-vector) model of a characteristic over a bit-vector function \(f\) for a particular Property is a set of bit-vector constraints that models the probability of the characteristic.

For the definition of characteristic and its probability see abstractproperty.characteristic.Characteristic.

A ChModel is mainly given by three bit-vector formulas or constraints: the validity constraint (see validity_assertions), the weight constraint (see weight_assertions), and probability-one constraint (see pr_one_assertions)

A ChModel object is defined for a type of Property, a BvFunction \(f\), the names of the input property words and the Property of the external variables of the SSA of \(f\).

A ChModel object also contains the symbolic properties \(\Delta_{x_i}\) in the trail as Variable objects and the models of the bit-vector operations (abstractproperty.opmodel.OpModel objects) of the non-trivial assignments \(x_{i+1} \leftarrow f_i(x_i)\) of the SSA representation of \(f\).

The trivial assignments are those that propagate properties deterministically (with probability one). The models for these assignments are not included in ChModel. Instead, the symbolic output property of each trivial assignment is automatically computed from the symbolic input property.

Note

A ChModel object can also be seen as a symbolic characteristic, where all the properties in the trail are represented by Variable objects. A particular instance of a characteristic with constant values of properties is represented by a abstractproperty.characteristic.Characteristic object.

A dictionary mapping abstractproperty.opmodel.OpModel classes to dictionaries (mapping class attributes names to their values) can be given in the argument op_model_class2options. In that case, the class attributes of the abstractproperty.opmodel.OpModel objects in the trail will be set to the values given in op_model_class2options. For example, op_model_class2options={XorModelBvAddCt: {'precision':0}} will set precision to 0 for all the XorModelBvAddCt models in the trail.

If the given bit-vector function \(f\) is a RoundBasedFunction including add_round_outputs calls in its eval, then the characteristic model over each round can be obtaining by combining split and get_round_separators.

This class is not meant to be instantiated but to provide a base class for creating characteristic models w.r.t some property, (see differential.chmodel.ChModel, linear.chmodel.ChModel or algebraic.chmodel.ChModel for some examples).

func: the BvFunction \(f\).

prop_type: the type of Property of the characteristic.

input_prop: a list of Property objects containing the (symbolic) input property.

output_prop: a list of Property objects containing the (symbolic) output property.

external_var2prop: a collections.OrderedDict mapping the external variables of ssa to their associated (symbolic or constant) Property objects.

assign_outprop2op_model: a collections.OrderedDict mapping the output Property \(\Delta_{x_{i+1}}\) of the non-trivial assignment \(x_{i+1} \leftarrow f_i(x_i)\) to the abstractproperty.opmodel.OpModel of this assignment.

ssa: the SSA of \(f\), where the input, output and intermediate values share the same names as the input, output and intermediate properties of the characteristic.

var2prop: a collections.OrderedDict mapping each variable in ssa to its associated Property object.

vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) returns a new ChModel object with the same content.

validity_assertions()[source]

Return the validity constraint as a list of assertions.

The validity constraint is a symbolic bit-vector expression (depending on the properties of the trail), and it is True if and only if the characteristic has non-zero probability.

The list of assertions is a list of symbolic Term objects that form the validity constraint when combined with the BvAnd operation.

The assertion list is composed of the OpModel.validity_constraint of the models of the non-trivial assignments.

pr_one_assertions()[source]

Return the probability-one constraint as a list of assertions.

Return the constraint that evaluates to True if the characteristic has probability-one as a list of assertions.

The probability-one constraint is a symbolic bit-vector expression (depending on the properties of the trail), and it is True if and only if the characteristic has probability 1.

The list of assertions is a list of symbolic Term objects that form the constraint when combined with the BvAnd operation.

The assertion list is composed of the OpModel.pr_one_constraint of the models of the non-trivial assignments.

weight_assertions(ch_weight_variable, assign_weight_variables, truncate=True)[source]

Return the weight constraint as a list of assertions.

The weight constraint is a symbolic bit-vector expression that depends on the properties of the trail, the characteristic weight variable and the weight variables of the models of the non-trivial assignments. This expression is True if and only if the weight (negative binary logarithm of the probability) of the characteristic is equals to the characteristic weight variable.

The list of assertions is a list of symbolic Term objects that form the weight constraint when combined with the BvAnd operation.

The assertion list is composed of the OpModel.weight_constraint of the models of the non-trivial assignments, plus a final assertion that sets the characteristic weight variable as the sum of the assignment weight variables.

Similar as abstractproperty.opmodel.OpModel, the characteristic weight variable can be interpreted as a rational value with num_frac_bits fractional bits, and the weight constraint can be True even if the characteristic weight variable is equals to the characteristic weight up to some error bounded by error.

If truncate is True, the sum of the assignment weight variables is truncated (fractional bits are removed) and the result is compared to the characteristic weight variable. In other words, the characteristic weight variable represents the integer part of the weight of the characteristic probability if truncate=True (default case).

external_vars_validity_assertions()[source]

Return the union of external variables of the constraints from validity_assertions.

See abstractproperty.opmodel.OpModel for the definition of an external variable of a constraint from a model.

external_vars_pr_one_assertions()[source]

Return the union of external variables of the constraints from pr_one_assertions.

See abstractproperty.opmodel.OpModel for the definition of an external variable of a constraint from a model.

external_vars_weight_assertions(assign_weight_variables)[source]

Return the union of external variables of the constraints from weight_assertions.

See abstractproperty.opmodel.OpModel for the definition of an external variable of a constraint from a model.

max_weight(truncate=True)[source]

Return the maximum value the ch. weight variable can achieve in weight_assertions.

If truncate is True, fractional bits are not considered in the ch. weight variable (see weight_assertions).

weight_width(truncate=True)[source]

Return the width of the ch. weight variable used weight_assertions.

If truncate is True, fractional bits are not considered in the ch. weight variable (see weight_assertions).

For the doctests see max_weight.

num_frac_bits()[source]

Return the number of fractional bits of the ch. weight variable used in weight_assertions.

If the number of fractional bits is k, then the bit-vector characteristic weight variable w of weight_assertions represents the number 2^{-k} * bv2int(w). In particular, if k == 0, then w represents an integer number. Otherwise, the k least significant bits of w denote the fractional part of the number represented by w.

For the doctests see max_weight.

error()[source]

Return the maximum difference between weight_assertions and the exact weight.

The exact weight is exact value (without error) of the negative binary logarithm (weight) of the characteristic probability.

This method returns an upper bound (in absolute value) of the maximum difference (over all properties in the trail) between the bit-vector characteristic weight from weight_assertions and the exact weight.

signature(sig_type)[source]

Return the signature of the characteristic model.

The argument sig_type is a type of the signature, see ChModelSigType.

The signature is an identifier of the characteristic model (used for comparing). Depending on the signature type, the identifier might uniquely represent the characteristic model or not.

The signature does not include the Property objects of the characteristic but their (symbolic) values (Variable objects).

split(prop_separators)[source]

Split into multiple ChModel objects given the list of property separators.

Given the ChModel with underlying SSA \(s\), this method returns a list of ch. models with underlying SSA objects \(s_1, s_2, ..., s_n\), such that their composition \(s_n \circ s_{n-1} \dots \circ s_1\) is functionally equivalent to \(s\).

The argument prop_separators is a list containing lists of properties. The \(i\)-th property list denote the last properties of the \(i\)-th ch. model. In other words, the \((i+1)\)-th ch. model immediately starts after the last property in prop_separators[i].

To split into \(n\) ch. models, prop_separators must contain \(n-1\) lists, as the property list of the last ch. model is not given (its last properties are the output properties of the main model).

Note the underlying functions of the new ch. models are BvFunction (and not RoundBasedFunction) even if func is a RoundBasedFunction.

get_formatted_logged_msgs()[source]

Return the list of logged messages.

If func includes log_msg calls in its eval, this method return the list of messages logged with the format field objects applied. Otherwise, an empty list is returned.

In the first case, the Variable objects of ssa appearing in the format field objects are replaced with their associated symbolic Property objects.

get_round_separators()[source]

Return the round separators if func is a RoundBasedFunction.

If func includes add_round_outputs calls in its eval, this method returns a list with the round Property outputs delimiting the rounds. Otherwise, None is returned.

In the first case, this list contains num_rounds - 1 entries, where the i-th entry is the list of Property outputs of the i-th round. In particular, the output properties of the last round are not included in this list.

The list returned by this method is meant to be used as the argument of ChModel.split to get the ChModel object of each round.

dotprinting(repeat=True, vrepr_label=False, **kwargs)[source]

Return the DOT description of the expression tree of assign_outprop2op_model.