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

• 学术论文 • 上一篇    下一篇

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

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

  1. 战略支援部队信息工程大学, 河南郑州 450001
  • 收稿日期:2018-07-11 修回日期:2019-02-26 出版日期:2019-12-25 发布日期: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   

  1. PLA Information Engineering University, Zhengzhou, Henan 450001, China
  • Received:2018-07-11 Revised:2019-02-26 Online:2019-12-25 Published:2019-12-25

摘要: 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算法在特殊输入输出差分和掩码集合下,不可能差分和零相关区分器轮数的上界.

关键词: 不可能差分区分器, 零相关区分器, ARX, Chaskey, SPECK, HIGHT, SAT求解器

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

中图分类号: