http://kste.github.io/cryptosmt/ cannot be displayed (referred to in the short description).

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

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

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

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

What is the role of weight in cryptoSMT
What does it mean that weight is equals to hamming weight of the given variables.

in cipher/simon.py
line 97 x[i] = (x[i] <<< 1) & (x[i] <<< 8) ^ y[i] ^ (x[i] << 2)
i think LHS is x[i+1] ??

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

Caused by: yaml/pyyaml#576

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.

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

Are the weight's value inversely proportional to the cipher's security?

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

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

# 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

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