update cipher suite

ciphers/craft.py

@@ -30,7 +30,7 @@ class CraftCipher(AbstractCipher):
 
     def constraints_by_craft_sbox(self, variables):
         """
-        generate constarints related to sbox
+        generate constraints for S-box
         """
         di = variables[0:4]
         do = variables[4:8]        
@@ -158,7 +158,7 @@ def setupCraftRound(self, stp_file, x_in, y, z, x_out, w, wordsize):
             command += "ASSERT(" + z + "[%d:%d]" % (4*i + 3, 4*i) + \
                 " = " + y + "[%d:%d]" % (4*self.PN[i] + 3,
                                          4*self.PN[i]) + ");\n"
-        # Sbox layer        
+        # Sbox layer     
         for i in range(16):
             variables = ["{0}[{1}:{1}]".format(z, 4*i + 3),
                          "{0}[{1}:{1}]".format(z, 4*i + 2),

ciphers/present.py

@@ -2,6 +2,8 @@
 Created on Dec 27, 2016
 
 @author: ralph
+@modifed by Hosein Hadipour on Jun 12, 2022: 
+Speeding up the tool by using an optimized S-box encoding
 '''
 
 from parser import stpcommands
@@ -10,11 +12,29 @@
 
 class PresentCipher(AbstractCipher):
     """
-    Represents the differential behaviour of PRESENT and can be used
+    Represents the differential behavior of PRESENT and can be used
     to find differential characteristics for the given parameters.
     """
 
     name = "present"
+    present_sbox_rpos = "(p1 | ~p0) & (~a3 | p0) & (~a2 | p0) & (~a1 | p0) & (~a0 | p0) & (a3 | a2 | a1 | ~p2) & (a0 | b3 | b1 | ~p2) & (a0 | b3 | ~b1 | p2) & (a0 | ~b3 | b1 | p2) & (~a3 | ~a1 | ~a0 | b3 | ~b1) & (~a2 | ~a1 | a0 | b3 | b1) & (~a3 | a2 | a1 | a0 | b0) & (~a2 | ~a1 | b3 | b1 | ~p2) & (b3 | ~b2 | b1 | ~b0 | ~p2) & (~a2 | a1 | a0 | b2 | p2) & (~a3 | ~a1 | a0 | ~b1 | p2) & (a3 | a2 | ~b3 | ~b1 | p2) & (~a2 | ~a1 | b3 | ~b1 | p2) & (~a2 | a1 | ~a0 | ~b0 | p2) & (a2 | ~a1 | b2 | ~b0 | p2) & (a3 | ~a1 | ~b3 | b0 | p2) & (a3 | a1 | ~b1 | b0 | p2) & (b3 | b2 | b1 | b0 | ~p0) & (a3 | ~a2 | a1 | ~a0 | b3 | ~b1) & (a2 | ~a1 | a0 | ~b3 | b2 | ~b0) & (a2 | ~a1 | a0 | ~b2 | ~b1 | ~b0) & (~a2 | a1 | a0 | b2 | ~b1 | ~b0) & (a3 | ~a1 | ~a0 | ~b3 | b1 | ~b0) & (~a3 | a2 | a0 | ~b2 | b1 | b0) & (a3 | a2 | ~b3 | b2 | b1 | ~p2) & (~a1 | ~a0 | b3 | ~b2 | ~b0 | p2) & (a2 | a1 | b3 | b1 | ~b0 | p2) & (~a3 | ~a2 | a1 | ~b2 | b0 | p2) & (a2 | a1 | b3 | ~b1 | b0 | p2) & (a3 | b3 | ~b2 | b1 | b0 | p2) & (a3 | a1 | b2 | b1 | b0 | ~p1) & (a3 | a2 | b3 | b2 | b0 | ~p0) & (a3 | a1 | b3 | b2 | b0 | ~p0) & (~a3 | ~a2 | a1 | b3 | ~b2 | ~b1 | b0) & (~a3 | a2 | ~a1 | a0 | b3 | ~b2 | ~p2) & (~a3 | ~a2 | a1 | a0 | ~b2 | b1 | ~p2) & (~a2 | a1 | ~a0 | b3 | ~b1 | b0 | ~p2) & (a2 | ~a1 | ~a0 | ~b2 | ~b1 | b0 | ~p2) & (a2 | ~a1 | ~a0 | ~b3 | b1 | b0 | ~p2) & (~a2 | a1 | ~a0 | ~b3 | b1 | b0 | ~p2) & (~a3 | ~a2 | ~a0 | ~b3 | b1 | ~p1 | ~p0) & (~a3 | a2 | a1 | ~a0 | ~b0 | ~p1 | ~p0) & (~a2 | ~a1 | ~b3 | ~b1 | ~p2 | ~p1 | ~p0) & (~a0 | ~b3 | ~b2 | ~b1 | ~p2 | ~p1 | ~p0) & (a3 | ~a2 | ~a1 | ~b0 | ~p2 | ~p1 | ~p0) & (~a0 | ~b3 | b2 | ~b1 | p2 | ~p1 | ~p0) & (~a2 | a1 | a0 | ~b3 | ~b2 | ~b0 | ~p1 | ~p0) & (~a3 | a2 | a1 | ~b3 | ~b1 | ~p2 | ~p1 | ~p0) & (~a3 | a2 | ~a1 | ~a0 | ~b2 | p2 | ~p1 | ~p0) & (a2 | a1 | ~a0 | ~b3 | b1 | b0 | p2 | ~p1 | ~p0) & (a2 | a1 | b3 | b1 | ~p2)"
+
+    def constraints_by_present_sbox(self, variables):
+        """
+        generate constraints for S-box
+        """
+        di = variables[0:4]
+        do = variables[4:8]        
+        w = variables[9:12]        
+        command = self.present_sbox_rpos
+        for i in range(4):
+            command = command.replace("a%d" % (3 - i), di[i])
+            command = command.replace("b%d" % (3 - i), do[i])            
+            if i <= 2:
+               command = command.replace("p%d" % (2 - i), w[i])            
+        command = "ASSERT(%s = 0bin1);\n" % command
+        command += "ASSERT(%s = 0bin0);\n" % variables[8]        
+        return command
 
     def getFormatString(self):
         """
@@ -104,7 +124,8 @@ def setupPresentRound(self, stp_file, s_in, p, s_out, w, wordsize):
                          "{0}[{1}:{1}]".format(w, 4*i + 2),
                          "{0}[{1}:{1}]".format(w, 4*i + 1),
                          "{0}[{1}:{1}]".format(w, 4*i + 0)]
-            command += stpcommands.add4bitSbox(present_sbox, variables)
+            # command += stpcommands.add4bitSbox(present_sbox, variables)
+            command += self.constraints_by_present_sbox(variables)
 
 
         stp_file.write(command)

ciphers/presentla.py

@@ -0,0 +1,129 @@
+'''
+Created on Jun 12, 2022
+
+@author by Hosein Hadipour
+'''
+
+from parser import stpcommands
+from ciphers.cipher import AbstractCipher
+
+
+class PresentLACipher(AbstractCipher):
+    """
+    Represents the linear behavior of PRESENT and can be used
+    to find linear characteristics for the given parameters.
+    """
+
+    name = "presentla"
+    # Encode the correlation ignoring the signs (it is not the squared correlation)
+    present_sbox_rpos = "(~a2 | p0) & (~b3 | p0) & (~b1 | p0) & (~b0 | p0) & (~p1 | p0) & (~a3 | ~a0 | ~b2 | p1) & (a3 | a2 | a1 | a0 | ~b1) & (a2 | a1 | b3 | b1 | ~p1) & (a2 | a0 | b3 | ~b2 | p1) & (~a3 | ~b3 | ~b2 | b1 | p1) & (~a3 | ~a0 | ~b3 | ~b0 | p1) & (~a3 | b3 | ~b1 | ~b0 | p1) & (a1 | b3 | ~b2 | b0 | p1) & (~a3 | ~a2 | ~a1 | ~b3 | ~b2 | ~b1) & (a3 | ~a2 | ~a1 | ~b3 | b2 | ~b1) & (~a2 | a1 | a0 | ~b3 | ~b2 | p1) & (~a3 | ~a2 | ~a1 | a0 | b2 | p1) & (~a2 | a1 | a0 | b3 | b2 | p1) & (~a3 | ~a2 | ~a1 | b3 | ~b1 | p1) & (a2 | ~a1 | ~b3 | ~b2 | ~b1 | p1) & (a3 | a2 | b3 | b2 | ~b1 | p1) & (a3 | ~a1 | a0 | b3 | b1 | p1) & (a2 | ~a1 | a0 | b2 | b1 | p1) & (a3 | a2 | ~a1 | ~a0 | ~b0 | p1) & (a3 | ~a2 | a1 | ~a0 | ~b0 | p1) & (a3 | ~a2 | a0 | b2 | b0 | p1) & (a2 | ~a0 | b3 | b2 | b0 | p1) & (~a1 | a0 | ~b3 | ~b1 | b0 | p1) & (a1 | ~a0 | ~b2 | ~b1 | b0 | p1) & (a3 | a2 | ~a1 | b1 | b0 | p1) & (a2 | a1 | ~b3 | b1 | b0 | p1) & (~a2 | ~a0 | b2 | b1 | b0 | p1) & (~a3 | a2 | ~a1 | ~b3 | ~b1 | b0 | p1) & (~a3 | ~a2 | a1 | ~b3 | ~b1 | b0 | p1) & (a3 | ~a2 | ~a0 | b3 | ~b1 | b0 | p1) & (a3 | ~a1 | ~a0 | ~b3 | b1 | b0 | p1) & (a1 | a0 | b1 | ~b0 | p3 | p2 | p1) & (a3 | a2 | a1 | b2 | p3 | p2 | ~p0) & (a3 | b3 | b2 | b1 | p3 | p2 | ~p0) & (~a3 | a2 | a1 | a0 | b2 | p3 | p2 | p1) & (a3 | ~a2 | ~a1 | ~b2 | ~b0 | p3 | p2 | p1 | ~p0) & (~a3 | a2 | ~a1 | b2 | ~p1) & (~b3 | b2 | ~b1 | ~p1) & (a3 | ~b3 | ~b2 | b1 | ~p1) & (a3 | ~a2 | ~a1 | ~p1) & (a2 | a1 | ~b3 | ~b1 | ~p1) & (a3 | b3 | ~b2 | ~b1 | ~p1) & (~a2 | ~a1 | b3 | b1 | ~p1) & (~a3 | ~a2 | a1 | b2 | ~p1) & (~p2) & (~p3)"
+
+    def constraints_by_present_sbox(self, variables):
+        """
+        generate constraints for S-box
+        """
+        di = variables[0:4]
+        do = variables[4:8]        
+        w = variables[8:12]
+        command = self.present_sbox_rpos
+        for i in range(4):
+            command = command.replace("a%d" % (3 - i), di[i])
+            command = command.replace("b%d" % (3 - i), do[i])            
+            command = command.replace("p%d" % (3 - i), w[i])  
+        command = "ASSERT(%s = 0bin1);\n" % command        
+        return command
+
+    def getFormatString(self):
+        """
+        Returns the print format.
+        """
+        return ['S', 'P', 'w']
+
+    def createSTP(self, stp_filename, parameters):
+        """
+        Creates an STP file to find a characteristic for PRESENT with
+        the given parameters.
+        """
+
+        wordsize = parameters["wordsize"]
+        rounds = parameters["rounds"]
+        weight = parameters["sweight"]
+
+        if wordsize != 64:
+            print("Only wordsize of 64-bit supported.")
+            exit(1)
+
+        with open(stp_filename, 'w') as stp_file:
+            header = ("% Input File for STP\n% PRESENT w={}"
+                      "rounds={}\n\n\n".format(wordsize, rounds))
+            stp_file.write(header)
+
+            # Setup variables
+            s = ["S{}".format(i) for i in range(rounds + 1)]
+            p = ["P{}".format(i) for i in range(rounds)]
+
+            # w = weight
+            w = ["w{}".format(i) for i in range(rounds)]
+
+            stpcommands.setupVariables(stp_file, s, wordsize)
+            stpcommands.setupVariables(stp_file, p, wordsize)
+            stpcommands.setupVariables(stp_file, w, wordsize)
+
+            stpcommands.setupWeightComputation(stp_file, weight, w, wordsize)
+
+            for i in range(rounds):
+                self.setupPresentRound(stp_file, s[i], p[i], s[i+1], 
+                                      w[i], wordsize)
+
+            # No all zero characteristic
+            stpcommands.assertNonZero(stp_file, s, wordsize)
+
+            # Iterative characteristics only
+            # Input difference = Output difference
+            if parameters["iterative"]:
+                stpcommands.assertVariableValue(stp_file, s[0], s[rounds])
+
+            for key, value in parameters["fixedVariables"].items():
+                stpcommands.assertVariableValue(stp_file, key, value)
+
+            for char in parameters["blockedCharacteristics"]:
+                stpcommands.blockCharacteristic(stp_file, char, wordsize)
+
+            stpcommands.setupQuery(stp_file)
+
+        return
+
+    def setupPresentRound(self, stp_file, s_in, p, s_out, w, wordsize):
+        """
+        Model for differential behaviour of one round PRESENT
+        """
+        command = ""
+
+        #Permutation Layer
+        for i in range(16):
+            command += "ASSERT({0}[{1}:{1}] = {2}[{3}:{3}]);\n".format(p, i*4+0, s_out, i)
+            command += "ASSERT({0}[{1}:{1}] = {2}[{3}:{3}]);\n".format(p, i*4+1, s_out, i+16)
+            command += "ASSERT({0}[{1}:{1}] = {2}[{3}:{3}]);\n".format(p, i*4+2, s_out, i+32)
+            command += "ASSERT({0}[{1}:{1}] = {2}[{3}:{3}]);\n".format(p, i*4+3, s_out, i+48)
+
+        # Substitution Layer
+        present_sbox = [0xc, 5, 6, 0xb, 9, 0, 0xa, 0xd, 3, 0xe, 0xf, 8, 4, 7, 1, 2]
+        for i in range(16):
+            variables = ["{0}[{1}:{1}]".format(s_in, 4*i + 3),
+                         "{0}[{1}:{1}]".format(s_in, 4*i + 2),
+                         "{0}[{1}:{1}]".format(s_in, 4*i + 1),
+                         "{0}[{1}:{1}]".format(s_in, 4*i + 0),
+                         "{0}[{1}:{1}]".format(p, 4*i + 3),
+                         "{0}[{1}:{1}]".format(p, 4*i + 2),
+                         "{0}[{1}:{1}]".format(p, 4*i + 1),
+                         "{0}[{1}:{1}]".format(p, 4*i + 0),
+                         "{0}[{1}:{1}]".format(w, 4*i + 3),
+                         "{0}[{1}:{1}]".format(w, 4*i + 2),
+                         "{0}[{1}:{1}]".format(w, 4*i + 1),
+                         "{0}[{1}:{1}]".format(w, 4*i + 0)]
+            # command += stpcommands.add4bitSbox(present_sbox, variables)
+            command += self.constraints_by_present_sbox(variables)
+
+
+        stp_file.write(command)
+        return

cryptosmt.py

@@ -8,7 +8,7 @@
 from ciphers import (simon, speck, simonlinear, keccak, keccakdiff,
                      siphash, simonrk, chaskeymachalf, simonkeyrc,
                      ketje, ascon, salsa, chacha, skinny, skinnyrk, gimli,
-                     present, craft, craftlinear, trifle, trifle, triflerk)
+                     present, craft, craftlinear, trifle, trifle, triflerk, presentla)
 from config import PATH_STP, PATH_CRYPTOMINISAT, PATH_BOOLECTOR
 
 from argparse import ArgumentParser, RawTextHelpFormatter
@@ -42,7 +42,8 @@ def startsearch(tool_parameters):
                     "craft" : craft.CraftCipher(),
                     "craftlinear" : craftlinear.CraftCipherLinear(),                   
                     "trifle" : trifle.TrifleCipher(),
-                    "triflerk" : triflerk.TrifleRK()}
+                    "triflerk" : triflerk.TrifleRK(),
+                    "presentla" : presentla.PresentLACipher()}
 
     cipher = None
 

docker/Dockerfile

@@ -1,38 +1,102 @@
+# Use Debian as the base image
 FROM debian:latest
 
-# Install all packages
-RUN apt-get update && apt-get install -y git build-essential cmake wget curl
+# Install all necessary system dependencies
+RUN apt-get update && apt-get install -y \
+    git build-essential cmake libgmp-dev \
+    zlib1g-dev python3 python3-dev libboost-all-dev \
+    bison flex python3-pip help2man \
+    perl curl libtinfo-dev && \
+    apt-get clean && rm -rf /var/lib/apt/lists/*
 
 WORKDIR /home/tools/
+
+# Clone and Build CaDiCaL
+WORKDIR /home/tools/cadical
+RUN git clone https://github.com/meelgroup/cadical . && \
+    git checkout mate-only-libraries-1.8.0 && \
+    ./configure && make && \
+    cp build/libcadical.* /usr/local/lib/ && \
+    mkdir -p /usr/local/include/cadical && \
+    cp -r src/* /usr/local/include/cadical/ && \
+    ldconfig
+
+# Clone and Build CaDiBack
+WORKDIR /home/tools/cadiback
+RUN git clone https://github.com/meelgroup/cadiback . && \
+    git checkout mate && \
+    ./configure && make && \
+    cp libcadiback.so /usr/local/lib/ && \
+    chmod +x /usr/local/lib/libcadiback.so && \
+    ldconfig
+
+# Clone and Build CryptoMiniSat
+WORKDIR /home/tools/cryptominisat
+RUN git clone https://github.com/msoos/cryptominisat . && \
+    mkdir build && cd build && \
+    cmake -DCMAKE_INSTALL_PREFIX=/usr/local \
+          -DCMAKE_LIBRARY_PATH=/usr/local/lib \
+          -DCMAKE_INCLUDE_PATH=/usr/local/include/cadical .. && \
+    make && make install && \
+    ldconfig
+
+# Ensure CryptoMiniSat shared libraries are correctly linked
+RUN echo "/usr/local/lib" > /etc/ld.so.conf.d/cryptominisat.conf && ldconfig
+
+# **Auto-detect CryptoMiniSat version and create symlink for STP**
+RUN latest_lib=$(ls /usr/local/lib/libcryptominisat5.so.* | sort -V | tail -n 1) && \
+    ln -sf "$latest_lib" /usr/local/lib/libcryptominisat5.so.5.11 && \
+    ldconfig
+
+# Clone Other Tools
+WORKDIR /home/tools
 RUN git clone https://github.com/agurfinkel/minisat && \
-    git clone https://github.com/msoos/cryptominisat && \
     git clone https://github.com/stp/stp && \
     git clone https://github.com/Boolector/boolector && \
     git clone https://github.com/kste/cryptosmt
 
+# Build Minisat
 WORKDIR /home/tools/minisat
-RUN apt-get install -y zlib1g-dev
-RUN make && make install
+RUN make && make install && \
+    find build -name "libminisat.*" -exec cp {} /usr/local/lib/ \; && \
+    ldconfig
 
-WORKDIR /home/tools/cryptominisat
-RUN apt-get install -y libm4ri-dev python3 python3-dev libboost-all-dev
-RUN mkdir build
-WORKDIR build
-RUN cmake ../ && make && make install
+# Build STP (Without Rebuilding)
+WORKDIR /home/tools/stp
+RUN git submodule update --init --recursive && \
+    ./scripts/deps/setup-gtest.sh && \
+    ./scripts/deps/setup-outputcheck.sh && \
+    ./scripts/deps/setup-cms.sh && \
+    ./scripts/deps/setup-minisat.sh && \
+    mkdir -p build && cd build && \
+    cmake .. -DCMAKE_INSTALL_PREFIX=/usr/local \
+        -DCMAKE_LIBRARY_PATH=/usr/local/lib \
+        -DCMAKE_INCLUDE_PATH=/usr/local/include/cadical \
+        -DCMAKE_CXX_FLAGS="-Wl,-rpath,/usr/local/lib" && \
+    make -j$(nproc) && make install && \
+    ldconfig
+
+# Ensure STP is in the PATH
+RUN ln -s /usr/local/bin/stp /usr/bin/stp || true
 
-WORKDIR /home/tools/stp/
-RUN apt-get install -y bison flex
-RUN mkdir build
-WORKDIR build
-RUN cmake ../ && make && make install
+# Fix STP Shared Library Issue (CryptoMiniSat Dependency)
+RUN echo "/usr/local/lib" > /etc/ld.so.conf.d/local-libs.conf && \
+    ldconfig
 
+# Set LD_LIBRARY_PATH to include /usr/local/lib
+ENV LD_LIBRARY_PATH="/usr/local/lib"
+
+# Build Boolector
 WORKDIR /home/tools/boolector
 RUN ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh
-RUN ./configure.sh --no-minisat --no-cms && cd build && make && make install
+RUN ./configure.sh && cd build && make && make install
 
+# Build CryptoSMT
 WORKDIR /home/tools/cryptosmt
-RUN apt-get install -y python3-pip
-RUN pip3 install pyyaml
+RUN python3 -m pip install --break-system-packages pyyaml
+
+# Ensure All Binaries are in PATH
+ENV PATH="/usr/local/bin:/home/tools/stp/build:/home/tools/minisat:$PATH"
 
-# Clean
-RUN apt-get clean && rm -rf /var/lib/apt/lists/*
+# Final Cleanup to Reduce Image Size
+RUN apt-get clean && rm -rf /var/lib/apt/lists/* /home/tools/*/.git

examples/present/present7rounds.yaml

@@ -6,6 +6,6 @@ rounds: 7
 wordsize: 64
 mode: 4
 fixedVariables:
-- S0: "0x0009000000000009"
-- S7: "0x0404040400000000"
+- S0: "0x000700000000000F"
+- S7: "0x0004040400040000"
 ...

examples/presentla/presentla7rounds.yaml

@@ -0,0 +1,11 @@
+# Example input file for PRESENT64 - 7 rounds to find all linear characteristics 
+---
+cipher: presentla
+sweight: 24
+rounds: 7
+wordsize: 64
+mode: 4
+fixedVariables:
+- S0: "0xCC00000000000000"
+- S7: "0x0080008000800080"
+...