Block Ciphers in Idealized Models: Automated Proofs and New Security Results

Ambrona, Miguel; Farshim, Pooya; Harasser, Patrick

Abstract

We develop and implement AlgoROM, a tool to systematically analyze the security of a wide class of symmetric primitives in idealized models of computation. The schemes that we consider are those that can be expressed over an alphabet consisting of XOR and function symbols for hash functions, permutations, or block ciphers. We implement our framework in OCaml and apply it to a number of prominent constructions, which include the Luby-Rackoff (LR), key-alternating Feistel (KAF), and iterated Even-Mansour (EM) ciphers, as well as substitution-permutation networks (SPN). The security models we consider are (S)PRP, and strengthenings thereof under related-key (RK), key-dependent message (KD), and more generally key-correlated (KC) attacks. Using AlgoROM, we are able to reconfirm a number of classical and previously established security theorems, and in one case we identify a gap in a proof from the literature (Connolly et al., ToSC'19). However, most results that we prove with AlgoROM are new. In particular, we obtain new positive results for LR, KAF, EM, and SPN in the above models. Our results better reflect the configurations actually implemented in practice, as they use a single idealized primitive. In contrast to many existing tools, our automated proofs do not operate in symbolic models, but rather in the standard probabilistic model for cryptography.

Citation

Ambrona, M., Farshim, P., & Harasser, P. (2024, October). Block Ciphers in Idealized Models: Automated Proofs and New Security Results. Presented at ACM SIGSAC Conference on Computer and Communications Security 2024, Salt Lake City, USA

• Presentation Conference Type: Conference Paper (published)
• Conference Name: ACM SIGSAC Conference on Computer and Communications Security 2024
• Start Date: Oct 14, 2024
• End Date: Oct 18, 2024
• Acceptance Date: Aug 14, 2024
• Online Publication Date: Dec 9, 2024
• Publication Date: Dec 9, 2024
• Deposit Date: Jan 9, 2025
• Publicly Available Date: Jan 15, 2025
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Pages: 2771-2785
• Book Title: CCS '24: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security
• ISBN: 9798400706363
• DOI: https://doi.org/10.1145/3658644.3690222
• Keywords: Automated Proofs; Idealized Models; Luby-Rackoff; Key-Alternating Feistel; Even-Mansour; Substitution-Permutation Network
• Public URL: https://durham-repository.worktribe.com/output/3328866
• Related Public URLs: https://eprint.iacr.org/2024/1584