cascada.smt.wrappedchmodel module

Wrap bit-vector functions for characteristics with one non-trivial transition.

`ChFuncAsOp`	Represent bit-vector operations wrapping functions of characteristic models.
`make_chfunc_as_op`	Return the `ChFuncAsOp` of the given characteristic model.
`ModelChFuncAsOp`	Represent models of `ChFuncAsOp` operations.
`make_chfuncasop_model`	Return the `ModelChFuncAsOp` of the given `ChFuncAsOp`.
`get_wrapped_chfunc`	Wrap and return the underlying bit-vector function of a characteristic model.
`get_wrapped_chcipher`	Wrap and return the underlying cipher of a characteristic model.
`get_wrapped_chmodel`	Return a wrapped model of the given characteristic model.
`get_wrapped_cipher_chmodel`	Return a wrapped model of the given cipher characteristic model.

class cascada.smt.wrappedchmodel.ChFuncAsOp(**kwargs)[source]

Bases: cascada.bitvector.operation.SecondaryOperation

Represent bit-vector operations wrapping functions of characteristic models.

Given a characteristic model (i.e., abstractproperty.chmodel.ChModel), a ChFuncAsOp operation is a SecondaryOperation that wraps the underlying bit-vector function of the characteristic model.

The operands of the wrapping operation are the input operands of the bit-vector function and its external variables. The eval method of wrapping operation calls the eval method of the bit-vector function and concatenates (with PropConcat) the outputs of the bit-vector function into a single bit-vector. This single bit-vector is the output of the wrapping operation.

This class is not meant to be instantiated but to provide a base class to define secondary operators wrapping bit-vector functions generated through make_chfunc_as_op.

ch_model: the characteristic model of the bit-vector function.

vrepr()[source]

Return an executable string representation.

This method returns a string so that the relation eval(expr.vrepr())) == expr holds when expr is a Term.

classmethod condition(*args)[source]: Check if the operands verify the restrictions of the operator.

classmethod output_width(*args)[source]: Return the bit-width of the resulting bit-vector.

classmethod eval(*args)[source]

Evaluate the operator with given operands.

This is an internal method that assumes the list args has been parsed. To evaluate a bit-vector operation, instantiate a new object with the operands as the object arguments (i.e., use the Python operator ()).

cascada.smt.wrappedchmodel.make_chfunc_as_op(ch_model)[source]

Return the ChFuncAsOp of the given characteristic model.

>>> from cascada.bitvector.core import Variable
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.wrappedchmodel import make_chfunc_as_op
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> plaintext = [Variable("p0", 16), Variable("p1", 16)]
>>> round_keys = [Variable("k0", 16), Variable("k1", 16)]
>>> Speck32.encryption.round_keys = round_keys
>>> Speck32.encryption(*plaintext, symbolic_inputs=True)  
((((((p0 >>> 7) + p1) ^ k0) >>> 7) + ((p1 <<< 2) ^ ((p0 >>> 7) + p1) ^ k0)) ^ k1,
(((p1 <<< 2) ^ ((p0 >>> 7) + p1) ^ k0) <<< 2) ^ (((((p0 >>> 7) + p1) ^ k0) >>> 7) + ((p1 <<< 2) ^ ((p0 >>> 7) + p1) ^ k0)) ^ k1)
>>> SpeckEncAsOp = make_chfunc_as_op(EncryptionChModel(Speck32, XorDiff))
>>> SpeckEncAsOp(*(plaintext + round_keys))
SpeckEncryption_2RAsOp(p0, p1, k0, k1)
>>> SpeckEncAsOp(*(plaintext + round_keys)).doit()  
Id((p1 <<< 2 ^ (p0 >>> 7 + p1) ^ k0) <<< 2 ^ (((p0 >>> 7 + p1) ^ k0) >>> 7 + (p1 <<< 2 ^ (p0 >>> 7 + p1) ^ k0)) ^ k1) ::
Id((((p0 >>> 7 + p1) ^ k0) >>> 7 + (p1 <<< 2 ^ (p0 >>> 7 + p1) ^ k0)) ^ k1)

class cascada.smt.wrappedchmodel.ModelChFuncAsOp[source]

Bases: object

Represent models of ChFuncAsOp operations.

The model of a ChFuncAsOp operation is the set of bit-vector constraints that models the propagation probability over the ChFuncAsOp operation (see abstractproperty.opmodel.OpModel).

Note

The model of a ChFuncAsOp operation models the probability that the input property \(\alpha\) propagates to the output property \(\beta\) over the ChFuncAsOp operation, and ignores the properties of the intermediate values of the ChFuncAsOp operation.

For the Difference/LinearMask property types, the model of a ChFuncAsOp models the probability of the differential/hull (instead of the probability of the characteristic).

The constraints of the model of a ChFuncAsOp operation are obtained from the underlying characteristic model. Specifically, the methods abstractproperty.opmodel.OpModel.validity_constraint, abstractproperty.opmodel.OpModel.pr_one_constraint and abstractproperty.opmodel.OpModel.weight_constraint of ModelChFuncAsOp used the methods abstractproperty.chmodel.ChModel.validity_assertions, abstractproperty.chmodel.ChModel.pr_one_assertions and abstractproperty.chmodel.ChModel.weight_assertions of the characteristic model respectively. Note that the external variables of validity_constraint, pr_one_constraint and weight_constraint include the intermediate properties in the characteristic model (the external variables of weight_constraint also include the intermediate weight variables).

The weight returned by the abstractproperty.opmodel.OpModel.decimal_weight method of ModelChFuncAsOp is computed by internally calling ChFinder.find_next_ch using the underlying characteristic model. In other words, the returned weight is a very weak approximation (with big abstractproperty.opmodel.OpModel.error) of the actual weight, since the returned weight is the weight of a random characteristic satisfying the underlying characteristic model.

This class is not meant to be instantiated but to provide a base class for models generated through make_chfuncasop_model.

property ch_model: The underlying characteristic model of ChFuncAsOp.

cascada.smt.wrappedchmodel.make_chfuncasop_model(my_chfunc_as_op)[source]

Return the ModelChFuncAsOp of the given ChFuncAsOp.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.wrappedchmodel import make_chfunc_as_op, make_chfuncasop_model
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> SpeckEncAsOp = make_chfunc_as_op(EncryptionChModel(Speck32, XorDiff))
>>> ModelSpeckEncAsOp = make_chfuncasop_model(SpeckEncAsOp)
>>> input_diff = [XorDiff(Constant(0, 16))]*4
>>> f = ModelSpeckEncAsOp(input_diff)
>>> print(f.vrepr())  
XorModelSpeckEncryption_2RAsOp([XorDiff(Constant(0x0000, width=16)), XorDiff(Constant(0x0000, width=16)),
    XorDiff(Constant(0x0000, width=16)), XorDiff(Constant(0x0000, width=16))])
>>> f.validity_constraint(XorDiff(Constant(0, 32)))  
(0x00000000 == (dx9_out :: dx7_out)) &
((~(dx1 << 0x0001) & dx1) == 0x0000) &
(((~((dx1 >>> 7) << 0x0001) ^ (dx1 << 0x0001)) & (~((dx1 >>> 7) << 0x0001) ^ (dx6 << 0x0001)) &
    ((dx1 >>> 7) ^ dx1 ^ dx6 ^ ((dx1 >>> 7) << 0x0001))) == 0x0000) &
(dx6 == dx7_out) & (((dx1 <<< 2) ^ dx6) == dx9_out)
>>> f.external_vars_validity_constraint(XorDiff(Constant(0, 32)))
[dx1, dx6, dx7_out, dx9_out]
>>> w = Variable("w", f.weight_width())
>>> f.weight_constraint(XorDiff(Constant(0, 32)), w)  
(0x00000000 == (dx9_out :: dx7_out)) &
(w == _w_tmp74c4f05762c354cc149091e363577700) &
(_w_tmp74c4f05762c354cc149091e363577700_0 == PopCount(dx1[14:])) &
(_w_tmp74c4f05762c354cc149091e363577700_1 == PopCount(~((~(dx1 >>> 7) ^ dx1) & (~(dx1 >>> 7) ^ dx6))[14:])) &
(_w_tmp74c4f05762c354cc149091e363577700_2 == 0b0) &
(_w_tmp74c4f05762c354cc149091e363577700_3 == 0b0) &
(_w_tmp74c4f05762c354cc149091e363577700 == ((0b0 :: _w_tmp74c4f05762c354cc149091e363577700_0) +
    (0b0 :: _w_tmp74c4f05762c354cc149091e363577700_1)))
>>> f.external_vars_weight_constraint(XorDiff(Constant(0, 32)), w)  
[_w_tmp74c4f05762c354cc149091e363577700, _w_tmp74c4f05762c354cc149091e363577700_0,
_w_tmp74c4f05762c354cc149091e363577700_1, _w_tmp74c4f05762c354cc149091e363577700_2,
_w_tmp74c4f05762c354cc149091e363577700_3, dx1, dx6, dx7_out, dx9_out]
>>> f.max_weight(), f.weight_width(), f.error(), f.num_frac_bits()
(30, 5, 30, 0)

cascada.smt.wrappedchmodel.get_wrapped_chfunc(ch_model)[source]

Wrap and return the underlying bit-vector function of a characteristic model.

Given a characteristic model (i.e., abstractproperty.chmodel.ChModel) of a bit-vector function \(f\), returns a functionally-equivalent (same input-output behaviour) bit-vector function \(g\) that contains the ChFuncAsOp of \(f\) and the output extraction (using PropExtract) of the single-output of ChFuncAsOp.

Note that the returned wrapped function \(g\) is a BvFunction (and not a RoundBasedFunction) even if func is a RoundBasedFunction.

>>> from cascada.bitvector.core import Constant
>>> from cascada.bitvector.ssa import RoundBasedFunction
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.smt.wrappedchmodel import get_wrapped_chfunc
>>> 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"])
>>> WrappedSpeck32KS = get_wrapped_chfunc(ch_model)
>>> ch_model.func.get_name(), WrappedSpeck32KS.get_name()
('SpeckKeySchedule_2R', 'WrappedSpeckKeySchedule_2R')
>>> ch_model.func.to_ssa(["mk0", "mk1", "mk2"], "k")  
SSA(input_vars=[mk0, mk1, mk2], output_vars=[mk2_out, k3_out, k8_out],
    assignments=[(k0, mk1 >>> 7), (k1, k0 + mk2), (k2, mk2 <<< 2), (k3, k2 ^ k1),
    (k4, mk0 >>> 7), (k5, k4 + k3), (k6, k5 ^ 0x0001), (k7, k3 <<< 2), (k8, k7 ^ k6),
    (mk2_out, Id(mk2)), (k3_out, Id(k3)), (k8_out, Id(k8))])
>>> WrappedSpeck32KS.to_ssa(["mk0", "mk1", "mk2"], "k") 
SSA(input_vars=[mk0, mk1, mk2], output_vars=[k1_out, k2_out, k3_out],
    assignments=[(k0, SpeckKeySchedule_2RAsOp(mk0, mk1, mk2)),
    (k1, PropExtract_{·, 15, 0}(k0)), (k2, PropExtract_{·, 31, 16}(k0)), (k3, PropExtract_{·, 47, 32}(k0)),
    (k1_out, Id(k1)), (k2_out, Id(k2)), (k3_out, Id(k3))])
>>> masterkey = [Constant(0, 16)]*3
>>> ch_model.func(*masterkey)
(0x0000, 0x0000, 0x0001)
>>> WrappedSpeck32KS(*masterkey)
(0x0000, 0x0000, 0x0001)
>>> issubclass(ch_model.func, RoundBasedFunction), issubclass(WrappedSpeck32KS, RoundBasedFunction)
(True, False)

cascada.smt.wrappedchmodel.get_wrapped_chcipher(ch_model)[source]

Wrap and return the underlying cipher of a characteristic model.

Given a characteristic model (i.e., abstractproperty.chmodel.CipherChModel) of a Cipher, returns a functionally-equivalent cipher where the key-schedule and encryption functions are wrapped by get_wrapped_chfunc.

If the given characteristic model is an abstractproperty.chmodel.EncryptionChModel of a Cipher.encryption, then a functionally-equivalent cipher is returned where only the encryption function is wrapped by get_wrapped_chfunc.

Note that the returned wrapped cipher is not iterated (see Cipher) even if the given cipher is iterated.

>>> from cascada.bitvector.core import Constant
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.wrappedchmodel import get_wrapped_chcipher
>>> 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)
>>> WrappedSpeck32 = get_wrapped_chcipher(ch_model)
>>> WrappedSpeck32Enc = WrappedSpeck32.encryption
>>> ch_model.func.get_name(), WrappedSpeck32Enc.get_name()
('SpeckEncryption_2R', 'WrappedSpeckEncryption_2R')
>>> ch_model.func.to_ssa(["p0", "p1"], "x")  
SSA(input_vars=[p0, p1], output_vars=[x7_out, x9_out], external_vars=[dk0, dk1],
    assignments=[(x0, p0 >>> 7), (x1, x0 + p1), (x2, x1 ^ dk0), (x3, p1 <<< 2), (x4, x3 ^ x2),
        (x5, x2 >>> 7), (x6, x5 + x4), (x7, x6 ^ dk1), (x8, x4 <<< 2), (x9, x8 ^ x7),
        (x7_out, Id(x7)), (x9_out, Id(x9))])
>>> WrappedSpeck32Enc.round_keys = ch_model.func.round_keys[:]
>>> WrappedSpeck32Enc.to_ssa(["p0", "p1"], "x")  
SSA(input_vars=[p0, p1], output_vars=[x1_out, x2_out], external_vars=[dk0, dk1],
    assignments=[(x0, SpeckEncryption_2RAsOp(p0, p1, dk0, dk1)),
        (x1, PropExtract_{·, 15, 0}(x0)), (x2, PropExtract_{·, 31, 16}(x0)),
        (x1_out, Id(x1)), (x2_out, Id(x2))])
>>> plaintext = Constant(1, 16), Constant(2, 16)
>>> list(ch_model.func(*plaintext, symbolic_inputs=True))  
[(((0x0202 ^ dk0) >>> 7) + (0x020a ^ dk0)) ^ dk1,
((0x020a ^ dk0) <<< 2) ^ (((0x0202 ^ dk0) >>> 7) + (0x020a ^ dk0)) ^ dk1]
>>> [x.doit() for x in WrappedSpeck32Enc(*plaintext, symbolic_inputs=True)]  
[Id(((0x0202 ^ dk0) >>> 7 + (0x020a ^ dk0)) ^ dk1),
Id((0x020a ^ dk0) <<< 2 ^ ((0x0202 ^ dk0) >>> 7 + (0x020a ^ dk0)) ^ dk1)]
>>> Speck32.num_rounds, WrappedSpeck32.num_rounds
(2, None)

cascada.smt.wrappedchmodel.get_wrapped_chmodel(ch_model)[source]

Return a wrapped model of the given characteristic model.

Given a characteristic model of a bit-vector function \(f\) (i.e., abstractproperty.chmodel.ChModel), a wrapped model is a characteristic model of the wrapped function of \(f\) through get_wrapped_chfunc. If the given characteristic model is an abstractproperty.chmodel.EncryptionChModel, the wrapped encryption is obtained through get_wrapped_chcipher.

The wrapped model only has one non-ModelIdentity transition: the ModelChFuncAsOp of the ChFuncAsOp of \(f\).

To avoid name collisions between the given characteristic model and the returned wrapped model (except for the external variables), an underscore is added to the variable prefix of the returned wrapped model.

>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.smt.wrappedchmodel import get_wrapped_chmodel
>>> 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)
>>> wrapped_ch_model = get_wrapped_chmodel(ch_model)
>>> wrapped_ch_model  
 EncryptionChModel(cipher=WrappedSpeckCipher_2R,
    input_diff=[XorDiff(_dp0), XorDiff(_dp1)],
    output_diff=[XorDiff(_dx1_out), XorDiff(_dx2_out)],
    external_var2diff=[(_dk0, XorDiff(0x0000)), (_dk1, XorDiff(0x0000))],
    assign_outdiff2op_model=[(XorDiff(_dx0), XorModelSpeckEncryption_2RAsOp([XorDiff(_dp0), XorDiff(_dp1), XorDiff(0x0000), XorDiff(0x0000)])),
        (XorDiff(_dx1_out), XorModelId(XorDiff(PropExtract_{·, 15, 0}(_dx0)))),
        (XorDiff(_dx2_out), XorModelId(XorDiff(PropExtract_{·, 31, 16}(_dx0))))])
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> 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"])
>>> wrapped_ch_model = get_wrapped_chmodel(ch_model)
>>> wrapped_ch_model  
ChModel(func=WrappedSpeckKeySchedule_2R,
    input_mask=[LinearMask(_mk0), LinearMask(_mk1), LinearMask(_mk2)],
    output_mask=[LinearMask(_mx1_out), LinearMask(_mx2_out), LinearMask(_mx3_out)],
    assign_outmask2op_model=[(LinearMask(_mx0), LinearModelSpeckKeySchedule_2RAsOp([LinearMask(_mk0), LinearMask(_mk1), LinearMask(_mk2)])),
        (LinearMask(_mx1_out), LinearModelId(LinearMask(PropExtract_{·, 15, 0}(_mx0)))),
        (LinearMask(_mx2_out), LinearModelId(LinearMask(PropExtract_{·, 31, 16}(_mx0)))),
        (LinearMask(_mx3_out), LinearModelId(LinearMask(PropExtract_{·, 47, 32}(_mx0))))])

cascada.smt.wrappedchmodel.get_wrapped_cipher_chmodel(cipher_ch_model)[source]

Return a wrapped model of the given cipher characteristic model.

Given a characteristic model of a Cipher (i.e., abstractproperty.chmodel.CipherChModel), a wrapped model is a characteristic model of the wrapped cipher through get_wrapped_chcipher.

The wrapped model only has two non-ModelIdentity transitions: the ModelChFuncAsOp of the ChFuncAsOp of the key-schedule function and the ModelChFuncAsOp of the ChFuncAsOp of the encryption function.

To avoid name collisions between the given cipher characteristic model and the returned wrapped model, an underscore is added to the variable prefix of the returned wrapped model.

>>> from cascada.differential.difference import RXDiff
>>> from cascada.differential.chmodel import CipherChModel
>>> from cascada.smt.wrappedchmodel import 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 = CipherChModel(Speck32, RXDiff)
>>> wrapped_ch_model = get_wrapped_cipher_chmodel(ch_model)
>>> wrapped_ch_model  
CipherChModel(ks_ch_model=ChModel(func=WrappedSpeckKeySchedule_1R,
    input_diff=[RXDiff(_dmk0), RXDiff(_dmk1)],
    output_diff=[RXDiff(_dk1_out), RXDiff(_dk2_out)],
    assign_outdiff2op_model=[(RXDiff(_dk0), RXModelSpeckKeySchedule_1RAsOp([RXDiff(_dmk0), RXDiff(_dmk1)])),
        (RXDiff(_dk1_out), RXModelId(RXDiff(PropExtract_{·, 15, 0}(_dk0)))),
        (RXDiff(_dk2_out), RXModelId(RXDiff(PropExtract_{·, 31, 16}(_dk0))))]),
    enc_ch_model=ChModel(func=WrappedSpeckEncryption_2R,
        input_diff=[RXDiff(_dp0), RXDiff(_dp1)],
        output_diff=[RXDiff(_dx1_out), RXDiff(_dx2_out)],
        external_var2diff=[(_dk1_out, RXDiff(_dk1_out)), (_dk2_out, RXDiff(_dk2_out))],
        assign_outdiff2op_model=[(RXDiff(_dx0), RXModelSpeckEncryption_2RAsOp([RXDiff(_dp0), RXDiff(_dp1), RXDiff(_dk1_out), RXDiff(_dk2_out)])),
            (RXDiff(_dx1_out), RXModelId(RXDiff(PropExtract_{·, 15, 0}(_dx0)))),
            (RXDiff(_dx2_out), RXModelId(RXDiff(PropExtract_{·, 31, 16}(_dx0))))]))