Related-key Differential Cryptanalysis of Full-round PFP Ultra-lightweight Block Cipher
-
摘要: 2017年,PFP作为一种超轻量级分组密码被提出,而因其卓越的实现性能备受业界广泛关注。该算法不仅硬件开销需求低(仅需约
1355 GE(等效门))、功耗小,而且加解密速度快(其速度甚至比国际著名算法 PRESENT的实现速度快1.5倍),非常适合在物联网环境中使用。在PFP算法的设计文档中,作者声称该算法具有足够的能力抵御差分攻击、线性攻击及不可能差分攻击等多种密码攻击方法。然而该算法是否存在未知的安全漏洞是目前研究的难点。该文基于可满足性模理论(SMT),结合PFP算法轮函数特点,构建两种区分器自动化搜索模型。实验测试结果表明:该算法在32轮加密中存在概率为2–62的相关密钥差分特征。由此,该文提出一种针对全轮PFP算法的相关密钥恢复攻击,即只需263个选择明文和248次全轮加密便可破译出80 bit的主密钥。这说明该算法无法抵抗相关密钥差分攻击。Abstract:Objective In 2017, the PFP algorithm was introduced as an ultra-lightweight block cipher to address the demand for efficient cryptographic solutions in constrained environments, such as the Internet of Things (IoT). With a hardware footprint of approximately 1355 GE and low power consumption, PFP has attracted attention for its ability to deliver high-speed encryption with minimal resource usage. Its encryption and decryption speeds outperform those of the internationally recognized PRESENT cipher by a factor of 1.5, making it highly suitable for real-time applications in embedded systems. While the original design documentation asserts that PFP resists various traditional cryptographic attacks, including differential, linear, and impossible differential attacks, the possibility of undiscovered vulnerabilities remains unexplored. This study evaluates the algorithm’s resistance to related-key differential attacks, a critical cryptanalysis method for lightweight ciphers, to determine the actual security level of the PFP algorithm using formal cryptanalysis techniques.Methods To evaluate the security of the PFP algorithm, Satisfiability Modulo Theories (SMT) is used to model the cipher’s round function and automate the search for distinguishers indicating potential design weaknesses. SMT, a formal method increasingly applied in cryptanalysis, facilitates automated attack generation and the detection of cryptographic flaws. The methodology involved constructing mathematical models of the cipher’s rounds, which are tested for differential characteristics under various key assumptions. Two distinguisher models are developed: one based on single-key differentials and the other on related-key differentials, the latter being the focus of this analysis. These models automated the search for weak key differentials that could enable efficient key recovery attacks. The analysis leveraged the nonlinear substitution-permutation structure of the PFP round function to systematically identify vulnerabilities. The results are examined to estimate the probability of key recovery under different attack scenarios and assess the effectiveness of related-key differential cryptanalysis against the full-round PFP cipher. Results and Discussions The SMT-based analysis revealed a critical vulnerability in the PFP algorithm. A related-key differential characteristic with a probability of 2–62 is identified, persisting through 32 encryption rounds. This characteristic indicates a predictable pattern in the cipher’s behavior under related-key conditions, which can be exploited to recover the secret key. Such differentials are particularly concerning as they expose a significant weakness in the cipher’s resistance to related-key attacks, a critical threat in IoT applications where keys may be reused or related across multiple devices or sessions.Based on this finding, a key recovery attack is developed, requiring only 263 chosen plaintexts and 248 full-round encryptions to retrieve the 80-bit master key. The efficiency of this attack demonstrates the vulnerability of the PFP cipher to practical cryptanalysis, even with limited computational resources. The attack’s relatively low complexity suggests that PFP may be unsuitable for applications demanding high security, particularly in environments where adversaries can exploit related-key differential characteristics. Moreover, these results indicate that the existing resistance claims for the PFP cipher are insufficient, as they do not account for the effectiveness of related-key differential cryptanalysis. This challenges the assertion that the PFP algorithm is secure against all known cryptographic attacks, emphasizing the need for thorough cryptanalysis before lightweight ciphers are deployed in real-world scenarios.( Fig. 2 : Related-key differential characteristic with probability 2–62 in 32 rounds;Table 1 : Attack complexity and resource requirements for related-key recovery.)Conclusions In conclusion, this paper presents a cryptographic analysis of the PFP lightweight block cipher, revealing its vulnerability to related-key differential attacks. The proposed key recovery attack demonstrates that, despite its efficiency in hardware and speed, PFP fails to resist attacks exploiting related-key differential characteristics. This weakness is particularly concerning for IoT applications, where key reuse or related keys across devices is common. These findings highlight the need for further refinement in lightweight cipher design to ensure robust resistance against advanced cryptanalysis techniques. As lightweight ciphers continue to be deployed in security-critical systems, it is essential that designers consider all potential attack vectors, including related-key differentials, to strengthen security guarantees. Future work should focus on enhancing the cipher’s security by exploring alternative key-schedule designs or increasing the number of rounds to mitigate the identified vulnerabilities. Additionally, this study emphasizes the effectiveness of SMT-based formal methods in cryptographic analysis, providing a systematic approach for identifying previously overlooked weaknesses in cipher designs. -
1. 引言
随着电子信息技术的飞速发展,物联网(Internet of Things, IoT)设备在日常生活中的需求持续上升。这些设备之间的信息交换常常依赖于嵌入式加密算法,以确保数据传输的安全性、设备的认证以及其它敏感性服务的可靠性。绝大多数物联网设备,尤其是传感器和微控制器,都处于存储空间小、计算性能弱、功耗低等资源受限的环境。传统的加密算法(如高级加密标准(Advanced Encryption Standard, AES)[1])因其健壮的设计原则通常具有较高的实现成本并不适用于资源受限环境下的应用。而轻量级分组密码通常具有低硬件实施成本和低能耗的特点,同时能在敏感应用中提供充足的安全保障非常适合资源环境受限的物联网设备,成为近年研究的热点,目前已经有许多轻量级分组密码算法(如LBlock[2], LED[3], GIFT[4], SIMON, SPECK[5], PRESENT[6], PFP[7])相继被提出,它们的安全性分析对于轻量级密码的应用和新算法设计具有重要价值。
差分分析[8]和线性分析[9]作为评估分组密码安全性的两种经典技术被广泛关注,并在此基础上衍生出了不可能差分分析[10]、零相关线性分析[11]、高阶差分分析[12]、截断差分分析[13]、相关密钥差分分析[14]等。相关密钥差分分析由Biham于1994年提出,其主要思想是利用密钥之间的差分在算法内部的扩散关系构建相关密钥差分区分器,并由区分器恢复密钥。这对分组密码算法中密钥编排提出了全新的要求。此外,目前比较流行的一种方式是通过结合自动化分析构建密码算法的差分或线性区分器,比如基于混合整数线性规划(Mixed Integer Linear Programming, MILP)[15]、约束规划(Constraint Programming, CP)[16]、布尔可满足性问题(Boolean SATisfiability problem, SAT)[17]、可满足性模理论(Satisfiability Modulo Theories, SMT)[18]的一些自动化分析方法。
PFP作为一种超轻量级分组密码,自2017年被推出以来因其显著的实现性能优势而备受关注[7]。该算法分组长度为64 bit,密钥长度为80 bit,迭代轮数为34轮。近年来,多位研究者对PFP算法的安全性进行了探讨:2017年,黄玉划等人[7]给出了1~20轮的最小差分和线性活跃S盒的个数,并使用中间相错技术成功构造了一个5轮的不可能差分区分器,使用该区分器对6轮PFP算法进行分析,成功恢复了32 bit的主密钥。随后在2020年,沈璇等人[19]通过研究S盒的差分传播特性,构造出了7轮不可能差分区分器,并由此发起了9轮的密钥恢复攻击,恢复了36 bit主密钥。2023年,赵光耀等人[20]通过研究S盒中的差分分布特性并结合置换操作的特点构造了一组共16条7轮的不可能差分区分器,再次对9轮PFP算法进行分析,恢复了40 bit的主密钥;并提出针对10轮PFP算法的密钥恢复攻击。此外,刘道瞳等人[21]基于MILP技术,构建了PFP算法的积分区分器搜索模型,使用该模型搜索到了PFP算法11轮的积分区分器;并选用搜索到的10轮积分区分器对12轮PFP算法进行了密钥恢复攻击。李艳俊等人[22]也基于MILP技术,搜索到了概率为2–11的4轮迭代差分特征,构造了概率为2–59的22轮差分区分器,通过在区分器前后各增加2轮,采用早期淘汰技术对PFP算法进行了26轮的密钥恢复攻击,所需的数据复杂度为260个明文,时间复杂度为254.3次26轮加密。
本文基于SMT自动化分析的技术,结合PFP算法轮函数特点,分别构造了两种搜索模型:即(1)单密钥(相关密钥)下比特级的最小差分活跃S盒自动化搜索模型,(2)单密钥(相关密钥)下比特级的最大期望差分特征概率差分区分器自动化搜索模型。通过构造的自动化搜索模型,我们的测试首次捕获了PFP密码算法在单密钥和相关密钥条件下的1~34轮(全轮)的最大期望差分特征概率的紧界。由此,本文通过将搜索到的差分特征概率为2–61的25轮差分区分器向前、后各扩展2轮,对PFP算法进行了29轮的差分分析。将搜索到的相关密钥差分特征概率为2–62的32轮相关密钥差分区分器向后扩展2轮,对PFP算法进行了34轮(全轮)的相关密钥差分分析(本文与已有的攻击结果对比见表1)。研究结果表明本密码算法无法抵抗相关密钥差分攻击。
2. 基础知识
2.1 PFP算法简介[7]
轻量级分组密码PFP算法使用经典的2分支Feistel结构,分组长度为64 bit,密钥长度为80 bit,迭代轮数为34轮,借鉴了PRESENT算法,并修改了扩散层的P置换,其轮函数F由轮密钥加、非线性层(S盒替换)、线性层(P置换)组成,非线性层并行使用了8个相同的4 bitS盒,所使用的4 bitS盒与PRESENT中的相同,线性层为32 bit的拉线变换P置换,该算法的加密过程如图1所示。
其中${L_i}$和${R_i}$分别为第$i$轮输入的左、右分支32 bit,${K_i}$为第$i$轮加密的轮密钥,F为轮函数,⊕表示逐比特异或运算,第$i$轮的加密可由式(1)表示
Li+1=RiRi+1=Li⊕F(Ki,Ri)} (1) 密钥编排:80 bit的主密钥存储在密钥寄存器$ K=({k}_{79}{k}_{78}\cdots {k}_{0}) $中。第$i$轮的32 bit轮密钥${K_i}$由寄存器当前最左边32 bit产生,即${K_i} = (k_{31}^ik_{30}^i \cdots k_0^i) = ({k_{79}}{k_{78}} \cdots {k_{48}})$。密钥更新步骤如下:
(1) ${\text{ }}[{k_{79}}{k_{78}} \cdots {k_0}] = [{k_{18}}{k_{17}} \cdots {k_{20}}{k_{19}}]$(右旋转19位);
(2) ${\text{ }}[{k_{79}}{k_{78}}{k_{77}}{k_{76}}] = S[{k_{79}}{k_{78}}{k_{77}}{k_{76}}]$;
(3) ${\text{ }}[{k_{19}}{k_{18}}{k_{17}}{k_{16}}] = [{k_{19}}{k_{18}}{k_{17}}{k_{16}}] \oplus {r_{\mathrm{c}}}$。
其中${r_{\mathrm{c}}}$为轮常数,即$0 \le {r_{\mathrm{c}}} \le 33$;$S[k]$为S盒替换。
轮密钥加:第$i$轮右分支的32 bit输入${R_i}$和32 bit的轮密钥${K_i}$进行异或即:${R_i} = {R_i} \oplus {K_i}$。
S盒:PFP算法的非线性层并行使用8个相同的4 bitS盒,如表2所示。
表 2 PFP算法的S盒x 0 1 2 3 4 5 6 7 8 9 A B C D E F S[x] C 5 6 B 9 0 A D 3 E F 8 4 7 1 2 S盒的差分分布表(Difference Distribution Table, DDT)如表3所示。
表 3 S盒的差分分布表输入差分 输出差分 0 1 2 3 4 5 6 7 8 9 A B C D E F 0 16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 4 0 0 0 4 0 4 0 0 0 4 0 0 2 0 0 0 2 0 4 2 0 0 0 2 0 2 2 2 0 3 0 2 0 2 2 0 4 2 0 0 2 2 0 0 0 0 4 0 0 0 0 0 4 2 2 0 2 2 0 2 0 2 0 5 0 2 0 0 2 0 0 0 0 2 2 2 4 2 0 0 6 0 0 2 0 0 0 2 0 2 0 0 4 2 0 0 4 7 0 4 2 0 0 0 2 0 2 0 0 0 2 0 0 4 8 0 0 0 2 0 0 0 2 0 2 0 4 0 2 0 4 9 0 0 2 0 4 0 2 0 2 0 0 0 2 0 4 0 A 0 0 2 2 0 4 0 0 2 0 2 0 0 2 2 0 B 0 2 0 0 2 0 0 0 4 2 2 2 0 2 0 0 C 0 0 2 0 0 4 0 2 2 2 2 0 0 0 2 0 D 0 2 4 2 2 0 0 2 0 0 2 2 0 0 0 0 E 0 0 2 2 0 0 2 2 2 2 0 0 2 2 0 0 F 0 4 0 0 4 0 0 0 0 0 0 0 0 0 4 4 P置换:该操作将32 bit数据按照比特排列置换,将数据从第$i$位移动到$P(i)$位。置换规则为
P(i)={31, i=31i⋅8 mod 31, 0≤i≤30 (2) 3. 自动化分析模型
SAT指的是命题逻辑公式的判定可满足性问题,也是第1个被证明的非确定性多项式完全问题(Non-deterministic Polynomial Complete, NPC)[23]问题,但SAT在表达能力上存在很大的局限性,对许多特定领域的问题无法直接表达,因此通过将SAT中命题逻辑公式的可满足性问题扩展到谓词逻辑上提出了具有更强表达能力的SMT。常见的求解SMT问题的求解器有Z3[24], CVC4[25], MathSAT5[26], Boolector[27]和STP[28]等。本文使用STP求解器进行SMT模型的求解,并使用协同有效性校验器(Cooperative Validity Checker, CVC)[29]语言进行模型描述。
3.1 差分分析SMT模型
差分分析模型1 异或操作(XOR):对于$n$ bit的异或操作,假设$\alpha $和$\beta $表示输入差分,$\gamma $表示输出差分即$\gamma = \alpha \oplus \beta $。则模型约束为
α,β,γ:BITVECTOR(n)ASSERT(γ=BVXOR(α,β))} (3) 注意在单密钥下由于密钥对差分传播无影响,因此差分分析模型中不需要考虑异或密钥操作,但在相关密钥条件下需要考虑异或密钥操作对于相关密钥差分分析模型的影响。
差分分析模型2 分支操作(Branch):对于$n$ bit的分支操作,假设$\alpha $表示输入差分,$\beta $和$\gamma $表示输出差分,即$\gamma = \alpha = \beta $。则模型约束为
α,β,γ:BITVECTOR(n)ASSERT( (γ = β) AND (β = α) )} (4) 差分分析模型3 P置换操作(Permutation):对于$n$ bit的置换操作,假设$\alpha $表示输入差分,$\beta $表示输出差分,$P$和${P^{ - 1}}$为P置换操作的置换和逆置换函数,即$\alpha [i] = \beta [P(i)]$, $ \beta [i] = \alpha [{P^{ - 1}}(i)] $, $i = 0, 1,\cdots,n$。则模型约束为
α,β:BITVECTOR(n)ASSERT(β[i:i]=α[P−1(i):P−1(i)])} (5) 注意在差分模型2和差分模型3中的多个变量取值相等的约束在实际进行建模时可以不添加,只需取其中一个变量在整个模型中对其它相等的变量进行相应的替换即可,这样可以减少变量的个数,加快求解时间。
差分分析模型4 S盒替换操作(Substitute):对于$n$ bit的S盒替换操作,由S盒的DDT可知S盒所有可能的输入(行)和输出(列)差分,假设${\alpha _i}$表示输入差分$\alpha $可能的取值,$\beta _i^j$表示输入差分${\alpha _i}$经过S盒替换后的输出差分$\beta $可能的取值,$ {\text{dp}}_i^j $表示S盒输入输出差分$({\alpha _i},\beta _i^j)$的差分传播概率,其中$i = 0, 1,\cdots,m$; $j = 0,1,\cdots,\varphi (i) - 1$;$\varphi (i)$表示差分分布表中第$i$行取值不为0的列的总数,即$S({\alpha _i}) = \beta _i^j$,则S盒差分传播的模型约束为
α,β:BITVECTOR(n)ASSERT(IF α=αi THEN (β=βφ(i)−1iOR β=βφ(i)−2i OR ⋯ OR β=β0i)ELSE NOT(α=αi) ENDIF)} (6) 当S盒输入差分$\alpha \ne {\{ 0\} ^n}$时称该S盒为差分活跃S盒,对于差分活跃S盒的模型约束需要引入一个辅助比特变量$a$,当$a = 1$时表示该S盒活跃,差分活跃S盒模型约束为
α,β:BITVECTOR(n)a:BITVECTOR(1)ASSERT(IF NOT(α=0bin0⋯0) THEN a = 0bin1 ELSE a=0bin0 ENDIF)} (7) 假设$b_i^j$为$ - \log _2^{{\text{dp}}_i^j}$的$l$位编码二进制表示,对于S盒的差分传播概率模型约束需要引入一个辅助变量$p$来表示该S盒差分传播概率的负对指数,则S盒差分传播概率模型约束为
α,β:BITVECTOR(n)p:BITVECTOR(l)ASSERT(IF α = αi AND β=βji THEN p=0binbji ELSE NOT(α = αi) ENDIF)} (8) 差分分析模型5 额外约束:对于分组长度位$2n$ bit,初始轮密钥长度为$k$比特的分组密码,在单密钥下需要保证初始输出差分${X_0} \ne {\{ 0\} ^{2n}}$,模型约束为
X0:BITVECTOR(n)ASSERT(NOT(X0=0bin0⋯0))} (9) 若在相关密钥下则需要保证输入差分${X_0}$和初始轮密钥差分${K_0}$不能同时为0,即${X_0}|{K_0} \ne {\{ 0\} ^{2n + k}}$,模型约束为
X0:BITVECTOR(n)K0:BITVECTOR(k)ASSERT(NOT(X0@K0=0bin0⋯0))} (10) 差分分析模型6 目标约束:若$r$轮密码算法共有${s_r}$个S盒(相关密钥下也包括密钥编排部分使用的S盒)记第$i$个S盒的差分活跃S盒辅助比特变量为${a_i}$,第$i$个差分传播概率$l$ bit辅助变量为${p_i}$,$i = 0, 1,\cdots,({s_r} - 1)$,引入$n$比特辅助变量${\text{tota}}{{\text{l}}_{{\text{acs}}}}$和${\text{tota}}{{\text{l}}_{{\text{pro}}}}$分别表示总的目标活跃S盒个数和总的目标差分特征概率。则差分活跃S盒的目标约束模型为
ai:BITVECTOR(1)totalacs:BITVECTOR(n)ASSERT(totalacs=BVPLUS(n,0bin0⋯0@a0,0bin0⋯0@a1,⋯,0bin0⋯0@asr−1))} (11) 差分特征概率的目标约束模型为
pi:BITVECTOR(l)totalpro:BITVECTOR(n)ASSERT( totalpro=BVPLUS(n,0bin0⋯0@p0,0bin0⋯0@p1,⋯,0bin0⋯0@psr−1) )} (12) 注意在本文针对PFP算法的安全性分析问题中我们提出的基于SMT的自动化分析模型比基于MILP的自动化分析技术搜索速度更快,具体来说在实验PC平台(Intel(R) Xeon(R) Silver 4210 CPU @ 2.2 GHz 32 GB)上进行实验测试,使用基于MILP的自动化分析技术近对15轮的PFP算法进行分析测试,在1周内无法返回最优解,而使用本文方法仅需约1.7天即可给出全轮PFP的最优搜索结果。接下来我们将使用上述自动化分析模型对PFP算法展开详细的差分分析。
4. 自动化分析结果
4.1 最优差分区分器搜索结果
为了得到PFP算法更精确的抵抗差分分析的安全界,使用上一节提出的自动化分析模型,本文首次获得了PFP算法1~34轮(全轮)在单密钥下的最大期望差分特征概率(差分界)及在相关密钥下的最大期望差分特征概率(差分界),由于自动化分析模型是比特级的,同时能获得对应的比特级的差分特征即区分器。搜索结果如表4所示。
表 4 PFP算法的差分界轮数 最大期望差分特征概率 轮数 最大期望差分特征概率 单密钥 相关密钥 单密钥 相关密钥 1 20 20 18 2–44 2–34 2 2–2 20 19 2–46 2–36 3 2–4 20 20 2–48 2–38 4 2–6 20 21 2–51 2–40 5 2–8 20 22 2–54 2–42 6 2–12 2–3 23 2–56 2–44 7 2–16 2–5 24 2–58 2–46 8 2–18 2–9 25 2–61 2–48 9 2–21 2–14 26 2–64 2–50 10 2–24 2–18 27 2–66 2–52 11 2–26 2–20 28 2–68 2–54 12 2–28 2–22 29 2–71 2–56 13 2–31 2–24 30 2–74 2–58 14 2–34 2–26 31 2–76 2–60 15 2–36 2–28 32 2–78 2–62 16 2–38 2–30 33 2–81 2–64 17 2–41 2–32 34 2–84 2–66 表4显示在单密钥下PFP算法25轮的最大期望差分特征概率为2–61,且26~34轮的最大期望差分特征概率均$ \le $2–64,如果攻击者向前后各扩展2轮则最多对29轮的PFP发起差分攻击,存在5轮的安全冗余,而在相关密钥下PFP算法32轮的最大期望差分特征概率为2–62且33~34轮的最大期望差分特征概率均$ \le $2–64如果攻击者向前后各扩展2轮则可对36轮的PFP算法发起相关密钥差分攻击(PFP算法全轮只有34轮),因此PFP算法不能抵抗相关密钥差分分析。
在本文搜索到的区分器中,24轮、25轮的差分区分器的最大期望差分特征概率为2–58, 2–61,比现有分析结果李艳俊等人[22]的差分特征概率为2–59的22轮差分区分器,概率更高、轮数更长。31轮、32轮的相关密钥差分区分器的最大期望差分特征概率为2–60, 2–62为目前已知PFP算法最长轮数区分器。下面给出搜索到的区分器的部分结果,如表5、表6所示,其中表5中1~5轮为4轮迭代差分特征,表6中0~2轮为2轮迭代相关密钥差分特征。
表 5 差分特征概率为2–61的25轮差分区分器轮数 左分支差分 右分支差分 轮数 左分支差分 右分支差分 0 0x00040D00 0x00000900 13 0x00000900 0x00000900 1 0x00000900 0x00000900 14 0x00000900 0x00000D00 2 0x00000900 0x00000D00 15 0x00000D00 0x00000D00 3 0x00000D00 0x00000D00 16 0x00000D00 0x00000900 4 0x00000D00 0x00000900 17 0x00000900 0x00000900 5 0x00000900 0x00000900 18 0x00000900 0x00000D00 6 0x00000900 0x00000D00 19 0x00000D00 0x00000D00 7 0x00000D00 0x00000D00 20 0x00000D00 0x00000900 8 0x00000D00 0x00000900 21 0x00000900 0x00000900 9 0x00000900 0x00000900 22 0x00000900 0x00000D00 10 0x00000900 0x00000D00 23 0x00000D00 0x00000D00 11 0x00000D00 0x00000D00 24 0x00000D00 0x00000900 12 0x00000D00 0x00000900 25 0x00000900 0x00040D00 表 6 差分特征概率为2–62的32轮相关密钥差分区分器轮数 左右分支差分 相关密钥差分 轮数 左右分支差分 相关密钥差分 0 0x8BBBBA22D1111177 0xD111117777444445DDDD 17 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 1 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 18 0x8BBBBA22D1111177 0xD111117777444445DDDD 2 0x8BBBBA22D1111177 0xD111117777444445DDDD 19 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 3 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 20 0x8BBBBA22D1111177 0xD111117777444445DDDD 4 0x8BBBBA22D1111177 0xD111117777444445DDDD 21 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 5 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 22 0x8BBBBA22D1111177 0xD111117777444445DDDD 6 0x8BBBBA22D1111177 0xD111117777444445DDDD 23 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 7 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 24 0x8BBBBA22D1111177 0xD111117777444445DDDD 8 0x8BBBBA22D1111177 0xD111117777444445DDDD 25 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 9 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 26 0x8BBBBA22D1111177 0xD111117777444445DDDD 10 0x8BBBBA22D1111177 0xD111117777444445DDDD 27 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 11 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 28 0x8BBBBA22D1111177 0xD111117777444445DDDD 12 0x8BBBBA22D1111177 0xD111117777444445DDDD 29 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 13 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 30 0x8BBBBA22D1111177 0xD111117777444445DDDD 14 0x8BBBBA22D1111177 0xD111117777444445DDDD 31 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 15 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 32 0x8BBBBA22D1111177 - 16 0x8BBBBA22D1111177 0xD111117777444445DDDD 4.2 对PFP算法的密钥恢复攻击
在单密钥下可以通过将表5中的25轮差分区分器向前后各扩展2轮对PFP进行29轮的差分分析,根据文献[30]中的差分分析密钥恢复攻击成功概率计算公式,当取攻击优势为1时,仅使用约259个选择明文,278.14次29轮加密即可恢复73比特主密钥,攻击成功概率为63.06%。
而在相关密钥下,通过将表6中的32轮相关密钥差分区分器向后扩展2轮可以对PFP进行34轮(全轮)的相关密钥差分分析。如图2所示,图中“?”表示不确定的差分值0和1,“♥♣♦♤♡♢♧”表示确定的差分值0和1,“♥”表示对“♥”的差分值取反,接下来我们主要介绍对PFP算法进行相关密钥差分分析的全轮密钥恢复过程。
4.3 全轮PFP算法密钥恢复攻击
根据图2对全轮PFP算法进行相关密钥差分分析恢复密钥,与单密钥下差分分析过程类似,不同的是在相关密钥条件下,假设攻击者可以在不获取正确密钥具体值的情况下知道一对正确密钥之间的差分值,具体过程如下:
首先注意到$\Delta {K_{32}}[31,\,30,\,29,\,28] = $♥♣♦1, $\Delta {K_{33}}[31,\,30,\,29,\,28] = $♤♡♢♧,根据密钥编排可知,$\Delta {K_{32}}[31,\,30,\,29,\,28]$和$\Delta {K_{33}}[31,\,30,\,29,\,28]$分别与第31轮和第32轮的80 bit密钥状态寄存器中第18~15位的4 bit密钥差分值0001和1011经过S盒替换后的差分值相同。S盒的DDT显示S盒输入差分为0001和1011时输出差分对应有4和7种可能的取值,即♥♣♦1∈{0011,0111,1001,1101},♤♡♢♧∈{0001,0100,1000,1001,1010,1011,1101},♥♣♦♤♡♢♧总的可能的取值有28种,只需对每种取值使用1次本文的攻击即可,因此每次攻击总是假设♥♣♦♤♡♢♧的取值是确定的。
数据收集阶段 选择${2^m}$个明文,大约有${2^{m - 1}}$个明文对符合第0轮的输入差分,由区分器的概率可知明文对中共有${2^{m - 1 - 62}} = {2^{m - 63}}$个正确对。根据$\Delta {L_{34}}|\Delta {R_{34}}$可知在密文随机分布的条件下${2^{m - 1}}$个明文对加密34轮大约有${2^{m - 1 - 32}} = {2^{m - 33}}$个密文对满足最后一轮的输出差分。对于输入差分满足图2中$\Delta {L_0}|\Delta {R_0}$和$\Delta {L_{34}}|\Delta {R_{34}}$的明密文对,在随机密钥的解密下,满足区分器的输出差分$\Delta {L_{32}}|\Delta {R_{32}}$的概率为${2^{ - 4 - 3 - 4 - 3 - 4 - 3 - 4 - 3 - 4}} = {2^{ - 32}}$,因此随机密钥的平均得票数为${2^{m - 33 - 32}} = {2^{m - 65}}$,信噪比为${S_N} = {2^2}$。
密钥恢复阶段
步骤1 猜测第33轮的28 bit密钥${K_{33}}[31{\text{~}}4]$,采用早期淘汰技术,每次只猜测其中的4 bit密钥,剩下的24 bit密钥分6步猜测,筛选后剩下的明密文对数量为${2^{m - 33 - 4 - 3 - 4 - 3 - 4 - 3 - 4 - 3}} = {2^{m - 61}}$。
步骤2 猜测第32轮的4 bit密钥${K_{32}}[21{\text{~}}28]$,注意由密钥编排可知${K_{32}}[21{\text{~}}28] = {K_{33}}[12{\text{~}}9]$,因此这一步不需要猜测密钥,筛选后剩下的明密文对数量为${2^{m - 61 - 4}} = {2^{m - 65}}$。
密钥恢复阶段具体的复杂度计算见表7。
表 7 相关密钥下PFP算法密钥恢复阶段的复杂度计算步数 猜测密钥 筛选后剩余明密文对数量 时间复杂度 1 ${K_{33}}[31,30,29,28]$ ${2^{m - 33 - 4}}$ $ 2 \cdot {2^{m - 33}} \cdot {2^4} $ 2 ${K_{33}}[23,22,21,20]$ ${2^{m - 37 - 4}}$ $ 2 \cdot {2^{m - 37}} \cdot {2^8} $ 3 ${K_{33}}[15,14,13,12]$ ${2^{m - 41 - 4}}$ $ 2 \cdot {2^{m - 41}} \cdot {2^{12}} $ 4 ${K_{33}}[7,6,5,4]$ ${2^{m - 45 - 4}}$ $ 2 \cdot {2^{m - 45}} \cdot {2^{16}} $ 5 ${K_{33}}[27,26,25,24]$ ${2^{m - 49 - 3}}$ $ 2 \cdot {2^{m - 49}} \cdot {2^{20}} $ 6 ${K_{33}}[19,18,17,16]$ ${2^{m - 52 - 3}}$ $ 2 \cdot {2^{m - 52}} \cdot {2^{24}} $ 7 ${K_{33}}[11,10,9,8]$ ${2^{m - 55 - 3}}$ $ 2 \cdot {2^{m - 55}} \cdot {2^{28}} $ 8 ${K_{33}}[3,2,1,0]$ ${2^{m - 58 - 3}}$ $ 2 \cdot {2^{m - 58}} \cdot {2^{32}} $ 9 ${K_{32}}[31,30,29,28]$ ${2^{m - 61 - 4}}$ $ 2 \cdot {2^{m - 61}} \cdot {2^{32}} $ 总和 ${2^{m - 24}} + {2^{m - 26}}$ 复杂度分析:由于经过区分器筛选后剩下的正确对的个数为${2^{m - 63}}$,本文取$m = 63$,对于正确密钥而言平均有一个明密文对留下来,所以数据复杂度为${2^{63}}$个选择明文。时间复杂度方面,由表7知1次攻击恢复32 bit主密钥的时间复杂度为$({2^{63 - 24}} + {2^{63 - 26}})/(34 \times 8) = {2^{31.23}}$次全轮加密,穷举剩余48 bit主密钥需要的时间复杂度为${2^{48}}$次全轮加密,数据复杂度为1个选择明文,所以恢复所有80 bit主密钥的总时间复杂度为${2^{36.03}} + {2^{48}} \approx {2^{48}}$次全轮加密,数据复杂度为${2^{63}} + 1 \approx {2^{63}}$个选择明文。
5. 结论
本文基于SMT的自动化分析技术对轻量级分组密码PFP抵抗差分分析的安全性进一步的评估,给出了全轮最优差分特征概率的精确下界,同时利用搜索到的区分器对PFP算法在相关密钥条件下进行了全轮的密钥恢复攻击 ,攻击所需数据复杂度为${2^{63}}$个选择明文,时间复杂度为${2^{48}}$次全轮加密,恢复出80 bit主密钥信息。这说明本算法在设计上存在明显的安全漏洞,无法抵抗相关密钥差分分析。
-
表 1 PFP算法攻击结果对比
表 2 PFP算法的S盒
x 0 1 2 3 4 5 6 7 8 9 A B C D E F S[x] C 5 6 B 9 0 A D 3 E F 8 4 7 1 2 表 3 S盒的差分分布表
输入差分 输出差分 0 1 2 3 4 5 6 7 8 9 A B C D E F 0 16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 4 0 0 0 4 0 4 0 0 0 4 0 0 2 0 0 0 2 0 4 2 0 0 0 2 0 2 2 2 0 3 0 2 0 2 2 0 4 2 0 0 2 2 0 0 0 0 4 0 0 0 0 0 4 2 2 0 2 2 0 2 0 2 0 5 0 2 0 0 2 0 0 0 0 2 2 2 4 2 0 0 6 0 0 2 0 0 0 2 0 2 0 0 4 2 0 0 4 7 0 4 2 0 0 0 2 0 2 0 0 0 2 0 0 4 8 0 0 0 2 0 0 0 2 0 2 0 4 0 2 0 4 9 0 0 2 0 4 0 2 0 2 0 0 0 2 0 4 0 A 0 0 2 2 0 4 0 0 2 0 2 0 0 2 2 0 B 0 2 0 0 2 0 0 0 4 2 2 2 0 2 0 0 C 0 0 2 0 0 4 0 2 2 2 2 0 0 0 2 0 D 0 2 4 2 2 0 0 2 0 0 2 2 0 0 0 0 E 0 0 2 2 0 0 2 2 2 2 0 0 2 2 0 0 F 0 4 0 0 4 0 0 0 0 0 0 0 0 0 4 4 表 4 PFP算法的差分界
轮数 最大期望差分特征概率 轮数 最大期望差分特征概率 单密钥 相关密钥 单密钥 相关密钥 1 20 20 18 2–44 2–34 2 2–2 20 19 2–46 2–36 3 2–4 20 20 2–48 2–38 4 2–6 20 21 2–51 2–40 5 2–8 20 22 2–54 2–42 6 2–12 2–3 23 2–56 2–44 7 2–16 2–5 24 2–58 2–46 8 2–18 2–9 25 2–61 2–48 9 2–21 2–14 26 2–64 2–50 10 2–24 2–18 27 2–66 2–52 11 2–26 2–20 28 2–68 2–54 12 2–28 2–22 29 2–71 2–56 13 2–31 2–24 30 2–74 2–58 14 2–34 2–26 31 2–76 2–60 15 2–36 2–28 32 2–78 2–62 16 2–38 2–30 33 2–81 2–64 17 2–41 2–32 34 2–84 2–66 表 5 差分特征概率为2–61的25轮差分区分器
轮数 左分支差分 右分支差分 轮数 左分支差分 右分支差分 0 0x00040D00 0x00000900 13 0x00000900 0x00000900 1 0x00000900 0x00000900 14 0x00000900 0x00000D00 2 0x00000900 0x00000D00 15 0x00000D00 0x00000D00 3 0x00000D00 0x00000D00 16 0x00000D00 0x00000900 4 0x00000D00 0x00000900 17 0x00000900 0x00000900 5 0x00000900 0x00000900 18 0x00000900 0x00000D00 6 0x00000900 0x00000D00 19 0x00000D00 0x00000D00 7 0x00000D00 0x00000D00 20 0x00000D00 0x00000900 8 0x00000D00 0x00000900 21 0x00000900 0x00000900 9 0x00000900 0x00000900 22 0x00000900 0x00000D00 10 0x00000900 0x00000D00 23 0x00000D00 0x00000D00 11 0x00000D00 0x00000D00 24 0x00000D00 0x00000900 12 0x00000D00 0x00000900 25 0x00000900 0x00040D00 表 6 差分特征概率为2–62的32轮相关密钥差分区分器
轮数 左右分支差分 相关密钥差分 轮数 左右分支差分 相关密钥差分 0 0x8BBBBA22D1111177 0xD111117777444445DDDD 17 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 1 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 18 0x8BBBBA22D1111177 0xD111117777444445DDDD 2 0x8BBBBA22D1111177 0xD111117777444445DDDD 19 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 3 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 20 0x8BBBBA22D1111177 0xD111117777444445DDDD 4 0x8BBBBA22D1111177 0xD111117777444445DDDD 21 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 5 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 22 0x8BBBBA22D1111177 0xD111117777444445DDDD 6 0x8BBBBA22D1111177 0xD111117777444445DDDD 23 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 7 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 24 0x8BBBBA22D1111177 0xD111117777444445DDDD 8 0x8BBBBA22D1111177 0xD111117777444445DDDD 25 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 9 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 26 0x8BBBBA22D1111177 0xD111117777444445DDDD 10 0x8BBBBA22D1111177 0xD111117777444445DDDD 27 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 11 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 28 0x8BBBBA22D1111177 0xD111117777444445DDDD 12 0x8BBBBA22D1111177 0xD111117777444445DDDD 29 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 13 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 30 0x8BBBBA22D1111177 0xD111117777444445DDDD 14 0x8BBBBA22D1111177 0xD111117777444445DDDD 31 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 15 0xD11111778BBBBA22 0x8BBBBA22222EEEE88888 32 0x8BBBBA22D1111177 - 16 0x8BBBBA22D1111177 0xD111117777444445DDDD 表 7 相关密钥下PFP算法密钥恢复阶段的复杂度计算
步数 猜测密钥 筛选后剩余明密文对数量 时间复杂度 1 ${K_{33}}[31,30,29,28]$ ${2^{m - 33 - 4}}$ $ 2 \cdot {2^{m - 33}} \cdot {2^4} $ 2 ${K_{33}}[23,22,21,20]$ ${2^{m - 37 - 4}}$ $ 2 \cdot {2^{m - 37}} \cdot {2^8} $ 3 ${K_{33}}[15,14,13,12]$ ${2^{m - 41 - 4}}$ $ 2 \cdot {2^{m - 41}} \cdot {2^{12}} $ 4 ${K_{33}}[7,6,5,4]$ ${2^{m - 45 - 4}}$ $ 2 \cdot {2^{m - 45}} \cdot {2^{16}} $ 5 ${K_{33}}[27,26,25,24]$ ${2^{m - 49 - 3}}$ $ 2 \cdot {2^{m - 49}} \cdot {2^{20}} $ 6 ${K_{33}}[19,18,17,16]$ ${2^{m - 52 - 3}}$ $ 2 \cdot {2^{m - 52}} \cdot {2^{24}} $ 7 ${K_{33}}[11,10,9,8]$ ${2^{m - 55 - 3}}$ $ 2 \cdot {2^{m - 55}} \cdot {2^{28}} $ 8 ${K_{33}}[3,2,1,0]$ ${2^{m - 58 - 3}}$ $ 2 \cdot {2^{m - 58}} \cdot {2^{32}} $ 9 ${K_{32}}[31,30,29,28]$ ${2^{m - 61 - 4}}$ $ 2 \cdot {2^{m - 61}} \cdot {2^{32}} $ 总和 ${2^{m - 24}} + {2^{m - 26}}$ -
[1] National Institute of Standards and Technology, DWORKIN M J, BARKER E, et al. Advanced encryption standard[R]. 197, 2001. doi: 10.6028/NIST.FIPS.197. [2] WU Wenling and ZHANG Lei. LBlock: A lightweight block cipher[C]. The 9th International Conference on Applied Cryptography and Network Security, Nerja, Spain, 2011: 327–344. doi: 10.1007/978-3-642-21554-4_19. [3] GUO Jian, PEYRIN T, POSCHMANN A, et al. The LED block cipher[C]. The 13th International Workshop on Cryptographic Hardware and Embedded Systems, Nara, Japan, 2011: 326–341. doi: 10.1007/978-3-642-23951-9_22. [4] BANIK S, PANDEY S K, PEYRIN T, et al. GIFT: A small present: Towards reaching the limit of lightweight encryption[C]. The 19th International Conference on Cryptographic Hardware and Embedded Systems, Taipei, China, 2017: 321–345. doi: 10.1007/978-3-319-66787-4_16. [5] BEAULIEU R, TREATMAN-CLARK S, SHORS D, et al. The SIMON and SPECK lightweight block ciphers[C]. Proceedings of the 52nd ACM/EDAC/IEEE Design Automation Conference, San Francisco, USA, 2015: 1–6. doi: 10.1145/2744769.2747946. [6] BOGDANOV A, KNUDSEN L R, LEANDER G, et al. PRESENT: An ultra-lightweight block cipher[C]. The 9th International Workshop, Vienna, Austria, 2007: 450–466. doi: 10.1007/978-3-540-74735-2_31. [7] 黄玉划, 代学俊, 时阳阳, 等. 基于Feistel结构的超轻量级分组密码算法(PFP)[J]. 计算机科学, 2017, 44(3): 163–167. doi: 10.11896/j.issn.1002-137X.2017.03.036.HUANG Yuhua, DAI Xuejun, SHI Yangyang, et al. Ultra-lightweight block cipher algorithm (PFP) based on Feistel structure[J]. Computer Science, 2017, 44(3): 163–167. doi: 10.11896/j.issn.1002-137X.2017.03.036. [8] BIHAM E and SHAMIR A. Differential cryptanalysis of DES-like cryptosystems[J]. Journal of Cryptology, 1991, 4(1): 3–72. doi: 10.1007/BF00630563. [9] MATSUI M. Linear cryptanalysis method for DES cipher[C]. The Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology (EUROCRYPT’93), Lofthus, Norway, 1993: 386–397. doi: 10.1007/3-540-48285-7_33. [10] HADIPOUR H, SADEGHI S and EICHLSEDER M. Finding the impossible: Automated search for full impossible-differential, zero-correlation, and integral attacks[C]. The 42nd Annual International Conference on the Theory and Applications of Cryptographic Techniques on Advances in Cryptology (EUROCRYPT 2023), Lyon, France, 2023: 128–157. doi: 10.1007/978-3-031-30634-1_5. [11] HADIPOUR H, GERHALTER S, SADEGHI S, et al. Improved search for integral, impossible differential and zero-correlation attacks[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(1): 234–325. doi: 10.46586/tosc.v2024.i1.234-325. [12] LAI Xuejia. Higher order derivatives and differential cryptanalysis[M]. BLAHUT R E, COSTELLO D J, MAURER U, et al. Communications and Cryptography: Two Sides of One Tapestry. Boston: Springer, 1994: 227–233. doi: 10.1007/978-1-4615-2694-0_23. [13] AHMADIAN Z, KHALESI A, M’FOUKH D, et al. Truncated differential cryptanalysis: New insights and application to QARMAv1-n and QARMAv2–64[J]. Designs, Codes and Cryptography, 2024, 92(12): 4549–4591. doi: 10.1007/s10623-024-01486-8. [14] BIHAM E. New types of cryptanalytic attacks using related keys[J]. Journal of Cryptology, 1994, 7(4): 229–246. doi: 10.1007/BF00203965. [15] ROHIT R and SARKAR S. Reconstructing s-boxes from cryptographic tables with MILP[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(3): 200–237. doi: 10.46586/tosc.v2024.i3.200-237. [16] CHAKRABORTY D, HADIPOUR H, NGUYEN P H, et al. Finding complete impossible differential attacks on AndRX ciphers and efficient distinguishers for ARX designs[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(3): 84–176. doi: 10.46586/tosc.v2024.i3.84-176. [17] WANG Dachao, WANG Baocang, and SUN Siwei. SAT-aided automatic search of boomerang distinguishers for ARX ciphers[J]. IACR Transactions on Symmetric Cryptology, 2023, 2023(1): 152–191. doi: 10.46586/tosc.v2023.i1.152-191. [18] ERLACHER J, MENDEL F, and EICHLSEDER M. Bounds for the security of ascon against differential and linear cryptanalysis[J]. IACR Transactions on Symmetric Cryptology, 2022, 2022(1): 64–87. doi: 10.46586/tosc.v2022.i1.64-87. [19] 沈璇, 王欣玫, 何俊, 等. PFP算法改进的不可能差分分析[J]. 计算机科学, 2020, 47(7): 263–267. doi: 10.11896/jsjkx.200200034.SHEN Xuan, WANG Xinmei, HE Jun, et al. Revised impossible differential cryptanalysis of PFP block cipher[J]. Computer Science, 2020, 47(7): 263–267. doi: 10.11896/jsjkx.200200034. [20] 赵光耀, 沈璇, 余波, 等. 缩减轮的超轻量级分组密码算法PFP的不可能差分分析[J]. 计算机应用, 2023, 43(9): 2784–2788. doi: 10.11772/j.issn.1001-9081.2022091395.ZHAO Guangyao, SHEN Xuan, YU Bo, et al. Impossible differential cryptanalysis of reduced-round ultra-lightweight block cipher PFP[J]. Journal of Computer Applications, 2023, 43(9): 2784–2788. doi: 10.11772/j.issn.1001-9081.2022091395. [21] 刘道瞳, 袁征, 魏锦鹏, 等. 轻量级分组密码算法PFP和SLIM的积分分析[J]. 密码学报, 2023, 10(3): 609–621. doi: 10.13868/j.cnki.jcr.000617.LIU Daotong, YUAN Zheng, WEI Jinpeng, et al. Integral cryptanalysis of lightweight block cipher PFP and SLIM[J]. Journal of Cryptologic Research, 2023, 10(3): 609–621. doi: 10.13868/j.cnki.jcr.000617. [22] 李艳俊, 李寅霜, 杨明华, 等. 轻量级PFP算法的差分攻击[J]. 计算机工程与应用, 2023, 59(21): 296–302. doi: 10.3778/j.issn.1002-8331.2305-0193.LI Yanjun, LI Yinshuang, YANG Minghua, et al. Differential attack on lightweight PFP algorithm[J]. Computer Engineering and Applications, 2023, 59(21): 296–302. doi: 10.3778/j.issn.1002-8331.2305-0193. [23] COOK S A. The complexity of theorem-proving procedures[C]. The Third Annual ACM Symposium on Theory of Computing (STOC’71), Shaker Heights, USA, 1971: 151–158. doi: 10.1145/800157.805047. [24] DE MOURA L and BJØRNER N. Z3: An efficient SMT solver[C]. The 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Budapest, Hungary, 2008: 337–340. doi: 10.1007/978-3-540-78800-3_24. [25] BARRETT C, CONWAY C L, DETERS M, et al. CVC4[C]. The 23rd International Conference on Computer aided verification (CAV 2011), Snowbird, USA, 2011: 171–177. [26] CIMATTI A, GRIGGIO A, SCHAAFSMA B J, et al. The MathSAT5 SMT solver[C]. The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, 2013: 93–107. doi: 10.1007/978-3-642-36742-7_7. [27] BRUMMAYER R and BIERE A. Boolector: An efficient SMT solver for bit-vectors and arrays[C]. The 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, UK, 2009: 174–177. doi: 10.1007/978-3-642-00768-2_16. [28] GANESH V and DILL D L. A decision procedure for bit-vectors and arrays[C]. The 19th International Conference on Computer Aided Verification (CAV 2007), Berlin, Germany, 2007: 519–531. doi: 10.1007/978-3-540-73368-3_52. [29] STUMP A, BARRETT C W, and DILL D L. CVC: A cooperating validity checker[C]. The 14th International Conference on Computer Aided Verification (CAV 2002), Copenhagen, Denmark, 2002: 500–504. doi: 10.1007/3-540-45657-0_40. [30] SELÇUK A A. On probability of success in linear and differential cryptanalysis[J]. Journal of Cryptology, 2008, 21(1): 131–147. doi: 10.1007/s00145-007-9013-7. -