Issue with Present80 Cipher - findAllCharacteristics

[MoritzHuppert]

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

[MoritzHuppert]

Might be completely unrelated, but part of the input to STP (tmp/present0b2f20180f3157b66a3556d7ac13bf.stp) is this (strange looking) line:

ASSERT(NO) = 0hex0000000000000000);

So there might be a problem with the blockCharacteristic function: It would make sense that cryptosmt crashes right after the first found characteristic, as blockCharacteristic is called thereafter.

[MoritzHuppert]

Found the problem in stpcommands.py:

    # Only add state words (x, y, s)
    # TODO: extend for other ciphers
    filtered_words = {var_name: var_value for var_name, var_value in
                      characteristic.characteristic_data.items()
                      if var_name.startswith('w') or
                      var_name.startswith('y') or
                      var_name.startswith('s') or
                      var_name.startswith('v')}

The method does not filter out words for the present cipher (characteristic_data consists of capitalized symbols P, S).