An Automated Fault Attack Framework for Block Ciphers Through Property Mining and Verification

Fault attacks are effective side-channel attack methods for cryptanalysis. However, existing fault attack methods involve manual derivation of complex fault models or computation-intensive statistical analysis of mass faulty ciphertexts to recover the key. In addition, most methods are only applicable to a specific cryptographic algorithm with strict requirements on the type and quantity of faults injected, lacking scalability and generality. Taking inspiration from machine learning and formal verification, we propose an automated fault attack framework, which supports multi-byte fault attacks on both SPN and generalized Feistel structure ciphers. This framework automates the generation of formal fault propagation models, extraction of fault properties, and formal fault analysis. We construct formal fault propagation models for cipher designs to measure the fault propagation precisely, eliminating the requirement of manually deriving fault propagation models. We mine accurate invariable behaviors in fault propagation effects as fault properties using a small number of fault traces and further utilize property constraints to retrieve the key through formal analysis. This method implements a formal fault attack on SM4 in 25th to 28th rounds for the first time. Experimental results on AES, RSM, LED and SM4 demonstrate the effectiveness of our method, with key search complexity lower than or equal to state-of-the-art methods, while requiring only four faulty ciphertexts to recover a round key.