A SAT-based preimage analysis of reduced KECCAK hash functions

被引：28
|
作者：
Morawiecki, Pawel [1 ,2 ]
Srebrny, Marian [1 ,2 ]
机构：
[1] Kielce Univ Commerce, PL-25562 Kielce, Poland
[2] Polish Acad Sci, Inst Comp Sci, PL-01237 Warsaw, Poland
来源：
INFORMATION PROCESSING LETTERS | 2013年 / 113卷 / 10-11期
关键词：
Cryptography; Hash functions; KECCAK; Algebraic cryptanalysis; Logical cryptanalysis; SAT solvers; CRYPTANALYSIS; SOLVERS;
D O I：
10.1016/j.ipl.2013.03.004
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper, we present a preimage attack on reduced versions of KECCAK hash functions. We use our recently developed toolkit CryptLogVer for generating the conjunctive normal form, CNF, which is passed to the SAT solver PrecoSAT. We found preimages for some reduced versions of the function and showed that full KECCAK function has a comfortable security margin against this kind of attack. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码：392 / 397
页数：6
相关论文
共 50 条
  • [41] An analysis of SAT-based model checking techniques in an industrial environment
    Amla, N
    Du, XQ
    Kuehlmann, A
    Kurshan, RP
    McMillan, KL
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 254 - 268
  • [42] A SAT-based algorithm for context matching
    Bouquet, P
    Magnini, B
    Serafini, L
    Zanobini, S
    [J]. MODELING AND USING CONTEXT, PROCEEDINGS, 2003, 2680 : 66 - 79
  • [43] The SAT-based Approach to Separation Logic
    Alessandro Armando
    Claudio Castellini
    Enrico Giunchiglia
    Marco Maratea
    [J]. Journal of Automated Reasoning, 2005, 35 : 237 - 263
  • [44] SAT-based model-checking for security protocols analysis
    Armando, Alessandro
    Compagna, Luca
    [J]. INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (01) : 3 - 32
  • [45] SAT-Based ATL Satisfiability Checking
    Kacprzak, Magdalena
    Niewiadomski, Artur
    Penczek, Wojciech
    [J]. KR2020: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2020, : 539 - 549
  • [46] The SAT-based approach to separation logic
    Armando, Alessandro
    Castellini, Claudio
    Giunchiglia, Enrico
    Maratea, Marco
    [J]. JOURNAL OF AUTOMATED REASONING, 2005, 35 (1-3) : 237 - 263
  • [47] Preimage Attacks on Round-Reduced KECCAK-224/256 via an Allocating Approach
    Li, Ting
    Sun, Yao
    [J]. ADVANCES IN CRYPTOLOGY - EUROCRYPT 2019, PT III, 2019, 11478 : 556 - 584
  • [48] SAT-based summarization for boolean programs
    Basler, Gerard
    Kroening, Daniel
    Weissenbacher, Georg
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2007, 4595 : 131 - +
  • [49] Interpolation and SAT-based model checking
    McMillan, KL
    [J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 1 - 13
  • [50] SAT-Based Methods for Circuit Synthesis
    Bloem, Roderick
    Egly, Uwe
    Klampfl, Patrick
    Koenighofer, Robert
    Lonsing, Florian
    [J]. 2014 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2014, : 31 - 34
12345