Grain of Salt

Grain-of-Salt is a tool that can generate CNFs for any shift register-based stream cipher. Currently, descriptions for ciphers Grain, Trivium, Bivium-B, HiTag2 and Crypto1 are included. The tool has 22 separate options, some implementing complex algorithms such Karnaugh table minimisation, greedy Monte-Carlo algorithms for best help bit generation, and extended monomial handling. The tool can be used to generate interesting statistics and visualisations if used in conjunction with CryptoMiniSat.

The code along with a 14-page description is available here.

Features

There are a number of features offered. The main features are:

  • Many ciphers already included. The program can generate problems for stream ciphers Grain, Trivium, Bivium, HiTag2 and Crypto1.
  • Extensible. Any shift-register and filter-based stream cipher can be added. Simply define the number of shift registers, the clocking, and the feedback and filter functions. All the rest is automatic.
  • Fast. Probem generation takes at most a couple of seconds. In contrast, the routines used (evaluate()) in Sage and Maple take minutes, sometimes hours.
  • Optimised CNFs. The CNF is optimized through extended monomials, Karnaugh tables (with espresso), value propagation, and equivalent variable replacement
  • Verbose CNF output. The CNF contains the definition of each and every variable and clause. These can be parsed up with CryptoMiniSat to get a full picure of what is causing propagations, conflicts, and how are variables learnt.
  • Automatic best help bit generation. It is not easy to find good bits to set as help bits. We provide two methods in Grain-of-Salt. The probabilistic method randomly picks variables from the correct range, and setst them randomly. Done enough time, this leads to a good average solving speed. The second method tries to find a good set of help bits through a greedy Monte-Carlo algorithm.

Example usage

Execute:

./grainofsalt --num 100 --outputs 90 --crypto grain --probBits 70

When finished, it generates 100 problems into the ‘satfiles’ directory. These problems are based on the
Grain cipher, with 90 bits of observed output, random key, random plaintext,
and 70 randomly given key bits, all set randomly to true or false.

Optimised CNFs

The generated CNF is optimised by first pushing it through a system that works with the ANF description of the cipher. All help bits and output bits are first propagated at the ANF level. Variable equivalences are also propagated, to further reduce the size of the resulting problem

Once the ANF has been propagated, the program can make an individual decision on each polynomial if it is best to represent it as an ANF or to represent it through Karnaugh tables. If the latter is made, it uses the esspresso logic minimiser as a built-in library. If the former is made, then monomials are not only re-used between polynomials, but are also made to work better in the CNF environment: they are extended. Simply put, this allows an inversion of variables when neccessary, minimising the resulting CNF description.

Extensibility

All that’s needed is the configuration of the cipher and the feedback and filter functions used. For the Grain cipher, these are the following:

sr_size = 80,80
linearizable_sr_during_init =
linearizable_sr_during_norm = 1
filters = 1
init_clock = 160
tweakable = sr1-0...63
one_out = sr1-64...79

Where the first line says that there are two shift registers, both of size 80. The second and third lines say that Grain’s second shift register is linear during normal (not initialisation) running. The frouth line says that there will be only one filter function used. The fifth line says that the initialisation for Grain is 160 clocks. The sixth line describes the tweakable bits (i.e. IV of the cipher), and the last line says that some of the bits of the second shift register must be filled with binary ones.

The description of the filter and feedback functions is similarly easy. For example, the feedback function of the second shift register of Grain is described as:

sr1-62
sr1-51
sr1-38
sr1-23
sr1-13
sr1-0

Where each line is a monomial, and each line is XOR-ed with the next one, to create the final polynomial. The feedback is essentially a copy-paste from the Grain description, and it describes the LFSR feedback: all monomials are of degree 1 here.

Fact propagation at the ANF level

The description of a cipher in CNF can loose a lot of structural information. In order to maximise the solving speed, we do the best we can at the ANF level before converting the cipher’s description to the CNF level. We do two important optimisations at the ANF level:

  • Value propagation. If variable v1 is found out to be TRUE, we replace all occurences of ‘v1’ with TRUE. This might imply newer similar variable settings. We therefore do this recursively.
  • Equivalent variable propagation. If variable ‘v2’ is found out to be equal to ‘v3’, we replace ‘v2’ with ‘v3’ at all places in the ANF. This might lead to new values or new equivalences. This is therefore done recursively with value propagation.

Complex example usage and explanation

Here is a somewhat complex example, with explanation:

./grainofsalt --outputs 160 --crypto grain --probBits 70 --init no 
              --base-shift 60,60 --xorcut 4 --num 100 --cnfDir GrainProblems

We are using the Grain cipher, with 160 bits of output, giving 70 randomly selected, randomly set help bits. The help bits will be selected from the shift registers 1 and 2, each from the range 60..140, since we shifted both shift registers by 60. There will be no initialisation used. The xor-cutting will be done at size 4 (instead of the default 7). There will be 100 such random problems generated, each to the directory ‘GrainProblems’.

Acknowledgements

Karsen Nohl has helped with some concepts, notably base-shifting. He was also responsible for starting the project.