cascada.smt.invalidpropsearch module

Search for zero-probability (invalid) properties (e.g., impossible differentials or zero-correlation hulls) by modeling the search as a sequence of SMT problems.

ActiveBitMode

Represent the subsets of bit-vectors available depending on which bits are activated (set to 1) for find_next_invalidprop_activebitmode.

InvalidPropFinder

Search for zero-probability (invalid) property pairs by modeling the search as a sequence of SMT problems.

InvalidCipherPropFinder

Search for invalid properties of ciphers by modeling the search as a sequence of SMT problems.

round_based_invalidprop_search

Search for zero-probability (invalid) property pairs of round-based functions over multiple number of rounds.

round_based_invalidcipherprop_search

Search for zero-probability (invalid) properties of iterated ciphers over multiple number of rounds.
class cascada.smt.invalidpropsearch.ActiveBitMode(value)[source]

Bases: enum.Enum

Represent the subsets of bit-vectors available depending on which bits are activated (set to 1) for find_next_invalidprop_activebitmode.

Default

all bit-vectors

SingleBit

bit-vectors with up to one bit activated (zero included)

MSBbit

bit-vectors with up to the most significant bit activated (zero included)

Zero

the zero bit-vector

class cascada.smt.invalidpropsearch.InvalidPropFinder(ch_model, solver_name, check_universally_invalid_ch_found=True, printing_mode=PrintingMode.Silent, filename=None, solver_seed=None, env=None)[source]

Bases: cascada.smt.chsearch.ChFinder

Search for zero-probability (invalid) property pairs by modeling the search as a sequence of SMT problems.

Given a characteristic model defined for a particular Property (e.g., XorDiff or LinearMask), this class finds universally-invalid characteristics following the characteristic model by modelling the search as a sequence of SMT problems in the bit-vector theory.

A universally-invalid characteristic is a characteristic where the characteristic input property \(\alpha\) propagates to the characteristic output property \(\beta\) with probability zero regardless of the intermediate properties (i.e., for all assignments of the intermediate properties). In other words, the input-output property pair \((\alpha, \beta)\) has zero propagation probability.

Note

For the Difference (resp. LinearMask) property, a universally-invalid characteristic is actually an impossible differential (resp. a zero-correlation hull).

Search for universally-invalid algebraic characteristic is not supported.

Consider the SMT problem \(\Omega\) of whether there exists a valid characteristic with constant input property \(\alpha\) and constant output property \(\beta\) (and where the intermediate properties are not specified). The main idea of the SMT-based search is that one can check whether \(\alpha\) propagates to \(\beta\) with probability zero by checking whether \(\Omega\) is unsatisfiable (UNSAT). Note that only the validity constraints are needed to build \(\Omega\); the weight constraints are ignored when searching for universally-invalid characteristics.

The initialization argument ch_model must be a subclass of abstractproperty.chmodel.ChModel with up to one non-trivial transitions (abstractproperty.opmodel.OpModel excluding ModelIdentity), since a zero-probability characteristic with up to one non-trivial transitions is a universally-invalid characteristic. For a characteristic model with more than one non-trivial transitions, the function get_wrapped_chmodel can be used to wrap the characteristic model into an equivalent characteristic model with one non-trivial transition.

An InvalidPropFinder object is also an instance of ChFinder where assert_type is Validity and with the given initialization arguments ch_model, solver_name, printing_mode, filename, solver_seed and env=env. See also ChFinder.

Similar as ChFinder, the methods of InvalidPropFinder that search for universally-invalid characteristics are Python generator functions, returning an iterator that yields the universally-invalid characteristics found in the search. If initialization argument ch_model is a abstractproperty.chmodel.ChModel (resp. abstractproperty.chmodel.EncryptionChModel), then these methods yield abstractproperty.characteristic.Characteristic (resp. abstractproperty.characteristic.EncryptionCharacteristic) objects.

If the initialization argument check_universally_invalid_ch_found is True, all universally-invalid characteristics found in the search are checked by searching for a valid characteristic with the same input and output property with ChFinder.find_next_ch.

>>> # example of SMT problem of universally-invalid LinearMask-EncryptionCharacteristic of (wrapped) Speck32
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import EncryptionChModel
>>> from cascada.smt.invalidpropsearch import InvalidPropFinder
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> wrapped_ch_model = get_wrapped_chmodel(EncryptionChModel(Speck32, LinearMask))
>>> invalid_prop_finder = InvalidPropFinder(wrapped_ch_model, "z3", solver_seed=0)
>>> invalid_prop_finder.formula_size()
133
>>> print(invalid_prop_finder.hrepr(full_repr=True))  
; characteristic model assertions
assert (_mx0 == (mx9_out :: mx7_out)) &
    ((~((mx1 ^ (_mp0 >>> 7)) | (mx1 ^ mp1__0)) | _tmp20affb7ca27930ce775156bcc0ecaf20) == 0xffff) &
    ((_tmp20affb7ca27930ce775156bcc0ecaf20 ^ (_tmp20affb7ca27930ce775156bcc0ecaf20 >> 0x0001) ^
        ((mx1 ^ (_mp0 >>> 7) ^ mp1__0) >> 0x0001)) == 0x0000) &
    (mx1 == _mk0) & (mx1 == mx2) & (((_mp1 ^ mp1__0) <<< 2) == mx2__0) & (((_mp1 ^ mp1__0) <<< 2) == mx4) &
    ((~((mx6 ^ ((mx2 ^ mx2__0) >>> 7)) | (mx6 ^ mx4__0)) | _tmp824d7e7c80d9889507eb4e5d5c7be280) == 0xffff) &
    ((_tmp824d7e7c80d9889507eb4e5d5c7be280 ^ (_tmp824d7e7c80d9889507eb4e5d5c7be280 >> 0x0001) ^
        ((mx6 ^ ((mx2 ^ mx2__0) >>> 7) ^ mx4__0) >> 0x0001)) == 0x0000) &
    (mx6 == _mk1) & (mx6 == mx7) & (((mx4 ^ mx4__0) <<< 2) == mx7__0) &
    (((mx4 ^ mx4__0) <<< 2) == mx9) & ((mx7 ^ mx7__0) == mx7_out) & (mx9 == mx9_out)
assert PropExtract_{·, 15, 0}(_mx0) == _mx1_out
assert PropExtract_{·, 31, 16}(_mx0) == _mx2_out

>>> # example of SMT problem of universally-invalid XorDiff-Characteristic of Speck32-KeySchedule
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import ChModel
>>> from cascada.smt.invalidpropsearch import InvalidPropFinder
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(1)
>>> ch_model = ChModel(Speck32_KS, XorDiff, ["mk0", "mk1"])
>>> invalid_prop_finder = InvalidPropFinder(ch_model, "z3", solver_seed=0)
>>> invalid_prop_finder.formula_size()
42
>>> print(invalid_prop_finder.hrepr(full_repr=True))  
; characteristic model assertions
assert ((~((mk0 >>> 7) << 0x0001) ^ (mk1 << 0x0001)) & (~((mk0 >>> 7) << 0x0001) ^ (dx1 << 0x0001)) &
    ((mk0 >>> 7) ^ mk1 ^ dx1 ^ ((mk0 >>> 7) << 0x0001))) == 0x0000
assert mk1 == mk1_out
assert ((mk1 <<< 2) ^ dx1) == dx3_out
find_next_invalidprop_activebitmode(initial_num_active_bits, input_prop_activebitmode, output_prop_activebitmode)[source]

Return an iterator that yields the universally-invalid characteristics found in the SMT-based search with given ActiveBitMode.

This method searches for universally-invalid characteristic using SMT solvers by checking one-by-one all input and output properties with given ActiveBitMode.

Given a particular input and output properties \((\alpha, \beta)\), the main subroutine of this method (herein call the check subroutine) checks whether \(\alpha\) propagates to \(\beta\) with probability zero by checking with an SMT solver whether the SMT problem, of whether there exists a valid characteristic with input property \(\alpha\) and output property \(\beta\), is unsatisfiable (UNSAT). If the problem is UNSAT, the universally-invalid abstractproperty.characteristic.Characteristic object with input and output properties \((\alpha, \beta)\) is created and yielded.

The check subroutine is repeated for all input and output properties where the ActiveBitMode of each word in the input (resp. output) property is input_prop_activebitmode (resp. output_prop_activebitmode). The search starts considering input and output properties where the total number of active bits is initial_num_active_bits, and the total number of active bits is incremented when all the input and output properties are checked.

>>> # example of search for universally-invalid LinearMask-EncryptionCharacteristic of (wrapped) Speck32
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import EncryptionChModel
>>> from cascada.smt.invalidpropsearch import InvalidPropFinder, ActiveBitMode
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> wrapped_ch_model = get_wrapped_chmodel(EncryptionChModel(Speck32, LinearMask))
>>> invalid_prop_finder = InvalidPropFinder(wrapped_ch_model, "btor", solver_seed=0)
>>> inab, ipabm, opabm = 1, ActiveBitMode.MSBit, ActiveBitMode.MSBit
>>> for ch in invalid_prop_finder.find_next_invalidprop_activebitmode(inab, ipabm, opabm):
...     print(ch.srepr())
Ch(w=Infinity, id=8000 0000, od=8000 0000)
Ch(w=Infinity, id=8000 0000, od=0000 8000)
Ch(w=Infinity, id=0000 8000, od=8000 0000)
Ch(w=Infinity, id=0000 8000, od=0000 8000)
Ch(w=Infinity, id=8000 0000, od=8000 8000)
Ch(w=Infinity, id=0000 8000, od=8000 8000)
Ch(w=Infinity, id=8000 8000, od=8000 0000)
Ch(w=Infinity, id=8000 8000, od=0000 8000)
Ch(w=Infinity, id=8000 8000, od=8000 8000)
>>> # example of SMT problem of universally-invalid XorDiff-Characteristic of Speck32-KeySchedule
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import ChModel
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(1)
>>> ch_model = ChModel(Speck32_KS, XorDiff, ["mk0", "mk1"])
>>> invalid_prop_finder = InvalidPropFinder(ch_model, "btor", solver_seed=0)
>>> inab, ipabm, opabm = 1, ActiveBitMode.SingleBit, ActiveBitMode.SingleBit
>>> ch = next(invalid_prop_finder.find_next_invalidprop_activebitmode(inab, ipabm, opabm))
>>> print(ch)  
Characteristic(ch_weight=inf, assignment_weights=[inf, inf, 0],
    input_diff=[0x0001, 0x0000], output_diff=[0x0001, 0x0000],
    assign_outdiff_list=[0x0000, 0x0001, 0x0000])
find_next_invalidprop_miss_in_the_middle(ch_model_E0, ch_model_E2, ch_model_E=None, ch_model_external_E=None, exclude_zero_input_prop_E0=True, exclude_zero_input_prop_E2=True, exclude_zero_input_prop_external_E=None)[source]

Return an iterator that yields the universally-invalid characteristics found in the SMT+MitM-based search.

This method searches for universally-invalid characteristic using SMT problems and the miss-in-the-middle approach.

Let \(E\) be a function split into three functions \(E = E_2 \circ E_1 \circ E_0\). Let \(((p_0, p_1), (p_2, p_3))\) denote a partial characteristic over \(E\), that is, a characteristic over \(E\) where:

  • \((p_0, p_1)\) are the non-zero input and output properties of a characteristic with probability 1 over \(E_0\)

  • \((p_2, p_3)\) are the non-zero input and output properties of a characteristic with probability 1 over \(E_2\)

  • no relation is imposed between \((p_1, p_2)\), the input and output properties of \(E_1\).

The underlying function of self.ch_model corresponds to \(E_1\), the underlying function of the abstractproperty.chmodel.ChModel ch_model_E0 corresponds to \(E_0\), and the underlying function of the abstractproperty.chmodel.ChModel ch_model_E2 corresponds to \(E_2\). The underlying function of the abstractproperty.chmodel.ChModel ch_model_E corresponds to \(E\), but this argument is optional (more on that later).

By default the input properties of ch_model_E0 and ch_model_E2 are excluded to be zero, but this can be changed with the optional arguments exclude_zero_input_prop_*.

Note

This method requires that for any probability-one characteristic over \(E_0\) with input-output property \((p_0, p_1)\), there is no other probability-one characteristic over \(E_0\) with input property \(p_0\) but output property \(\neq p_1\).

Similarly, for any probability-one characteristic over \(E_2\) with input-output property \((p_2, p_3)\), there is no other probability-one characteristic over \(E_2\) with output property \(p3\) but input property \(\neq p_2\).

If \(E_0\) and \(E_2\) are permutations, then these two requirements are satisfied for Difference and LinearMask properties.

If the optional argument ch_model_external_E is given as a abstractproperty.chmodel.ChModel with input and output properties \((q_0, q_1)\), the definition of a partial characteristic is extended to \(((p_0, p_1), (p_2, p_3), (q_0, q_1)\) such that \((q_0, q_1)\) are the input and output properties of a characteristic with probability 1 where \(q_1\) is the list of external variables of \(E\) (see SSA). If ch_model_external_E is given, the argument exclude_zero_input_prop_external_E that determines whether to exclude non-zero \(q_0\) must also be given.

Note

The functions \((E_0, E_1, E_2)\) can be easily obtained from a RoundBasedFunction \(E\) that includes add_round_outputs calls in its eval.

For example, obtaining \(E_0\) from the round ns to ns+ne0 (ns denoting the initial number of skipped rounds), \(E_1\) as the next ne1 rounds, and \(E_2\) as the next ne2 rounds can be done as follows:

[...]
ns, ne0, ne1, ne2 = ...
MyRoundBasedFunction.set_num_rounds(ns+ne0+ne1+ne2)
ch_model_E = ChModel(MyRoundBasedFunction, ...)
rs = ch_model.get_round_separators()
# the end of the i-th round (i=1,2,...) is rs[i-1]
e0_rs, e1_rs = rs[ns+ne0-1], rs[ns+ne0+ne1-1]
ch_model_E0, ch_model_E1, ch_model_E2 = ch_model_E.split([e0_rs, e1_rs])
ch_model_E1 = get_wrapped_chmodel(ch_model_E1)  # in case ch_model_E1 2+ non-trivial transitions
invalid_prop_finder = InvalidPropFinder(ch_model_E1, ...)
invalid_prop_finder.find_next_invalidprop_miss_in_the_middle(
    ch_model_E0=ch_model_E0, ch_model_E2=ch_model_E2, ch_model_E=ch_model_E)

Alternatively, one can use the function round_based_invalidprop_search which automates the generation of \((E_0, E_1, E_2)\) and applies this method iteratively on the number of rounds.

This method finds universally-invalid characteristics by searching for all partial characteristics over \(E\) using ChFinder.find_next_ch, and for each partial characteristic we apply the check subroutine to check whether \(p_1\) propagates to \(p_2\) with zero probability over \(E_1\). The check subroutine is explained in find_next_invalidprop_activebitmode.

For each partial characteristic \(((p_0, p_1), (p_2, p_3))\) found, if the check subroutine finds that \(p_1\) propagates to \(p_2\) with zero probability, a tuple of 3 abstractproperty.characteristic.Characteristic is yielded:

  • the first characteristic corresponds to the characteristic with probability 1 over \(E_0\) with input and output properties \((p_0, p_1)\)

  • the second characteristic corresponds to the universally-invalid characteristic over \(E_1\) with input and output properties \((p_1, p_2)\)

  • the third characteristic corresponds to the characteristic with probability 1 over \(E_2\) with input and output properties \((p_2, p_3)\)

Since the first and third characteristics have probability one, the concatenation of these three characteristics is a universally-invalid characteristic over \(E\) (regardless of the external variables of \(E\))

If the optional argument ch_model_external_E is given, instead a tuple of 4 characteristic is yieled; the 4-th characteristic corresponds to the characteristic with probability 1 with input and output properties \((q_0, q_1)\). In this case, the concatenation of the first 3 characteristics is a universally-invalid characteristic over \(E\) for the external properties given by the outputs of the 4-th characteristic.

If the initialization argument check_universally_invalid_ch_found is True, all universally-invalid characteristics found over \(E_1\) in the search are checked by searching for a valid characteristic with the same input and output property with ChFinder.find_next_ch. In addition, if the optional argument ch_model_E is given, then the universally-invalid characteristic over \(E\) (the concatenation of the characteristic founds over \(E_0\), \(E_1\) and \(E_2\)) is also checked in a similar way.

>>> # example of search for universally-invalid LinearMask-EncryptionCharacteristic of (wrapped) Speck32
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import EncryptionChModel
>>> from cascada.smt.invalidpropsearch import InvalidPropFinder
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(3)
>>> ch_model_E = EncryptionChModel(Speck32, LinearMask)
>>> ch_model_E0, ch_model_E1, ch_model_E2 = ch_model_E.split(ch_model_E.get_round_separators())
>>> ch_model_E1 = get_wrapped_chmodel(ch_model_E1)
>>> invalid_prop_finder = InvalidPropFinder(ch_model_E1, "btor", solver_seed=0)
>>> tuple_iterator = invalid_prop_finder.find_next_invalidprop_miss_in_the_middle(ch_model_E0, ch_model_E2)
>>> for i, (pr1_ch_E0, uni_inv_ch_E1, pr1_ch_E2) in enumerate(tuple_iterator):
...     print(pr1_ch_E0.srepr(), uni_inv_ch_E1.srepr(), pr1_ch_E2.srepr())
...     if i == 2: break
Ch(w=0, id=0000 0001, od=0004 0004) Ch(w=Infinity, id=0004 0004, od=0000 0001) Ch(w=0, id=0000 0001, od=0004 0004)
Ch(w=0, id=0000 0001, od=0004 0004) Ch(w=Infinity, id=0004 0004, od=0080 e001) Ch(w=0, id=0080 e001, od=8002 8003)
Ch(w=0, id=0000 0001, od=0004 0004) Ch(w=Infinity, id=0004 0004, od=0080 f001) Ch(w=0, id=0080 f001, od=c002 c003)
>>> # example of SMT problem of universally-invalid XorDiff-Characteristic of Speck32-KeySchedule
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import ChModel
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(3)
>>> ch_model_E = ChModel(Speck32_KS, XorDiff, ["mk0", "mk1", "mk2", "mk3"])
>>> ch_model_E0, ch_model_E1, ch_model_E2 = ch_model_E.split(ch_model_E.get_round_separators())
>>> invalid_prop_finder = InvalidPropFinder(ch_model_E1, "btor", solver_seed=0)
>>> ti = invalid_prop_finder.find_next_invalidprop_miss_in_the_middle(ch_model_E0, ch_model_E2, ch_model_E=ch_model_E)
>>> pr1_ch_E0, uni_inv_ch_E1, pr1_ch_E2 = next(ti)
>>> print(pr1_ch_E0)  
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0, 0, 0],
    input_diff=[0x0001, 0x0001, 0x0000, 0x0000], output_diff=[0x0001, 0x0000, 0x0001, 0x0000],
    assign_outdiff_list=[0x0000, 0x0001, 0x0000, 0x0001, 0x0000])
>>> print(uni_inv_ch_E1)  
Characteristic(ch_weight=inf, assignment_weights=[inf, inf, 0, inf, inf],
    input_diff=[0x0001, 0x0000, 0x0001, 0x0000], output_diff=[0x0000, 0x8000, 0x0001, 0x0001],
    assign_outdiff_list=[0x8000, 0x0000, 0x8000, 0x0001, 0x0001])
>>> print(pr1_ch_E2)  
Characteristic(ch_weight=0, assignment_weights=[0, 0, 0, 0, 0],
    input_diff=[0x0000, 0x8000, 0x0001, 0x0001], output_diff=[0x0001, 0x0001, 0x8000, 0x8002],
    assign_outdiff_list=[0x8000, 0x0001, 0x0001, 0x8000, 0x8002])
find_next_invalidprop_quantified_logic()[source]

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

This method searches for universally-invalid characteristic using SMT problems in the quantified bit-vector logic (with the ForAll quantifier).

Let \(P(\alpha, \gamma_1, \dots, \gamma_t, \beta)\) be the underlying bit-vector formula of the decision problem of whether there exists a characteristic following the characteristic model ch_model with non-zero probability, where \((\alpha, \beta)\) is the input and output properties and \((\gamma_1, \dots, \gamma_t)\) are the intermediate properties.

First, this method creates the decision problem of whether there exists an assignment of the input and output properties \((\alpha, \beta)\) such that for all intermediate properties \((\gamma_1, \dots, \gamma_t)\) the negation of \(P\) is True; in other words, the decision problem given by the underlying quantified formula \(\exists \alpha, \beta, \forall \gamma_1, \dots, \gamma_t : \ \neg P(\alpha, \gamma_1, \dots, \gamma_t, \beta)\)

If the SMT solver finds the first problem satisfiable, an assignment of the input and output properties \((\alpha, \beta)\) that makes \(\neg P(\alpha, \gamma_1, \dots, \gamma_t, \beta) = True\) is obtained, and a universally-invalid abstractproperty.characteristic.Characteristic object is created and yielded.

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.

This method requires that the SMT solver given in solver_name supports the bit-vector logic with quantifiers. Although the recent version of boolector supports the bit-vector logic with quantifiers, pySMT does not support yet this recent feature of boolector.

>>> # example of search for universally-invalid XorDiff-EncryptionCharacteristic of (wrapped) Speck32
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.invalidpropsearch import InvalidPropFinder
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> wrapped_ch_model = get_wrapped_chmodel(EncryptionChModel(Speck32, XorDiff))
>>> invalid_prop_finder = InvalidPropFinder(wrapped_ch_model, "z3", solver_seed=0)
>>> for i, ch in enumerate(invalid_prop_finder.find_next_invalidprop_quantified_logic()):
...     print(ch.srepr())
...     if i == 2: break  
Ch(w=Infinity, id=..., od=...)
Ch(w=Infinity, id=..., od=...)
Ch(w=Infinity, id=..., od=...)
>>> # example of SMT problem of universally-invalid RXDiff-Characteristic of Speck32-KeySchedule
>>> from cascada.differential.difference import RXDiff
>>> from cascada.differential.chmodel import ChModel
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(1)
>>> ch_model = ChModel(Speck32_KS, RXDiff, ["mk0", "mk1"])
>>> invalid_prop_finder = InvalidPropFinder(ch_model, "z3", solver_seed=0)
>>> for i, ch in enumerate(invalid_prop_finder.find_next_invalidprop_quantified_logic()):
...     print(ch.srepr())
...     if i == 2: break  
Ch(w=Infinity, id=..., od=...)
Ch(w=Infinity, id=..., od=...)
Ch(w=Infinity, id=..., od=...)
hrepr(full_repr=False)[source]

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

The base SMT problem is the decision problem of whether there exists a valid characteristic for an input-output property pair. In other words, it contains the validity assertions of the underlying characteristic model.

The methods InvalidPropFinder.find_next_invalidprop_activebitmode and InvalidPropFinder.find_next_invalidprop_miss_in_the_middle check for the unsatisfiability of this base SMT problem (with some additional constraints), while InvalidPropFinder.find_next_invalidprop_quantified_logic uses this base SMT problem to create a quantified bit-vector formula.

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

class cascada.smt.invalidpropsearch.InvalidCipherPropFinder(ch_model, solver_name, check_universally_invalid_ch_found=True, printing_mode=PrintingMode.Silent, filename=None, solver_seed=None, env=None)[source]

Bases: cascada.smt.invalidpropsearch.InvalidPropFinder

Search for invalid properties of ciphers 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 RXDiff), this class finds universally-invalid cipher characteristics (abstractproperty.characteristic.CipherCharacteristic) following the characteristic model by modelling the search as a sequence of SMT problems in the bit-vector theory.

Given a cipher characteristic, let \(\alpha_{KS}\) be the input property of the underlying key-schedule characteristic and \((\alpha_{ENC}, \beta_{ENC})\) be the input and output properties of the underlying encryption characteristic. A universally-invalid characteristic over a cipher is a characteristic where \((\alpha_{KS}, \alpha_{ENC})\) propagates to \(\beta_{ENC}\) with probability zero regardless of the intermediate properties. In other words, the input-output property pair \(((\alpha_{KS}, \alpha_{ENC}), \beta_{ENC})\) has zero propagation probability.

Note

For the Difference property, a universally-invalid characteristic over a cipher is actually a related-key impossible differential.

To initialize an InvalidCipherPropFinder object, first two auxiliary instances of InvalidPropFinder are created:

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

Then, these two auxiliary InvalidPropFinder objects are merged into an InvalidCipherPropFinder (which is also an instance of InvalidPropFinder) 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)

  • chmodel_asserts is the union of chmodel_asserts of ks_finder and enc_finder

See also ChFinder.

>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.invalidpropsearch import InvalidCipherPropFinder, get_wrapped_cipher_chmodel
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = get_wrapped_cipher_chmodel(CipherChModel(Speck32, XorDiff))
>>> invalid_prop_finder = InvalidCipherPropFinder(ch_model, "btor", solver_seed=0)
>>> invalid_prop_finder.formula_size()
177
>>> print(invalid_prop_finder.hrepr(full_repr=False))  
; characteristic model assertions
assert (_dk0 == (dk3_out :: dmk1_out)) & ((... & ... & (... ^ ...)) == 0x0000) &
    (_dmk1 == dmk1_out) & (((_dmk1 <<< 2) ^ dk1) == dk3_out)
assert PropExtract_{·, 15, 0}(_dk0) == _dk1_out
assert PropExtract_{·, 31, 16}(_dk0) == _dk2_out
assert (_dx0 == (dx9_out :: dx7_out)) & ((... & ...) == 0x0000) & ((... & ...) == 0x0000) &
    ((dx6 ^ _dk2_out) == dx7_out) & ((((... ^ ...) <<< 2) ^ dx6 ^ _dk2_out) == dx9_out)
assert PropExtract_{·, 15, 0}(_dx0) == _dx1_out
assert PropExtract_{·, 31, 16}(_dx0) == _dx2_out
find_next_invalidprop_activebitmode(initial_num_active_bits, input_prop_activebitmode, output_prop_activebitmode)[source]

Return an iterator that yields the universally-invalid characteristics found in the SMT-based search with given ActiveBitMode.

This method is similar to InvalidPropFinder.find_next_invalidprop_activebitmode; the only difference is that the input property considered by this method is the concatenation of the input property of the underlying key-schedule characteristic and the input property of the underlying encryption characteristic, and the output property considered by this method is the output property of the encryption characteristic. In other words, output_prop_activebitmode only affects to the output property of the encryption characteristic and not to the output property of the key-schedule characteristic.

>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.invalidpropsearch import InvalidCipherPropFinder, ActiveBitMode, get_wrapped_cipher_chmodel
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = get_wrapped_cipher_chmodel(CipherChModel(Speck32, XorDiff))
>>> invalid_prop_finder = InvalidCipherPropFinder(ch_model, "btor", solver_seed=0)
>>> inab, ipabm, opabm = 1, ActiveBitMode.MSBit, ActiveBitMode.Zero
>>> for ch in invalid_prop_finder.find_next_invalidprop_activebitmode(inab, ipabm, opabm):
...     print(ch.srepr())
Ch(ks_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000), enc_ch=Ch(w=0, id=0000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=0000 8000, od=0000 0000), enc_ch=Ch(w=0, id=0000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=0000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000), enc_ch=Ch(w=0, id=0000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=0000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 8000, od=8000 8002), enc_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 8000, od=8000 8002), enc_ch=Ch(w=Infinity, id=0000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000), enc_ch=Ch(w=Infinity, id=0000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 0000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=0, id=0000 8000, od=8000 8002), enc_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000))
Ch(ks_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000), enc_ch=Ch(w=Infinity, id=8000 8000, od=0000 0000))
find_next_invalidprop_miss_in_the_middle(*args, **kargs)[source]

This method is disabled, see round_based_invalidcipherprop_search for an alternative.

find_next_invalidprop_quantified_logic()[source]

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

See also InvalidPropFinder.find_next_invalidprop_quantified_logic.

>>> from cascada.differential.difference import RXDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.invalidpropsearch import InvalidCipherPropFinder, get_wrapped_cipher_chmodel
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model = get_wrapped_cipher_chmodel(CipherChModel(Speck32, RXDiff))
>>> invalid_prop_finder = InvalidCipherPropFinder(ch_model, "z3", solver_seed=0)
>>> uni_inv_ch = next(invalid_prop_finder.find_next_invalidprop_quantified_logic())
>>> print(uni_inv_ch)  
CipherCharacteristic(ks_characteristic=Characteristic(ch_weight=...,
    assignment_weights=[..., ..., ...],
    input_diff=[..., ...], output_diff=[..., ...],
    assign_outdiff_list=[..., ..., ...]),
enc_characteristic=Characteristic(ch_weight=...,
    assignment_weights=[..., ..., ...],
    input_diff=[..., ...], output_diff=[..., ...], external_diffs=[..., ...],
    assign_outdiff_list=[..., ..., ...]))

Search for zero-probability (invalid) property pairs of round-based functions over multiple number of rounds.

This function searches for universally-invalid characteristics (leading to invalid properties, see InvalidPropFinder) of a RoundBasedFunction func by modelling the search as a sequence of SMT problems (using InvalidPropFinder.find_next_invalidprop_miss_in_the_middle), but the search is perfomed iteratively over the number of rounds of func. That is, first universally-invalid characteristics covering initial_num_rounds rounds are searched, then initial_num_rounds + 1, until final_num_rounds. See also round_based_ch_search.

Note

The RoundBasedFunction func must include add_round_outputs calls in its eval.

While InvalidPropFinder requires wrapping the characteristic model if it has more than one non-trivial transition, this method does require the function func to be not wrapped.

This method also requires that for all the round functions \(f_i\) of func (generated through SSA.split with SSA.get_round_separators), given any probability-one characteristic over \(f\) with input-output property \((\alpha, \beta)\), then there is no other probability-one characteristic with input property \(\alpha\) (resp. output property \(\beta\)) but output property \(\neq \beta\) (resp. input property \(\neq \alpha\)). If all the round functions are permutations, then this is satisfied for Difference and LinearMask properties. See also InvalidPropFinder.find_next_invalidprop_miss_in_the_middle.

This function proceed as follows:

  1. Set the current number of rounds of the universally-invalid characteristics to search for to initial_num_rounds.

  2. Set the current number of initial rounds to skip to 0.

  3. Set the number of rounds of func to the sum of the number of rounds of step 1 and step 2, and split func into \(E \circ S\) (\(S\) denotes the skipped rounds and \(E\) the target function of the universally-invalid characteristics to search for).

  4. Create a abstractproperty.chmodel.ChModel (resp. abstractproperty.chmodel.EncryptionChModel) object of \(E\) using as arguments prop_type and extra_chmodel_args.

  5. Split \(E\) into \(E = E_2 \circ E_1 \circ E_0\) taking into account min_num_E0_rounds, min_num_E2_rounds and generate the characteristic models of \((E_0, E_1, E_2)\) using abstractproperty.chmodel.ChModel.get_round_separators and abstractproperty.chmodel.ChModel.split. See InvalidPropFinder.find_next_invalidprop_miss_in_the_middle for more details about \((E_0, E_1, E_2)\).

  6. Create an InvalidPropFinder object with arguments the characteristic model over \(E_1\), solver_name and extra_invalidpropfinder_args.

  7. Loop over the generator InvalidPropFinder.find_next_invalidprop_miss_in_the_middle (with arguments exclude_zero_input_prop_E0 and exclude_zero_input_prop_E2) and yield all the 3-length tuples of characteristics from the generator (together with the current number of rounds).

  8. After the generator is exhausted, go to step 5 but splitting \(E\) into antoher another partition \((E_0, E_1, E_2)\).

    1. If all partitions has been exhausted, instead increase the current number of initial rounds to skip (up to max_num_skipped_rounds) and go to step 3.

    2. If the current number of skipped rounds was max_num_skipped_rounds, instead increase the current number of rounds of the universally-invalid characteristics to search for and go to step 2.

    3. If this number was final_num_rounds, instead the search is finished.

This function is a Python generator function (see InvalidPropFinder), returning an iterator that yields 2-length tuples:

The argument prop_type is a particular Property such as XorDiff or LinearMask. For solver_name, see InvalidPropFinder. The optional arguments extra_chmodel_args and extra_invalidpropfinder_args can be given as dictionaries (in the form of **kwargs) containing additional arguments for ChModel/EncryptionChModel and InvalidPropFinder 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 (see round_based_ch_search).

This function reuses information from previous partitions \((E_0', E_1', E_2')\) to directly avoid some new partitions \((E_0, E_1, E_2)\) that don’t contain universally-invalid characteristics. Assume that no universally-invalid characteristic was found for the partition \((E_0', E_1', E_2')\), where \(E_0'\) covers from the \(a'\)-th round to the \(b'\)-th round (i.e., a'-›b') and \(E_2'\) covers c'-›d'. Then it holds that no universally-invalid characteristic can be found using InvalidPropFinder.find_next_invalidprop_miss_in_the_middle from any partition \((E_0, E_1, E_2)\) where \(E_0\) covers a-›a'-›b'-›b and \(E_2\) covers c-›c'-›d'-›d, that is, from any partition \((E_0, E_1, E_2)\) where \(E_0\) covers a-›b and \(E_2\) covers c-›d such that \(a \le a', b' \le b, c \le c\) and \(d' \le d\).

Note

Note that InvalidPropFinder contains other methods to search for universally-invalid characteristics (e.g., InvalidPropFinder.find_next_invalidprop_activebitmode or InvalidPropFinder.find_next_invalidprop_quantified_logic) which might find universally-invalid characteristics faster.

>>> # example of searching for XorDiff universally-invalid Characteristic over a BvFunction
>>> from cascada.differential.difference import XorDiff
>>> from cascada.smt.invalidpropsearch import round_based_invalidprop_search, INCREMENT_NUM_ROUNDS
>>> from cascada.primitives import speck
>>> Speck32_ks = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> iterator = round_based_invalidprop_search(Speck32_ks, 3, 3, XorDiff, "btor",
...     extra_invalidpropfinder_args={"solver_seed":0})
>>> for i, (tuple_rounds, tuple_chs) in enumerate(iterator):
...     print(tuple_rounds, ":", ', '.join([ch.srepr() for ch in tuple_chs]))
...     if i == 2: break  
(0, 1, 1, 1) : Ch(w=0, id=..., od=...), Ch(w=Infinity, id=..., od=...), Ch(w=0, id=..., od=...)
(0, 1, 1, 1) : Ch(w=0, id=..., od=...), Ch(w=Infinity, id=..., od=...), Ch(w=0, id=..., od=...)
(0, 1, 1, 1) : Ch(w=0, id=..., od=...), Ch(w=Infinity, id=..., od=...), Ch(w=0, id=..., od=...)
>>> # example of searching for LinearMask universally-invalid EncryptionCharacteristic over a Cipher
>>> from cascada.linear.mask import LinearMask
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> iterator = round_based_invalidprop_search(Speck32, 4, 5, LinearMask, "btor",
...     min_num_E0_rounds=2, extra_invalidpropfinder_args={"solver_seed":0})
>>> tuple_rounds, tuple_chs = next(iterator)
>>> print(tuple_rounds, ":", ', '.join([ch.srepr() for ch in tuple_chs]))
(0, 2, 1, 1) : Ch(w=0, id=0080 4021, od=0201 0200), Ch(w=Infinity, id=0201 0200, od=0000 0001), Ch(w=0, id=0000 0001, od=0004 0004)
>>> tuple_rounds, tuple_chs = next(iterator)
>>> print(tuple_rounds, ":", ', '.join([ch.srepr() for ch in tuple_chs]))
(0, 2, 1, 1) : Ch(w=0, id=0080 4021, od=0201 0200), Ch(w=Infinity, id=0201 0200, od=0080 e001), Ch(w=0, id=0080 e001, od=8002 8003)
>>> iterator.send(INCREMENT_NUM_ROUNDS)  # stop current num_rounds and increment by 1
>>> tuple_rounds, tuple_chs = next(iterator)
>>> print(tuple_rounds, ":", ', '.join([ch.srepr() for ch in tuple_chs]))
(0, 2, 1, 2) : Ch(w=0, id=0080 4021, od=0201 0200), Ch(w=Infinity, id=0201 0200, od=0080 4021), Ch(w=0, id=0080 4021, od=0201 0200)

Search for zero-probability (invalid) properties of iterated ciphers over multiple number of rounds.

Note

The Cipher.encryption of cipher must be a RoundBasedFunction including add_round_outputs calls in its eval.

This function is similar to round_based_invalidprop_search. The only differences are:

  • The function func (i.e., \(E \circ S\)) is the Cipher.encryption of the given cipher. Thus, \(S\) denote the skipped rounds of the encryption function.

  • Let \(K\) denote the Cipher.key_schedule of cipher, that is, the function whose outputs are the round keys used in \(E \circ S\). The generator InvalidPropFinder.find_next_invalidprop_miss_in_the_middle is called with the argument ch_model_external_E given as the characteristic model over \(K\) and with the argument exclude_zero_input_prop_external_E.

  • This function yields 2-length tuples where the 2nd element is a 4-length tuple; the last characteristic is the characteristic with probability 1 over \(K\). Thus, the concatenation of the first 3 characteristics is a universally-invalid characteristic over \(E\) where the round key properties are given by the outputs of the probability-one characteristic over \(K\).

Note that initial rounds are only skipped in the encryption function and not in the key-schedule function.

Note

Let (tuple_nr, tuple_ch) be an element yielded by round_based_invalidcipherprop_search.

Let \(\alpha_{K}\) be the input property of the 4-th characteristic in tuple_ch, and let \((\alpha_{E}, \beta_{E})\) be the input-output property pair of the concatenation of the first three characteristic in tuple_ch.

If tuple_nr[0] is 0, no initial rounds are skipped, and \((\alpha_{K}, \alpha_{E}) \mapsto \beta_{E}\) is a universally-invalid cipher characteristic (as defined in InvalidCipherPropFinder) of cipher.set_num_rounds_and_return(tuple_nr[1]+tuple_nr[2]+tuple_nr[3]), that is, the cipher with number of rounds tuple_nr[1]+tuple_nr[2]+tuple_nr[3].

If tuple_nr[0] is not zero then a universally-invalid cipher characteristic is also obtained but the underlying cipher is more difficult to generate due to the skipped initial rounds.

>>> from cascada.differential.difference import XorDiff
>>> from cascada.smt.invalidpropsearch import round_based_invalidcipherprop_search
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> iterator = round_based_invalidcipherprop_search(Speck32, 3, 3, XorDiff, "btor",
...     extra_invalidcipherpropfinder_args={"solver_seed":0})
>>> for i, (tuple_rounds, tuple_chs) in enumerate(iterator):
...     print(tuple_rounds, ":", ', '.join([ch.srepr() for ch in tuple_chs]))
...     if i == 1: break  
(0, 1, 1, 1) : Ch(w=0, id=0000 8000, od=8000 8002),
               Ch(w=Infinity, id=8000 8002, od=0000 8000),
               Ch(w=0, id=0000 8000, od=0002 0000),
               Ch(w=0, id=0000 0040 0000, od=0000 8000 8002)
(0, 1, 1, 1) : Ch(w=0, id=0000 8000, od=8000 8002),
               Ch(w=Infinity, id=8000 8002, od=0040 8000),
               Ch(w=0, id=0040 8000, od=8002 8000),
               Ch(w=0, id=0000 0040 0000, od=0000 8000 8002)