Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up

An easy-to-use and open-source tool for differential, linear, differential-linear, and integral analysis of S-boxes

License

NotificationsYou must be signed in to change notification settings

hadipourh/sboxanalyzer

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

42 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

license

S-box Analyzer

S-box Analyzer is a tool for analyzing S-boxes and (vectorial) Boolean functions against differential, linear, differential-linear, boomerang, and integral attacks.

Particularly, it derives the minimized CP/MILP and SMT/SAT constraints to encode a set of binary vectors, (vectorial) Boolean functions, the Differential Distribution Table (DDT), Linear Approximation Table (LAT),Differential-Linear Connectivity Table (DLCT) andMonomial Prediction Table (MPT) of S-boxes.

logo

Dependencies

S-box Analyzer has been implemented as a SageMath module and employs ESPRESSO for logic minimization. Thus, it requires the following software:

Installation

  • ESPRESSO

    To build ESPRESSO, navigate into the espresso folder and run the following commands:

    cd espressomkdir build&&cd buildcmake ..make -j8

    To see more details about the ESPRESSO logic minimizer, seehere. The updated versions of ESPRESSO, compatible with new compilers, are availablehere andhere.

  • SageMath

    To see the installation recipe of SageMath, seehere.

Usage

Run the SageMath in the same directory as the S-box Analyzer. Next, importsboxanalyzer into the SageMath and then simply use it. The following example shows how to use the S-box Analyzer to encode the DDT ofGIFT's S-box:

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportGIFTassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.02secondsNumberofconstraints:49Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:3.0000p0+2.0000p1+1.4150p2sage:print(milp)['- a0 - a1 - a2 + a3 - b2 >= -3''a0 - a1 - a2 - a3 - b1 - b2 >= -4''a0 - a1 + a2 - b0 + b1 - b2 >= -2''a1 + a2 - b0 - b1 - b2 + b3 >= -2''a1 - a2 - a3 + b1 - b2 + b3 >= -2''a0 + a1 + a2 - b0 - b1 + b2 - b3 >= -2''a0 + a1 - a2 - a3 + b1 + b2 - b3 >= -2''- p0 - p1 >= -1''- p0 - p2 >= -1''- p1 - p2 >= -1''a1 - a3 + p0 >= 0''- b0 + b2 + p0 >= 0''- b0 + b3 + p0 >= 0''a2 + b1 - p2 >= 0''b0 + b2 + b3 - p0 >= 0''a0 - a3 + b0 + p0 >= 0''- a0 - a3 + b1 + p0 >= -1''a1 + a2 + b2 - p1 >= 0''- a0 + a3 + b0 + p1 >= 0''- a0 - a1 + a2 + a3 - b3 >= -2''a1 - a2 + a3 - b2 - b3 >= -2''a0 + a1 + b0 - b2 - b3 >= -1''- a1 - a3 + b0 - b2 - b3 >= -3''- a0 + b0 - b1 + b2 - b3 >= -2''a0 + b0 + b1 + b2 - b3 >= 0''a1 + a2 + a3 - b1 + b3 >= 0''a1 + b0 + b1 - b2 + b3 >= 0''a0 - a1 + a3 + b2 + b3 >= 0''a1 - a2 + a3 + b2 + b3 >= 0''- a0 + b0 + b1 + b2 + b3 >= 0''a0 - a1 - a2 - b1 + p0 >= -2''- a0 - a1 - b1 - b2 + p0 >= -3''a1 + a2 + a3 - b0 + p1 >= 0''a3 + b0 + b2 - b3 + p1 >= 0''- a1 + b0 - b1 + b3 + p1 >= -1''a3 + b0 - b2 + b3 + p1 >= 0''a0 - a1 - a2 - b0 - b1 - b3 >= -4''a0 - a1 + a2 - a3 + b1 - b3 >= -2''- a0 - a2 - a3 - b1 + b2 - b3 >= -4''- a0 + a2 - b0 + b1 + b2 - b3 >= -2''a0 - a1 - b0 - b2 - b3 + p1 >= -3''- a0 + a1 - b0 - b2 - b3 + p1 >= -3''- a0 - a1 - a3 + b2 + b3 + p1 >= -2''a0 + a2 + a3 - b1 - b2 + p2 >= -1''a0 + a2 + a3 - b2 + p0 + p2 >= 0''- a0 - a1 - a2 - a3 - b0 + b1 + b3 >= -4''- a0 - a1 + a2 - a3 - b1 - b2 + b3 >= -4''a0 - a1 - a2 + a3 + b1 - b3 + p2 >= -2']sage:print(cnf)(~a0|~a1|~a2|a3|~b2)& (a0|~a1|~a2|~a3|~b1|~b2)& (a0|~a1|a2|~b0|b1|~b2)& (a1|a2|~b0|~b1|~b2|b3)& (a1|~a2|~a3|b1|~b2|b3)& (a0|a1|a2|~b0|~b1|b2|~b3)& (a0|a1|~a2|~a3|b1|b2|~b3)& (~p0|~p1)& (~p0|~p2)& (~p1|~p2)& (a1|~a3|p0)& (~b0|b2|p0)& (~b0|b3|p0)& (a2|b1|~p2)& (b0|b2|b3|~p0)& (a0|~a3|b0|p0)& (~a0|~a3|b1|p0)& (a1|a2|b2|~p1)& (~a0|a3|b0|p1)& (~a0|~a1|a2|a3|~b3)& (a1|~a2|a3|~b2|~b3)& (a0|a1|b0|~b2|~b3)& (~a1|~a3|b0|~b2|~b3)& (~a0|b0|~b1|b2|~b3)& (a0|b0|b1|b2|~b3)& (a1|a2|a3|~b1|b3)& (a1|b0|b1|~b2|b3)& (a0|~a1|a3|b2|b3)& (a1|~a2|a3|b2|b3)& (~a0|b0|b1|b2|b3)& (a0|~a1|~a2|~b1|p0)& (~a0|~a1|~b1|~b2|p0)& (a1|a2|a3|~b0|p1)& (a3|b0|b2|~b3|p1)& (~a1|b0|~b1|b3|p1)& (a3|b0|~b2|b3|p1)& (a0|~a1|~a2|~b0|~b1|~b3)& (a0|~a1|a2|~a3|b1|~b3)& (~a0|~a2|~a3|~b1|b2|~b3)& (~a0|a2|~b0|b1|b2|~b3)& (a0|~a1|~b0|~b2|~b3|p1)& (~a0|a1|~b0|~b2|~b3|p1)& (~a0|~a1|~a3|b2|b3|p1)& (a0|a2|a3|~b1|~b2|p2)& (a0|a2|a3|~b2|p0|p2)& (~a0|~a1|~a2|~a3|~b0|b1|b3)& (~a0|~a1|a2|~a3|~b1|~b2|b3)& (a0|~a1|~a2|a3|b1|~b3|p2)

Interpretation of the outputs:

  • Input: a0||a1||a2||a3; a0: msb: The binary vector$a = a_{0}||a_{1}||a_{2}||a_{3}$ encodes the input difference where$a_{0}$ is the most significant bit of$a$.
  • Output: b0||b1||b2||b3; b0: msb: The binary vector$b = b_{0}||b_{1}||b_{2}||b_{3}$ encodes the output difference where$b_{0}$ is the most significant bit of$b$.
  • Weight: 3.0000 p0 + 2.0000 p1 + 1.4150 p2: The linear function$3 \cdot p_0 + 2 \cdot p_1 + 1.4150 \cdot p_2$ encodes the weight of differential transition$a \rightarrow b$, where$\Pr (a \rightarrow b) = 2^{-(3 \cdot p_0 + 2 \cdot p_1 + 1.4150 \cdot p_2)}$. The additional variables$p_{0}, p_{1}$, and$p_{2}$ are binary decision variables to encode the probability of differential transitions.

Convert a Set of Binary Vectors to CNF/MILP Constraints

Here, we show how to describe a set of binary vectors over$\mathbb{F}_{2}^{n}$ to (minimized) CNF/MILP constraints.

Assume that we have a set of binary vectors over$\mathbb{F}_{2}^{17}$ as follows:

S = {  (1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 1, 0),  (1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0),  (1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 0, 1, 0, 0),  (1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 1, 0),  (0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0),  (0, 1, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 1, 1, 0, 0),  (0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 1)}

We can use S-box Analyzer to encode$S$ to (minimized) CNF/MILP constraints.The following code shows how to do this:

sage:fromsboxanalyzerimportSboxAnalyzerasSAsage:S= [....:     (1,0,0,1,1,1,0,0,0,1,0,0,0,1,1,1,0),....:     (1,1,1,0,0,1,1,0,0,0,1,1,1,1,1,1,0),....:     (1,0,0,1,1,1,0,0,1,1,1,1,1,0,1,0,0),....:     (1,0,0,0,1,0,0,0,1,1,0,1,0,1,1,1,0),....:     (0,0,0,1,0,1,0,0,0,1,1,0,1,1,0,1,0),....:     (0,1,1,0,1,1,1,1,1,0,0,1,0,1,1,0,0),....:     (0,0,0,1,0,1,1,1,1,1,0,0,1,1,1,0,1)....: ]sage:cnf,milp=SA.encode_set_of_binary_vectors(S,mode=6)GenerateingandsimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.12secondsNumberofconstraints:27Variables:x0||x1||x2||x3||x4||x5||x6||x7||x8||x9||x10||x11||x12||x13||x14||x15||x16;msb:x0sage:pretty_print(milp)['- x1 - x3 >= -1','- x3 + x5 >= 0','x5 - x6 >= 0','x6 - x7 >= 0','- x2 - x9 >= -1','x1 + x9 >= 1','- x6 + x13 >= 0','- x11 + x14 >= 0','x12 + x14 >= 1','x13 - x15 >= 0','x8 + x15 >= 1','x3 - x16 >= 0','x7 - x16 >= 0','x14 - x16 >= 0','x3 + x4 - x7 >= 0','x3 + x6 + x8 >= 1','- x0 + x4 - x9 >= -1','x4 - x8 - x10 >= -1','- x4 - x8 + x11 >= -1','- x4 - x10 - x13 >= -2','x0 + x7 - x14 >= 0','- x6 + x11 - x15 >= -1','- x1 + x12 - x15 >= -1','- x0 + x3 + x15 >= 0','x10 - x12 + x16 >= 0','- x5 - x8 - x9 + x12 >= -2','x2 - x5 - x11 - x13 >= -2']sage:print(cnf)(~x1|~x3)& (~x3|x5)& (x5|~x6)& (x6|~x7)& (~x2|~x9)& (x1|x9)& (~x6|x13)& (~x11|x14)& (x12|x14)& (x13|~x15)& (x8|x15)& (x3|~x16)& (x7|~x16)& (x14|~x16)& (x3|x4|~x7)& (x3|x6|x8)& (~x0|x4|~x9)& (x4|~x8|~x10)& (~x4|~x8|x11)& (~x4|~x10|~x13)& (x0|x7|~x14)& (~x6|x11|~x15)& (~x1|x12|~x15)& (~x0|x3|x15)& (x10|~x12|x16)& (~x5|~x8|~x9|x12)& (x2|~x5|~x11|~x13)

Convert a Truth Table to CNF/MILP Constraints

Here, we show how to convert a truth table of a Boolean function to CNF/MILP constraints.Let's generate a random truth table of a Boolean function $f:\mathbb{F}{2}^{4} \rightarrow \mathbb{F}{2}$:

sage:BF= [randint(0,1)for_inrange(16)];BF[1,1,0,1,0,1,1,0,1,0,0,1,1,1,0,0]

We can use S-box Analyzer to encode the truth table of$f$ to (minimized) CNF/MILP constraints as follows:

sage:fromsboxanalyzerimportSboxAnalyzerasSAsage:cnf,milp=SA.encode_boolean_function(BF,mode=6)GenerateingandsimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.00secondsNumberofconstraints:5Variables:x0||x1||x2||x3;msb:x0sage:pretty_print(milp)['- x0 - x2 + x3 >= -1','x0 - x1 + x2 + x3 >= 0','- x0 + x1 + x2 - x3 >= -1','x1 - x2 + x3 >= 0','- x1 - x2 - x3 >= -2']sage:pretty_print(cnf)'(~x0 | ~x2 | x3) & (x0 | ~x1 | x2 | x3) & (~x0 | x1 | x2 | ~x3) & (x1 | ~x2 | x3) & (~x1 | ~x2 | ~x3)'

DDT Encoding

Encoding the DDT of SKINNY-64

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportSKINNY_4assbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.02secondsNumberofconstraints:39Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:3.0000p0+2.0000p1

To make a trade-off between the time of simplification and the solution's optimality, S-Box Analyzer supports seven different modes, i.e.,[mode=1,...,mode=7]. The default mode is 6, which is the best choice for both simplification time and optimality. For example, using the following command, we can minimize the number of constraints a little more:

sage:cnf,milp=sa.minimized_diff_constraints(mode=5)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.22secondsNumberofconstraints:37Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:3.0000p0+2.0000p1

Encoding the DDT of Ascon

sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.04secondsNumberofconstraints:77Input:a0||a1||a2||a3||a4;a0:msbOutput:b0||b1||b2||b3||b4;b0:msbWeight:4.0000p0+3.0000p1+2.0000p2

Encoding the DDT of PRESENT

sage:fromsage.crypto.sboxesimportPRESENTassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.03secondsNumberofconstraints:54Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:3.0000p0+2.0000p1

Encoding the DDT of SKINNY-128

To encode the DDT of large S-boxes (8-bit S-boxes), we usually divide the DDT into several sub-DDTs and encode the sub-DDTs seperately. Lastly, we put the constraints for all sub-DDTs together to encode the whole DDT. The following code shows how to encode the DDT of SKINNY-128.

Encode 2-DDT

sage:fromsage.crypto.sboxesimportSKINNY_8assbsage:sa=SboxAnalyzer(sb)sage:sa.get_differential_spectrum()                                                     [2,4,6,8,12,16,20,24,28,32,40,48,64]sage:cnf,milp=sa.minimized_diff_constraints(subtable=2,mode=2)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.50secondsNumberofconstraints:206Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msb

Encode 4-DDT

sage:cnf,milp=sa.minimized_diff_constraints(subtable=4)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.67secondsNumberofconstraints:279Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msb

Encode 6-DDT

sage:cnf,milp=sa.minimized_diff_constraints(subtable=6)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.03secondsNumberofconstraints:33Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msb

Encode 8-DDT

sage:cnf,milp=sa.minimized_diff_constraints(subtable=8)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.75secondsNumberofconstraints:235Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msb

You can encode other sub-DDTs of SKINNY-128's S-box in a similar way. Moreover, you may achieve a more optimal solution using the different modes such asmode=2 ormode=5. However, the simplification time might be higher. The default mode ismode=6 since it generates the nearly optimum result and is sufficient to get a remarkable speed up in automatic differential analysis based on MILP or SAT/SMT.

Encoding the DDT of AES

sage:fromsage.crypto.sboxesimportAESassbsage:sa=SboxAnalyzer(sb)sage:sa.get_differential_spectrum()                                                         [2,4]sage:cnf,milp=sa.minimized_diff_constraints(subtable=2)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:65.11secondsNumberofconstraints:7967Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msbsage:cnf,milp=sa.minimized_diff_constraints(subtable=4)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:869.08secondsNumberofconstraints:321Input:a0||a1||a2||a3||a4||a5||a6||a7;a0:msbOutput:b0||b1||b2||b3||b4||b5||b6||b7;b0:msb

As can be seen our results concerning encoding the DDT of AES's S-box is much better than the results reported inthis paper.

Encoding the *-DDT and *-LAT

In impossible differential attack (or zero correlation linear attacks) we only encode the possibility of the differential transitions (or a linear transitions), i.e., the *-DDT (or *-LAT). As illustrated in the following example, by setting thesubtable argument tostar we can simply encode the *-DDT.

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportMidori_Sb0assbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints(subtable="star",mode=5)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.01secondsNumberofconstraints:47Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msb

Encoding the DDT for CryptoSMT

By setting thecryptosmt_compatible argument toTrue, you can generate an SMT formula compatible with CryptoSMT. For example, to encode the DDT ofCRAFT in a format compatible with CryptoSMT, you can use the following commands:

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportCRAFTassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_diff_constraints(cryptosmt_compatible=True)SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.02secondsNumberofconstraints:54Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:p0+p1+p2sage:print(cnf)'(~a2 | p1) & (~b2 | p1) & (~p0 | p1) & (~p1 | p2) & (a1 | ~a2 | a3 | ~p0) & (a1 | ~a3 | b2 | p0) & (a2 | ~a3 | b2 | p0) & (~a1 | a3 | b2 | p0) & (a2 | b1 | ~b3 | p0) & (a2 | ~b1 | b3 | p0) & (~a0 | b2 | b3 | p0) & (a1 | a2 | a3 | ~b1 | ~b3) & (a0 | ~a2 | a3 | ~b2 | b3) & (~a1 | ~a2 | ~a3 | b2 | b3) & (~a1 | ~a3 | b0 | b1 | p0) & (a0 | a1 | ~b1 | ~b3 | p0) & (a1 | ~a3 | ~b1 | ~b3 | p0) & (~a1 | a3 | ~b1 | ~b3 | p0) & (~a0 | a3 | b1 | ~b3 | p0) & (~a1 | ~b0 | b1 | ~b3 | p0) & (a1 | ~a3 | ~b0 | b3 | p0) & (~a3 | ~b0 | ~b1 | b3 | p0) & (a0 | a1 | a2 | a3 | ~p2) & (b0 | b1 | b2 | b3 | ~p2) & (~a1 | ~a2 | ~b0 | b1 | b2 | ~b3) & (~a2 | a3 | b0 | ~b1 | b2 | ~p0) & (~a2 | ~a3 | b0 | b2 | ~b3 | ~p0) & (~a0 | a1 | ~a3 | ~b2 | b3 | ~p0) & (a0 | a3 | ~b0 | b1 | b3 | p0) & (a1 | a2 | a3 | b1 | b3 | ~p2) & (a0 | a3 | ~b0 | b1 | b2 | ~b3 | ~p0) & (~a0 | a1 | a2 | ~a3 | b0 | b3 | ~p0) & (a0 | a1 | ~b0 | ~b1 | b2 | b3 | ~p0) & (~a1 | ~a3 | b1 | b3 | ~p0 | ~p1 | ~p2) & (~a0 | ~a2 | b0 | ~b2 | p0 | ~p1 | ~p2) & (~a0 | ~a1 | a3 | ~b0 | b1 | ~b2 | ~p1 | ~p2) & (~a0 | a1 | ~a2 | ~b0 | ~b1 | b3 | ~p1 | ~p2) & (a0 | a2 | ~a3 | b1 | ~b2 | ~p0 | ~p1 | ~p2) & (a2 | b0 | ~b1 | ~b2 | ~b3 | ~p0 | ~p1 | ~p2) & (a0 | ~a1 | a2 | ~b2 | b3 | ~p0 | ~p1 | ~p2) & (a0 | ~a1 | ~a2 | ~a3 | ~b2 | p0 | ~p1 | ~p2) & (a0 | a1 | ~a2 | b1 | ~b2 | p0 | ~p1 | ~p2) & (~a0 | ~a1 | a2 | a3 | b0 | b1 | ~p0 | ~p1 | ~p2) & (~a2 | a3 | b1 | ~b2 | ~p0) & (a1 | ~a2 | ~b2 | b3 | ~p0) & (~a1 | ~a3 | ~b1 | ~b3 | ~p0) & (a2 | ~b0 | ~b1 | ~b3) & (~a0 | ~a3 | b0 | b1 | b2) & (a1 | ~a2 | b1 | ~b2 | ~p0) & (~a0 | ~a1 | b0 | b2 | b3) & (~a2 | a3 | ~b2 | b3 | ~p0) & (a0 | a1 | a2 | ~b0 | ~b3) & (a0 | a2 | a3 | ~b0 | ~b1) & (~a0 | ~a1 | ~a3 | b2)'

Deriving and Encoding Deterministic Differential Propagation

The following example shows how to derive and encode the deterministic differential propagation of the Ascon S-box.

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb)sage:ddp=sa.encode_deterministic_differential_behavior()sage:cp=sa.generate_cp_constraints(ddp)Input:a0||a1||a2||a3||a4;a0:msbOutput:b0||b1||b2||b3||b4;b0:msbsage:print(cp)if (a0==0/\a1==0/\a2==0/\a3==0/\a4==0)then (b0=0/\b1=0/\b2=0/\b3=0/\b4=0)elseif (a0==0/\a1==0/\a2==0/\a3==0/\a4==1)then (b0=-1/\b1=1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==0/\a3==1/\a4==0)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==0/\a1==0/\a2==0/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=0/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=1/\b3=1/\b4=0)elseif (a0==0/\a1==0/\a2==1/\a3==0/\a4==1)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==1/\a4==0)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==0/\a1==0/\a2==1/\a3==1/\a4==1)then (b0=0/\b1=-1/\b2=-1/\b3=1/\b4=-1)elseif (a0==0/\a1==0/\a2==-1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=0)elseif (a0==0/\a1==0/\a2==-1/\a3==1/\a4==0)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==0/\a1==1/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=1/\b3=1/\b4=-1)elseif (a0==0/\a1==1/\a2==0/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=1/\b4=-1)elseif (a0==0/\a1==1/\a2==1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=0/\b3=0/\b4=-1)elseif (a0==0/\a1==1/\a2==1/\a3==1/\a4==0)then (b0=-1/\b1=0/\b2=-1/\b3=-1/\b4=-1)elseif (a0==0/\a1==1/\a2==1/\a3==1/\a4==1)then (b0=-1/\b1=1/\b2=-1/\b3=0/\b4=-1)elseif (a0==1/\a1==0/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=1/\b2=0/\b3=-1/\b4=-1)elseif (a0==1/\a1==0/\a2==0/\a3==0/\a4==1)then (b0=1/\b1=0/\b2=-1/\b3=-1/\b4=1)elseif (a0==1/\a1==0/\a2==0/\a3==1/\a4==1)then (b0=0/\b1=-1/\b2=-1/\b3=-1/\b4=0)elseif (a0==1/\a1==0/\a2==1/\a3==0/\a4==0)then (b0=0/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==1/\a1==0/\a2==1/\a3==0/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==1/\a1==0/\a2==1/\a3==1/\a4==0)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==0/\a2==1/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=0)elseif (a0==1/\a1==0/\a2==-1/\a3==0/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==1/\a1==0/\a2==-1/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=0)elseif (a0==1/\a1==1/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==1/\a1==1/\a2==1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)elseif (a0==1/\a1==1/\a2==1/\a3==1/\a4==0)then (b0=-1/\b1=1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==1/\a2==1/\a3==1/\a4==1)then (b0=-1/\b1=0/\b2=-1/\b3=-1/\b4=-1)elseif (a0==-1/\a1==0/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)elseif (a0==-1/\a1==0/\a2==1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==-1/\a1==1/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==-1/\a1==1/\a2==1/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)else (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)endif

LAT Encoding

Here, we show how to encode the (squared) LAT of S-boxes.

Encoding the LAT of SKINNY-64

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportSKINNY_4assbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_linear_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.01secondsNumberofconstraints:29Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msbWeight:4.0000p0+2.0000p1

Note thatsa.minimized_linear_constraints() encode the squared LAT scaled by correlation.

Encoding the LAT of Ascon

sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_linear_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.04secondsNumberofconstraints:96Input:a0||a1||a2||a3||a4;a0:msbOutput:b0||b1||b2||b3||b4;b0:msbWeight:4.0000p0+2.0000p1

Deriving and Encoding Deterministic Linear Propagation

The following example shows how to derive and encode the deterministic linear propagation through the inverse of the Ascon S-box.

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb.inverse())sage:dlp=sa.encode_deterministic_linear_behavior()sage:cp=sa.generate_cp_constraints(dlp)Input:a0||a1||a2||a3||a4;a0:msbOutput:b0||b1||b2||b3||b4;b0:msbsage:print(cp)if (a0==0/\a1==0/\a2==0/\a3==0/\a4==0)then (b0=0/\b1=0/\b2=0/\b3=0/\b4=0)elseif (a0==0/\a1==0/\a2==0/\a3==0/\a4==1)then (b0=-1/\b1=-1/\b2=0/\b3=1/\b4=-1)elseif (a0==0/\a1==0/\a2==0/\a3==0/\a4==-1)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==0/\a3==1/\a4==0)then (b0=-1/\b1=1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==0/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==0/\a3==1/\a4==-1)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==0/\a4==0)then (b0=0/\b1=1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==0/\a4==1)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==0/\a4==-1)then (b0=-1/\b1=-1/\b2=1/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==1/\a4==0)then (b0=-1/\b1=0/\b2=0/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==1/\a4==1)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==1/\a3==1/\a4==-1)then (b0=-1/\b1=-1/\b2=0/\b3=-1/\b4=-1)elseif (a0==0/\a1==0/\a2==-1/\a3==0/\a4==0)then (b0=0/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==0/\a1==1/\a2==0/\a3==0/\a4==0)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=1)elseif (a0==0/\a1==1/\a2==1/\a3==0/\a4==0)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==0/\a1==1/\a2==-1/\a3==0/\a4==0)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==0/\a2==0/\a3==0/\a4==0)then (b0=-1/\b1=-1/\b2=-1/\b3=1/\b4=-1)elseif (a0==1/\a1==0/\a2==0/\a3==0/\a4==1)then (b0=1/\b1=-1/\b2=-1/\b3=0/\b4=1)elseif (a0==1/\a1==0/\a2==1/\a3==0/\a4==1)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==0/\a2==-1/\a3==0/\a4==1)then (b0=1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==1/\a2==0/\a3==0/\a4==1)then (b0=0/\b1=-1/\b2=-1/\b3=-1/\b4=0)elseif (a0==1/\a1==1/\a2==1/\a3==0/\a4==1)then (b0=0/\b1=-1/\b2=-1/\b3=-1/\b4=-1)elseif (a0==1/\a1==1/\a2==-1/\a3==0/\a4==1)then (b0=0/\b1=-1/\b2=-1/\b3=-1/\b4=-1)else (b0=-1/\b1=-1/\b2=-1/\b3=-1/\b4=-1)endif

MPT Encoding

Here, we show how to encode the propagation of monomial trails through S-boxes.

Encoding the MPT of PRESENT

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportPRESENTassbsage:sa=SboxAnalyzer(sb)sage:mpt=sa.monomial_prediction_table();mpt[[1,0,0,0,1,0,0,0,1,0,0,0,1,0,0,0], [0,1,0,0,0,1,0,0,1,0,0,0,1,0,0,0], [0,0,1,0,0,0,1,0,1,0,0,0,1,0,0,0], [0,0,0,1,1,1,1,0,0,1,1,1,1,0,0,0], [0,1,0,0,1,0,0,0,0,1,0,0,1,0,0,0], [0,0,0,0,0,1,0,0,0,1,0,0,1,0,0,0], [0,1,0,0,0,0,1,0,1,1,1,0,1,0,0,0], [0,0,1,1,0,0,1,0,1,1,0,1,0,1,0,0], [0,1,1,1,1,0,0,0,1,0,0,0,1,0,0,0], [0,0,0,1,1,1,1,0,0,0,1,0,0,0,1,0], [0,0,1,0,1,1,0,1,0,1,1,1,0,1,1,1], [0,0,1,1,1,0,1,1,1,0,1,0,1,1,0,1], [0,0,1,1,0,0,0,0,0,1,0,0,1,0,0,0], [0,0,1,0,1,0,0,1,1,1,1,0,0,0,1,0], [0,0,0,0,0,1,0,1,0,0,0,1,0,1,1,1], [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1]]sage:cnf,milp=sa.minimized_integral_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.00secondsNumberofconstraints:41Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msb

Encoding the MPT of Ascon

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_integral_constraints()SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.01secondsNumberofconstraints:97Input:a0||a1||a2||a3||a4;a0:msbOutput:b0||b1||b2||b3||b4;b0:msb

DLCT Encoding

Here, we show how to encode the DLCT of S-boxes.

Encoding the *-DLCT of KNOT

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportKNOTassbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_differential_linear_constraints(subtable='star')SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.00secondsNumberofconstraints:34Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msb

Encoding the *-DLCT of Midori

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportMidori_Sb0assbsage:sa=SboxAnalyzer(sb)sage:cnf,milp=sa.minimized_differential_linear_constraints(subtable='star')SimplifyingtheMILP/SATconstraints ...Timeusedtosimplifytheconstraints:0.00secondsNumberofconstraints:43Input:a0||a1||a2||a3;a0:msbOutput:b0||b1||b2||b3;b0:msb

Verification of Hadipour et al.'s Theorem

The following code verifies the Hadipour et al.'s theorem, (Proposition 2 in2024/255) for the S-box of Ascon.

sage:fromsboxanalyzerimport*sage:fromsage.crypto.sboxesimportAsconassbsage:sa=SboxAnalyzer(sb)sage:check=sa.check_hadipour_theorem();checkTheHadipouretal.'stheoremissatisfied.True

Citation

If you use our tools in a project resulting in an academic publication, please acknowledge it by citing our paper:

@article{DBLP:journals/tosc/HadipourNE22,  author    = {Hosein Hadipour and               Marcel Nageler and               Maria Eichlseder},  title     = {Throwing Boomerangs into Feistel Structures Application to CLEFIA,               WARP, LBlock, LBlock-s and {TWINE}},  journal   = {IACR Trans. Symmetric Cryptol.},  volume    = {2022},  number    = {3},  pages     = {271--302},  year      = {2022},  doi       = {10.46586/tosc.v2022.i3.271-302}}

Papers

Sbox Analyzer has been used in the following papers:

Road Map

Any contributions or comments regarding the development of the tool are warmly welcome.

License

S-box Analyszer is released under theMIT license.

About

An easy-to-use and open-source tool for differential, linear, differential-linear, and integral analysis of S-boxes

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

[8]ページ先頭
©2009-2025 Movatter.jp