Welcome to ArxPy’s documentation!¶
ArxPy 0.3¶
ArxPy is a python3 library to find XOR differential characteristics, rotational-XOR characteristics, and impossible differentials in ARX primitives (e.g., block ciphers) using SMT solvers.
ArxPy implements, improves and unifies the SMT-based methods of the following papers:
Towards Finding Optimal Differential Characteristics for ARX: Application to Salsa20
Observations on the SIMON Block Cipher Family
An Easy-to-Use Tool for Rotational-XOR Cryptanalysis of ARX Block Ciphers
Rotational-XOR Cryptanalysis of Reduced-round SPECK
A Bit-Vector Differential Model for the Modular Addition by a Constant
ArxPy provides a complete documentation and an extensive suite of tests.
Usage¶
First, the ARX cipher needs to be implemented following ArxPy interface.
There are several ARX ciphers implemented already (see the folder arxpy/primitives).
To implemented a new cipher, the easiest way is to take a similar cipher
already implemented as a template and modify the python code directly.
Searching the optimal XOR differential characteristic can be done easily with
the function round_based_search_SkCh(). For example, searching for the best
2-round and 3-round differential characteristics of Speck32_64 can be done as follows
>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.smt.search_differential import SkChSearchMode, DerMode, round_based_search_SkCh
>>> from arxpy.primitives import speck
>>> cipher = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> start_rounds, end_rounds = 4, 5
>>> round_based_search_SkCh(cipher, XorDiff, 0, "btor", start_rounds, end_rounds,
... DerMode.Default, SkChSearchMode.Optimal, True, 0, None)
Num rounds: 4
Best characteristic found:
(weight 5) 2800 0010 -> 8000 840a
Num rounds: 5
Best characteristic found:
(weight 9) 0211 0a04 -> 8000 840a
Apart from the cipher and the number of rounds to search, the function
round_based_search_SkCh() has several parameters to adapt the search as needed.
For example, by changing verbose_lvl`to `1 it is shown the intermediate
differences of the found characteristic and the weights of the non-linear operations.
This function stores each characteristic found as a ChFound object.
The explanation of these paremeters and the attributes of ChFound objects
can be found in the documentation.
Every function and class in ArxPy is documented with a description of
the object and with doctests!
If the argument check is True in round_based_search_SkCh(), the
weight of each characteristic found is checked by computing the empirical
weight (by sampling many plaintexts and keys and computing the
differential probability manually). This is useful since for
ARX ciphers the theoretical weight and the actual weight might differ
in some cases.
Searching the optimal related-key XOR differential characteristic can be done
in a similar way with the function round_based_search_RkCh(). For example,
searching for the best 4-round and 5-round related-key characteristics of
XTEA can be done as follows (this can take some minutes)
>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.smt.search_differential import RkChSearchMode, DerMode, round_based_search_RkCh
>>> from arxpy.primitives.xtea import XteaCipher
>>> cipher = XteaCipher
>>> round_based_search_RkCh(cipher, XorDiff, 0, 0, "btor", 4, 5, DerMode.Default,
... DerMode.Default, True, RkChSearchMode.OptimalMinSum, True, 0, None)
Num rounds: 4
Best related-key characteristic found:
E: (weight 0) 80000000 00000000 -> 00000000 80000000 | K: (weight 0) 80000000 00000000 80000000 00000000 -> 80000000 00000000 00000000 80000000
Num rounds: 5
Best related-key characteristic found:
E: (weight 0) 80000000 00000000 -> 00000000 00000000 | K: (weight 0) 80000000 00000000 00000000 00000000 -> 80000000 00000000 00000000 00000000 00000000
A related-key characteristic is split into two characteristics, one describing the propagation of differences through the key schedule (‘key_ch_found’) and another one describing the propagation of differences through the encryption function (‘enc_ch_found’).
To search for rotational-XOR characteristics, the same functions
round_based_search_SkCh() and round_based_search_RkCh() can be used
but using RXDiff as the difference_type argument. For example,
searching for 4-round and 5-round rotational-XOR differential characteristics
of CHAM_64_128 can be done in the following way
>>> from arxpy.differential.difference import RXDiff
>>> from arxpy.smt.search_differential import RkChSearchMode, DerMode, round_based_search_RkCh
>>> from arxpy.primitives import cham
>>> cipher = cham.get_Cham_instance(cham.ChamInstance.cham_64_128)
>>> round_based_search_RkCh(cipher, RXDiff, 0, 0, "btor", 4, 5, DerMode.Default,
... DerMode.Default, True, RkChSearchMode.FirstMinSumValid, True, 0, None)
Num rounds: 4
Best related-key characteristic found:
E: (weight 5) 8000 0002 8006 0004 -> 0100 0001 0080 0001 | K: (weight 0) 6123 0281 c246 6020 8000 8000 8000 8000 -> 8004 8681 0009 8000
Num rounds: 5
Best related-key characteristic found:
E: (weight 8) 0000 0002 8007 0005 -> 0002 0000 0000 0000 | K: (weight 0) 0202 2261 22e7 0503 0103 8000 8000 8000 -> 0404 0781 800b 0c00 0004
While there is no tutorial to learn how to use ArxPy yet,
the doctests and doctstrings from arxpy/smt/search.py provides
plenty of information and examples of searching characteristics.
Installation¶
ArxPy requires python3 (>= 3.7) and the following python libraries:
cython
sympy
bidict
cffi
pySMT
These libraries can be easily installed with pip:
pip install cython sympy bidict cffi pysmt
ArxPy also requires an SMT solver supporting the bit-vector theory, installed through pySMT. We recommend boolector.
pysmt-install --btor
Optionally, hypothesis and yices can be installed to run the tests, and sphinx and sphinx-rtd-theme to build the documentation.