基于SAT的ARX不可能差分和零相关区分器的自动化搜索

doi:10.3969/j.issn.0372-2112.2019.12.010

电子学报 ›› 2019, Vol. 47 ›› Issue (12): 2524-2532.DOI: 10.3969/j.issn.0372-2112.2019.12.010

基于SAT的ARX不可能差分和零相关区分器的自动化搜索

任炯炯, 张仕伟, 李曼曼, 陈少真

战略支援部队信息工程大学, 河南郑州 450001

收稿日期:2018-07-11 修回日期:2019-02-26 出版日期:2019-12-25
- 作者简介:
- 任炯炯 男,1994年生于甘肃天水,信息工程大学博士研究生,研究方向为对称密码设计与分析.E-mail:jiongjiong_fun@163.com;张仕伟 男,1988年生于河北唐山,信息工程大学硕士生,究方向为对称密码设计与分析.;李曼曼 女,1986年出生于河南开封,信息工程大学讲师,研究方向为对称密码设计与分析.;陈少真 女,1967年生于江苏无锡,信息工程大学教授,研究方向为密码学与信息安全.
- 基金资助:
- 国家密码发展基金 (No.MMJJ20180203）; 数学工程与先进计算国家重点实验室开放基金 (No.2018A03）; 信息保障技术重点实验室开放基金 (No.KJ-17-002）

SAT-Based Automatic Search for Impossible Differentials and Zero-Correlation Linear Approximations in ARX

REN Jiong-jiong, ZHANG Shi-wei, LI Man-man, CHEN Shao-zhen

PLA Information Engineering University, Zhengzhou, Henan 450001, China

Received:2018-07-11 Revised:2019-02-26 Online:2019-12-25 Published:2019-12-25
- Supported by:
- National Cryptography Development Fund (No.MMJJ20180203); Open Fund of State Key Laboratory of Mathematical Engineering and Advanced Computing (No.2018A03); Open Fund of Key Laboratory of Information Assurance Technology (No.KJ-17-002)

摘要/Abstract

摘要： ARX（Addition，Rotation，Xor）算法基于模整数加，异或加和循环移位三种运算，便于软硬件的快速实现.不可能差分分析和零相关分析是攻击ARX的有效方法，攻击的关键是搜索更长轮数、更多数量的不可能差分和零相关区分器.目前很多的搜索方法都没有充分考虑非线性组件的性质，往往不能搜索得到更好、更准确的区分器.本文提出了基于SAT（Satisfiability）的ARX不可能差分和零相关区分器的自动化搜索算法.通过分析ARX算法组件的性质，特别是常规模加和密钥模加这两种非线性运算差分和线性传播的特性，给出了高效简单的SAT约束式.在此基础上，建立SAT模型进行区分器的搜索.作为应用，本文首次给出了Chaskey算法13条4轮不可能差分和1条4轮零相关区分器；首次给出了SPECK32算法10条6轮零相关区分器和SPECK48算法15条6轮零相关区分器；在较短的时间内，给出了HIGHT算法17轮的不可能差分和零相关区分器.与现有结果相比，无论是区分器的条数，还是搜索区分器的时间均有明显的提升.此外，通过重新封装求解器STP的输出接口，建立了自动化的SAT\\SMT分析模型，能够给出ARX算法在特殊输入输出差分和掩码集合下，不可能差分和零相关区分器轮数的上界.

Abstract: ARX (Addition, Rotation, Xor) algorithms are based on three operations:modular addition, exclusive-OR and bitwise rotation, which execute very fast in both software and hardware. Impossible differential cryptanalysis and zero-correlation linear cryptanalysis are among the most powerful attacks for ARX ciphers. The key problem for the attacks is searching more and longer impossible differentials and zero-correlation linear approximations. Although there are many automatic search algorithms, these approaches do not fully utilize the non-linear component properties, which cannot reach their potential. A SAT (Satisfiability) -based model to automatic search for impossible differentials and zero-correlation linear approximations in ARX is proposed.By exploiting behaviors of every component, especially the differential and linear propagation properties through general modular addition and key modular addition operations, we generate computable and easily implementable constraints and establish the SAT-based model. As applications, we apply our model to Chaskey, SPECK and HIGHT. For Chaskey, we are able to find 13 4-round impossible differentials and 1 4-round zero-correlation linear approximation for the first time. For SPECK, we first find 10 6-round zero-correlation linear approximations of SPECK32 and 15 6-round zero-correlation linear approximations of SPECK48. Besides, we find 4 17-round impossible differentials and zero-correlation linear approximations of HIGHT in a few minutes. Compared with the existing results, both the number and the search time of distinguishers are significantly improved. In addition, by repackaging the output interface of the STP solver, we establish the automated SAT\\SMT model, which can give the upper bound of rounds of impossible differentials and zero-correlation linear approximations under special input and output differential and mask sets for ARX algorithm.

Key words: impossible differential, zero-correlation linear approximation, ARX, Chaskey, SPECK, HIGHT, SAT-solver

中图分类号:

TN918.1

任炯炯, 张仕伟, 李曼曼, 等. 基于SAT的ARX不可能差分和零相关区分器的自动化搜索[J]. 电子学报, 2019, 47(12): 2524-2532.

REN Jiong-jiong, ZHANG Shi-wei, LI Man-man, et al. SAT-Based Automatic Search for Impossible Differentials and Zero-Correlation Linear Approximations in ARX[J]. Acta Electronica Sinica, 2019, 47(12): 2524-2532.

参考文献

[1] R Beaulieu,D Shors,J Smith,et al.The SIMON and SPECK families of lightweight block ciphers[DB/OL].http://eprint.iacr.org/2013/404/2013-06-20.
[2] D Hong,J K Lee,D C Kim,et al.LEA:A 128-bit block cipher for fast encryption on common processors[A].International Workshop on Information Security Applications[C].Heidelberg:Springer,2013.3-27.
[3] D J Wheeler,R M Needham.TEA,a tiny encryption algorithm[A].FSE 1995[C].Heidelberg:Springer,LNCS,1995.363-366.
[4] R M Needham,D J Wheeler l.TEA extensions[R].Cambridge:University of Cambridge,1997.
[5] D Hong,J Sung,S Hong,J Lim,et al.HIGHT:A new block cipher suitable for low-resource device[A].Cryptographic Hardware and Embedded Systems-CHES 2006[C].Heidelberg:Springer,2006.46-59.
[6] N Mouha,B Mennink,A Van Herrewege,D Watanabe,B Preneel,I Ver-bauwhede.Chaskey:An efficient MAC algorithm for 32-bit microcontrollers[A].Selected Areas in Cryptography-SAC 2014[C].Heidelberg:Springer,2014.306-323.
[7] D Dinu,L Perrin,A Udovenko,V Velichkov,et al.Design strategies for ARX with provable bounds:Sparx and LAX[A].ASIACRYPT 2016[C].Heidelberg:Springer,2016.484-513.
[8] L R Knudsen.DEAL a 128-bit block cipher[R].Bergen:Department of Informatics,University of Bergen,1998.
[9] E Biham,A Biryukov,A Shamir.Cryptanalysis of Skipjack reduced to 31 rounds using impossibledifferentials[A].EUROCRYPT 1999[C].Heidelberg:Springer,1999.291-311.
[10] C W Phan.Impossible differential cryptanalysis of 7-round Advanced Encryption Standard (AES)[J].Information Processing Letters,2004,91(1),33-38.
[11] D Yang,W Qi,H Chen.Impossible differential attack on QARMA family of block ciphers[DB/OL].http://eprint.iacr.org/2018/334,2018-04-11.
[12] A Bogdanov,V Rijmen.Linear hulls with correlation zero and linear cryptanalysis of block ciphers[J].Designs,Codes and Cryptography,2014,70(3):369-383.
[13] J Kim,S Hong,J Lim.Impossible differential cryptanalysis using matrix method[J].Discrete Mathematics,2010,310(5):988-1002.
[14] Y Luo,X Lai,Z Wu,G Gong.A unified method for finding impossible differentials of block cipher structures[J].Information Sciences,2014,263(1):211-220.
[15] S Wu,M Wang.Automatic search of truncated impossible differentials for word-oriented block ciphers[A].INDOCRYPT 2012[C].Heidelberg:Springer,2012.283-302.
[16] T Cui,K Jia,K Fu,et al.New automatic search tool for impossible differentials and zero-correlation linearapproximations[DB/OL].http://eprint.iacr.org/2016/689,2018-11-21.
[17] Y Sasaki,Y Todo.New impossible differential search tool from design and cryptanalysis aspects revealing structural properties of several ciphers[A].EUROCRYPT 2017[C].Heidelberg:Springer,2017,185-215.
[18] N Mouha,B Preneel.Towards finding optimal differential characteristics for ARX:Application to Salsa20[DB/OL].http://eprint.iacr.org/2013/328,2013-11-23.
[19] L Song,Z Huang,Q Yang.Automatic differential analysis of ARX block ciphers with application to SPECK and LEA[A].ACISP 2016[C].Heidelberg:Springer,2016.379-394.
[20] Y Liu,Q Wang,V Rijmen.Automatic search of linear trails in ARX with applications to SPECK and Chaskey[A].ACNS 2016[C].Heidelberg:Springer,2016.485-499.
[21] S Kölbl,G.Leander,T Tiessen.Observations on the SIMON block cipher family[A].CRYPTO 2015[C].Heidelberg:Springer,2015.161-185.
[22] H Lipmaa,S Moriai.Efficient algorithms for computing differential properties of addition[A].FSE 2002[C].Heidelberg:Springer,2002.336-350.
[23] E Schulte-Geers.On CCZ-equivalence of addition mod 2ⁿ[J].Designs,Codes and Cryptography,2013,66(1-3):111-127.
[24] A Bogdanov,M Wang.Zero correlation linear cryptanalysis with reduced data complexity[A].FSE 2012[C].Heidelberg:Springer,2012.29-48.
[25] H Lee,H Kang,D Hong et al.New impossible differential characteristic of SPECK64 using MILP[DB/OL].http://eprint.iacr.org/2016/1137,2016-12-21.
[26] J Lu.Cryptanalysis of reduced versions of the HIGHT block cipher from CHES 2006[A].ICISC 2007[C].Heidelberg:Springer,2007.11-26.
[27] L Wen,M Wang,A Bogdanov,H Chen.Multidimensional zero-correlation attacks on lightweight block cipher HIGHT:Improved cryptanalysis of an ISO standard[J].Information Processing Letters,2014,114(6):322-330.

基于SAT的ARX不可能差分和零相关区分器的自动化搜索

SAT-Based Automatic Search for Impossible Differentials and Zero-Correlation Linear Approximations in ARX

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 6

编辑推荐

Metrics

[1]	李航, 任炯炯, 陈少真. 减轮LEA密码算法的积分攻击[J]. 电子学报, 2020, 48(1): 17-27.
[2]	刘梦, 欧阳丹彤, 刘伯文, 张立明, 张永刚. 结合问题特征的分组式诊断方法[J]. 电子学报, 2018, 46(3): 589-594.
[3]	赵相福;欧阳丹彤;. 使用SAT求解器产生所有极小冲突部件集[J]. 电子学报, 2009, 37(4): 804-810.
[4]	付强, Peter Murphy, 颜永红. 一种基于联合源-滤波器模型优化的语音声门源模型估计方法[J]. 电子学报, 2007, 35(5): 982-986.
[5]	吴家骥, 吴成柯, 吴振森. 三维图像的任意形状ROI小波零块压缩编码算法[J]. 电子学报, 2006, 34(10): 1828-1832.
[6]	卓力, 沈兰荪, 李朝峰, 朱青. 基于DCT变换的渐进式图像编码方法[J]. 电子学报, 2002, 30(S1): 2105-2107.