Giter Site home page Giter Site logo

cryptosmt's Introduction

CryptoSMT

CryptoSMT is an easy to use tool for cryptanalysis of symmetric primitives likes block ciphers or hash functions. It is based on SMT/SAT solvers like STP, Boolector, CryptoMiniSat and provides a simple framework to use them for cryptanalytic techniques.

Some of the features are:

  • Proof properties regarding the differential behavious of a primitive.
  • Find the best linear/differential trails.
  • Compute probability of a differential.
  • Find preimages for hash functions.
  • Recover a secret key.

The following primitives are supported by CryptoSMT at the moment:

Block Ciphers
  • Simon[3],
  • Speck[3],
  • Skinny[4],
  • Present[5],
  • Midori[6],
  • LBlock[7],
  • Sparx[8],
  • Twine[9],
  • Noekeon[10],
  • Prince[11],
  • Mantis[4],
  • Speckey[8],
  • Rectangle[12],
  • Cham[13],
  • CRAFT[21],
  • TRIFLE[22]
Hash Functions
  • Keccak[14]
Stream Ciphers
  • Salsa[15],
  • ChaCha[16]
Authenticated Encryption Ciphers
  • Ketje[17],
  • Ascon[18]
Message Authentication Codes
  • Chaskey[19],
  • SipHash[20]

Please note that at the moment not all features are available for all ciphers. A detailed description on the application of this tool on the SIMON block ciphers and how a differential/linear model for SIMON can be constructed is given in [1].

Installation

CryptoSMT requires you to have STP and Cryptominisat installed and setup the paths to the binaries in config.py. Further it requires the pyyaml which you can install using

$ pip3 install pyyaml

The easiest way to get all the external tools to run is with the provided Dockerfile. You can build a basic image using:

cd docker/
docker build -t cryptosmt .

This includes building minisat, cryptominisat, STP, boolector and all dependencies. You can then run the image with:

docker run -it cryptosmt

which gives you a ready to use setup of CryptoSMT.

Usage

As an example we will look at how CryptoSMT can be used to find the optimal differential characteristics for the block cipher Simon.

Running the command

$ python3 cryptosmt.py --cipher simon --rounds 8 --wordsize 16

will start the search for the optimal trail and you will see as output

simon - Rounds: 8 Wordsize: 16
---
Weight: 0 Time: 0.0s
Weight: 1 Time: 0.08s
Weight: 2 Time: 0.16s
Weight: 3 Time: 0.44s
Weight: 4 Time: 0.74s
Weight: 5 Time: 0.89s
...

CryptoSMT tries to find a differential trail with a given weight w_i. If no such trail exists w_i is incremented and the search continues. In this case the best trail has a weight of 18 and can be quickly found:

Characteristic for simon - Rounds 8 - Wordsize 16 - Weight 18 - Time 13.15s
Rounds  x       y       w
-------------------------------
0       0x0040  0x0191  -2
1       0x0011  0x0040  -4
2       0x0004  0x0011  -2
3       0x0001  0x0004  -2
4       0x0000  0x0001  -0
5       0x0001  0x0000  -2
6       0x0004  0x0001  -2
7       0x0011  0x0004  -4
8       0x0040  0x0011  none

Weight: 18

CryptoSMT prints out the difference in the two state words x_i, y_i and the probability for the transition between two rounds w_i.

Adding a cipher to the CryptoSMT's cipher suites

Let's say you want to add "NewCipher" to the tool:

  1. Make a copy from an example in "./ciphers/" which is similar to the design you want to analyze (for example if you want an ARX, Speck might be a good start) and rename it to "NewCipher.py".
  2. Modify the content of "NewCipher.py" to adapt it to your cipher (here it's best to look at some examples, as it depends a lot on design).
  3. Update the file "cryptosmt.py": Add "NewCipher" in the import (line 8), and include it in the tool by adding it to the ciphersuite (line 25).
  4. Run "python3 cryptosmt.py --cipher NewCipher" to see if it works.

How does it work?

We can describe the process of the CryptoSMT as the following steps:

  1. It creates an stp file which contains the SMT model of the differential cryptanaysis of the given cipher in CVC format (this file is placed in "./tmp/" folder)
  2. After generation of SMT model in CVC format, it calls an SMT solver to solve the generated model. The STP is used by default as SMT solver. You can also use the Boolector as SMT solver.
  3. The SMT model contains some inherent constraints which are used for modeling the differential propagation rules, and some additional constraints which are used to model the outside counditions like the fixed input/output differentials values.
  4. One of the additional constraints is the starting weight (of the differential probability) constraint. The first SMT model is generated with the starting weight, and this model is changed repeatedly by increasing the weight by one, and each time, it's satisfiablity is checked by an SMT solver. The goal is to find the minimum weight which makes the model satisfiable.
  5. If the SMT model is satisfiable for the first time, the weight (of the differential probability) which is used, is reteurned as the minimum weight (of the differential probability) as one of the output, and the process is stoped.

These processes are almost realted to the mod0, which is used to find the best differential with maximum (minimum) differential probablity (weight).

Credits

Special thanks to Ralph Ankele and Hosein Hadipour for their extensive contributions!

References

[1] Observations on the SIMON block cipher family

[2] Mind the Gap - A Closer Look at the Security of Block Ciphers against Differential Cryptanalysis

[3] The SIMON and SPECK Families of Lightweight Block Ciphers

[4] The SKINNY Family of Block Ciphers and its Low-Latency Variant MANTIS

[5] PRESENT: An Ultra-Lightweight Block Cipher

[6] Midori: A Block Cipher for Low Energy (Extended Version)

[7] LBlock: A Lightweight Block Cipher

[8] Design Strategies for ARX with Provable Bounds: SPARX and LAX (Full Version)

[9] TWINE: A Lightweight Block Cipher for Multiple Platforms

[10] Nessie Proposal: NOEKEON

[11] PRINCE - A Low-latency Block Cipher for Pervasive Computing Applications (Full version)

[12] RECTANGLE: A Bit-slice Lightweight Block Cipher Suitable for Multiple Platforms

[13] CHAM: A Family of Lightweight Block Ciphers for Resource-Constrained Devices

[14] The Keccak reference

[15] The Salsa20 family of stream ciphers

[16] ChaCha, a variant of Salsa20

[17] CAESAR submission: Kђѡїђ v2

[18] Ascon v1.2 Submission to the CAESAR Competition

[19] Chaskey: An Efficient MAC Algorithm for 32-bit Microcontrollers

[20] SipHash: a fast short-input PRF

[21] CRAFT: Lightweight Tweakable Block Cipher with Efficient Protection Against DFA Attacks

[22] TRIFLE

BibTex

@misc{CryptoSMT-ref,
    author = {{Stefan Kölbl}},
    title = {{CryptoSMT: An easy to use tool for cryptanalysis of symmetric primitives}},
    note = {\url{https://github.com/kste/cryptosmt}},
}

cryptosmt's People

Contributors

hadipourh avatar kste avatar lightbit avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar

cryptosmt's Issues

Loading Example YAML Files is Broken

Caused by: yaml/pyyaml#576


doc = yaml.load(input_file)

Due to the "breaking" change introduced in PyYAML 6.0, the use of --inputfile argument now throws TypeError due to the missing Loader argument. It seems like one of the following has to happen to make it work again: (1) update CryptoSMT code to be compliant with PyYAML 6.0, or (2) cap PyYAML version to < 6.0 then update Dockerfile and README accordingly.

OSError: [Errno 13] Permission denied

While executing cryptosmt, i used to get the following error. Can you please me

python cryptosmt.py --inputfile examples/speck64_14rounds_lux.yaml

Traceback (most recent call last):
File "cryptosmt.py", line 155, in
main()
File "cryptosmt.py", line 150, in main
startTool(params)
File "cryptosmt.py", line 53, in startTool
searchDifferential.computeProbabilityOfDifferentials(cipher, toolParameters)
File "/home/naresh/Desktop/SMT/cryptosmt-master/cryptanalysis/differentialSearch.py", line 52, in computeProbabilityOfDifferentials
"tmp/{}{}.stp".format(cipher.getName(), randomStringForTMPFile)])
File "/usr/lib/python2.7/subprocess.py", line 566, in check_output
process = Popen(stdout=PIPE, _popenargs, *_kwargs)
File "/usr/lib/python2.7/subprocess.py", line 710, in init
errread, errwrite)
File "/usr/lib/python2.7/subprocess.py", line 1327, in _execute_child
raise child_exception
OSError: [Errno 13] Permission denied

differential characteristics

# While executing cryptosmt, i used to get the following error. Can you please help me

python cryptosmt.py --inputfile examples/salsa20/testpath.yaml

Starting search for characteristic with minimal weight
salsa - Rounds: 3 Wordsize: 32

Weight: 0 Time: 0.0s
<open file 'tmp/salsa32.stp', mode 'w' at 0x7f7eb7ebf9c0>
Traceback (most recent call last):
File "cryptosmt.py", line 207, in
main()
File "cryptosmt.py", line 203, in main
startsearch(params)
File "cryptosmt.py", line 48, in startsearch
search.findMinWeightCharacteristic(cipher, tool_parameters)
File "/home/nagendar/Desktop/temp/cryptosmt-master/cryptanalysis/search.py", line 158, in findMinWeightCharacteristic
result = solveSTP(stp_file)
File "/home/nagendar/Desktop/temp/cryptosmt-master/cryptanalysis/search.py", line 313, in solveSTP
result = subprocess.check_output(stp_parameters)
File "/usr/lib/python2.7/subprocess.py", line 567, in check_output
process = Popen(stdout=PIPE, *popenargs, **kwargs)
File "/usr/lib/python2.7/subprocess.py", line 711, in init
errread, errwrite)
File "/usr/lib/python2.7/subprocess.py", line 1343, in _execute_child
raise child_exception
OSError: [Errno 13] Permission denied

cryptosmt

Hi kste,

Great project !
I am also working on automatic cryptanalysis based on Mixed-integer linear programming (MILP), instead of SAT.

See

  1. http://eprint.iacr.org/2013/676
  2. http://eprint.iacr.org/2014/747

One main drawback of the MILP based method is that it is not suitable for ARX construction (modelling the differential behavior of mod addition introduces too many variables and constraints), and I think the method presented in "Towards Finding Optimal Differential Characteristics for ARX: Application to Salsa20" is very promising for ARX. And I think the framework you implement is very interesting and will be very useful.

I see that you have implemented the examples of SIMON and SPECK. May I know the results you have obtained using this framework? For example, can you use your framework to prove that SPECK is secure against basic differential attack (based on differential characteristic)? What is the longest/best characteristic you've got for SIMON and SPECK?

Best regards,
Siwei Sun

E-mail: sunsiwei at iie.ac.cn

Issue with Present80 Cipher - findAllCharacteristics

Hey,

firstly, I really appreciate the work you have put in this project. The amount of supported ciphers that have accumulated over the years is impressive.
I am currently working on a different research project that integrates the cryptosmt solver in a larger cryptanalysis process. One of the requirements is to collect minimal weight differential trails of lightweight block ciphers, such as Speck32/64 or Present80. To accomplish this requirement, I am using the cryptosmt method findAllCharacteristics (mode 2) on the respective cipher. While this works great for Speck32/64, I get the following output (including an error) for Present80:

Characteristic for present - Rounds 2 - Wordsize 64- Weight 4
Rounds  S                   P                   w                   
-------------------------------------------------------------------
0       0x000000000000000B  0x0000000000000008  -2                  
1       0x0001000000000000  0x0007000000000000  -2                  
2       0x0000100010001000  none                none                

Weight: 4
Unresolved symbol:NO
Fatal Error: 
STP Error: 
Traceback (most recent call last):
  File "cryptosmt/cryptosmt.py", line 61, in startsearch
    search.findAllCharacteristics(cipher, tool_parameters)
  File "cryptosmt/cryptanalysis/search.py", line 215, in findAllCharacteristics
    result = solveSTP(stp_file)
  File "cryptosmt/cryptanalysis/search.py", line 312, in solveSTP
    result = subprocess.check_output(stp_parameters)
  File "opt/anaconda3/envs/project/lib/python3.9/subprocess.py", line 424, in check_output
    return run(*popenargs, stdout=PIPE, timeout=timeout, check=True,
  File "opt/anaconda3/envs/project/lib/python3.9/subprocess.py", line 528, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['stp/build/stp', 'tmp/present0b2f20180f3157b66a3556d7ac13bf.stp', '--CVC']' returned non-zero exit status 255.

Note that I am using a starting weight of 4 and search for two rounds of Present encryption. It outputs one minimal weight differential trail and terminates right after. It seems to be an error with STP ('non-zero exit status 255'). Did you see this error before, or do you have any idea how to solve this issue?

With kind regards
Moritz Huppert

S2 rotate in simon

in simon.py line 87 i think the argument for right rotate for 6 is wrong,
we need to rotate left for twice only S2

def getDependentBitsForAND(self, x_in, wordsize):
"rotate_right(diff, 6) & (rotate_left(diff, 1)) & rotate_left(diff, 8);"
command = "({0} & (
{1}) & {2})".format(StpCommands().getStringRightRotate(x_in, 6, wordsize),
StpCommands().getStringLeftRotate(x_in, 1, wordsize),
StpCommands().getStringLeftRotate(x_in, 8, wordsize));
return command

Mode 4 issue

Hi,
I executed the following command and obtained the results given below. I have a few queries regarding the output:

  1. Current probability is greater than 1. What does the 'current probability' depict here?
  2. Can you please direct me towards the documentation to highlight the significance of the words 'trails' and 'weights'

python3 cryptosmt.py --cipher present --rounds 1 --wordsize 64 --mode 4 --boolector Finding all trails of weight 0 Solutions: 0 Finding all trails of weight 1 Solutions: 0 Finding all trails of weight 2 Solutions: 384 Trails found: 384 Current Probability: 6.584962500721156 Time: 7.89s Finding all trails of weight 3 Solutions: 1152 Trails found: 1536 Current Probability: 7.906890595608519 Time: 18.62s Finding all trails of weight 4 Solutions: 69120 Trails found: 70656 Current Probability: 12.154818109052105 Time: 611.57s Finding all trails of weight 5 Solutions: 38478 Trails found: 109134 Current Probability: 12.49246348266757 Time: 1012.54s

"docker build -t cryptosmt ."cannot be executed

My name is Riko and I am a graduate student in Japan.
I'm planning to use this tool for my research.
When I built the dockerfile on wsl2 kali linux, I got the following error. Is there a solution to this problem?

┌──(xxx㉿LAPTOP-Q28HUGQ8)-[/mnt/c/users/xxxx/desktop/cryptosmt-master/cryptosmt-master/docker]
[+] Building 2.6s (10/27)
=> [internal] load build definition from Dockerfile 0.0s
=> => transferring dockerfile: 38B 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 2B 0.0s
=> [internal] load metadata for docker.io/library/debian:latest 2.0s
=> [ 1/24] FROM docker.io/library/debian:latest@sha256:2906804d2a64e8a13a434a1a127fe3f6a28bf7cf3696be4223b06276f 0.0s
=> CACHED [ 2/24] RUN apt-get update && apt-get install -y git build-essential cmake wget curl 0.0s
=> CACHED [ 3/24] WORKDIR /home/tools/ 0.0s
=> CACHED [ 4/24] RUN git clone https://github.com/niklasso/minisat && git clone https://github.com/msoos/cr 0.0s
=> CACHED [ 5/24] WORKDIR /home/tools/minisat 0.0s
=> CACHED [ 6/24] RUN apt-get install -y zlib1g-dev 0.0s
=> ERROR [ 7/24] RUN make && make install 0.6s

[ 7/24] RUN make && make install:
#10 0.412 Compiling: build/release/minisat/simp/Main.o
#10 0.447 In file included from minisat/simp/Main.cc:26:
#10 0.447 ./minisat/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
#10 0.447 285 | fprintf(stderr, "%4"PRIi64, range.begin);
#10 0.447 | ^
#10 0.447 ./minisat/utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
#10 0.447 291 | fprintf(stderr, "%4"PRIi64, range.end);
#10 0.447 | ^
#10 0.447 ./minisat/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
#10 0.447 293 | fprintf(stderr, "] (default: %"PRIi64")\n", value);
#10 0.447 | ^
#10 0.503 In file included from ./minisat/core/Dimacs.h:27,
#10 0.503 from minisat/simp/Main.cc:27:
#10 0.503 ./minisat/core/SolverTypes.h:55:16: error: friend declaration of 'Minisat::Lit mkLit(Minisat::Var, bool)' specifies default arguments and isn't a definition [-fpermissive]
#10 0.503 55 | friend Lit mkLit(Var var, bool sign = false);
#10 0.503 | ^~~~~
#10 0.503 ./minisat/core/SolverTypes.h:63:14: error: friend declaration of 'Minisat::Lit Minisat::mkLit(Minisat::Var, bool)' specifies default arguments and isn't the only declaration [-fpermissive]
#10 0.503 63 | inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
#10 0.503 | ^~~~~
#10 0.503 ./minisat/core/SolverTypes.h:55:16: note: previous declaration of 'Minisat::Lit Minisat::mkLit(Minisat::Var, bool)'
#10 0.503 55 | friend Lit mkLit(Var var, bool sign = false);
#10 0.503 | ^~~~~
#10 0.542 make: *** [Makefile:129: build/release/minisat/simp/Main.o] Error 1


executor failed running [/bin/sh -c make && make install]: exit code: 2

Error: BVTypeCheck: terms in atomic formulas must be of equal length

When I execute CryptoSMT with simon32_4rounds_iterative.yaml
We got the following error

Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length

362:(EQ
360:0b10000000000000000
46:weight)
0
stp: Error: BVTypeCheck: terms in atomic formulas must be of equal length
Traceback (most recent call last):
File "cryptosmt.py", line 154, in
main()
File "cryptosmt.py", line 149, in main
startTool(params)
File "cryptosmt.py", line 52, in startTool
searchDifferential.computeProbabilityOfDifferentials(cipher, toolParameters)
File "/home/naresh/Desktop/SMT/cryptosmt-master/cryptanalysis/differentialSearch.py", line 52, in computeProbabilityOfDifferentials
"tmp/{}{}.stp".format(cipher.getName(), randomStringForTMPFile)])
File "/usr/lib/python2.7/subprocess.py", line 573, in check_output
raise CalledProcessError(retcode, cmd, output=output)
subprocess.CalledProcessError: Command '['../stp/stp', '--exit-after-CNF', '--output-CNF', 'tmp/simon83f626e417821d2ab9c40aedd579e7.stp']' returned non-zero exit status 255

Docmentation

Dear Author
May I know how the tool is implemented, what are the underlying algorithms/procedures.

Algorithms/procedures

Dear Author,
May I know how the tool was developed. What are different algorithms used. Can you explain what are the steps involved.What is the input for SMT, from there what is the output to STP/cryptominisat

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.