Quantitative analyses of the costs of cryptographic attack algorithms play a central role in comparing cryptosystems, guiding the search for improved attacks, and deciding which cryptosystems to standardize. Unfortunately, these analyses often turn out to be wrong.

Formally verifying complete proofs of attack performance is a natural response but crashes into an insurmountable structural problem: there are large gaps between the best proven cost among known attack algorithms and the best conjectured cost among known attack algorithms. Ignoring conjectured speedups would be a security disaster.

The CryptAttackTester (CAT) software demonstrates the feasibility and value of successfully formalizing what state-of-the-art attack analyses actually do. The input to this formalization is not a proof, and the output is not a formally verified proof; the formalization process nevertheless enforces clear definitions, systematically accounts for all algorithm steps, simplifies review, improves reproducibility, and reduces the risk of error.

CAT includes formal specifications of (1) a general-purpose model of computation and cost metric, (2) various attack algorithms, and (3) formulas predicting the cost and success probability of each algorithm. The software includes general-purpose simulators that systematically compare the predictions to the observed attack behavior in the same model. The accompanying paper gives various examples of errors in the literature that survived typical informal testing practices and that would have been immediately caught if CAT-enforced links had been in place.

Currently CAT includes two case studies. The first case study is a simple baseline, namely enumerating AES-128 keys. The second case study is information-set decoding (ISD), the top attack strategy against the McEliece cryptosystem. CAT formalizes analyses of many ISD algorithms, covering interactions between (1) high-level search strategies from Prange, Lee–Brickell, Leon, Stern, Dumer, May–Meurer–Thomae, and Becker–Joux–May–Meurer; (2) random walks from Omura, Canteaut–Chabaud, Canteaut–Sendrier, and Bernstein–Lange–Peters; and (3) speedups in core subroutines such as linear algebra and sorting.

Contributors, alphabetical order

• Daniel J. Bernstein (Department of Computer Science, University of Illinois at Chicago, USA, and Horst Görtz Institute for IT Security, Ruhr University Bochum, Germany)
• Tung Chou (Research Center of Information Technology and Innovation, Academia Sinica, Taiwan)

Funding

This work was funded by the Intel Crypto Frontiers Research Center; by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) as part of the Excellence Strategy of the German Federal and State Governments—EXC 2092 CASA—390781972 "Cyber Security in the Age of Large-Scale Adversaries"; by the U.S. National Science Foundation under grant 1913167; by the Taiwan’s Executive Yuan Data Safety and Talent Cultivation Project (AS-KPQ-109-DSTCP); and by the Taiwan's National Science and Technology Council (NSTC) grant 109-2222-E-001-001-MY3. "Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation" (or other funding agencies).