Ambrona, Miguel ; Farshim, Pooya ; Harasser, Patrick (2024)
Block Ciphers in Idealized Models: Automated Proofs and New Security Results.
31st ACM Conference on Computer and Communications Security (CCS 2024). Salt Lake City, USA (14.10.2024 - 18.10.2024)
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2024 |
| Autor(en): | Ambrona, Miguel ; Farshim, Pooya ; Harasser, Patrick |
| Art des Eintrags: | Bibliographie |
| Titel: | Block Ciphers in Idealized Models: Automated Proofs and New Security Results |
| Sprache: | Englisch |
| Publikationsjahr: | 19 Oktober 2024 |
| Veranstaltungstitel: | 31st ACM Conference on Computer and Communications Security (CCS 2024) |
| Veranstaltungsort: | Salt Lake City, USA |
| Veranstaltungsdatum: | 14.10.2024 - 18.10.2024 |
| Zugehörige Links: | |
| Kurzbeschreibung (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. |
| Freie Schlagworte: | P2 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Kryptographie und Komplexitätstheorie DFG-Sonderforschungsbereiche (inkl. Transregio) DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche DFG-Graduiertenkollegs DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1119: CROSSING – Kryptographiebasierte Sicherheitslösungen als Grundlage für Vertrauen in heutigen und zukünftigen IT-Systemen |
| Hinterlegungsdatum: | 25 Okt 2024 14:25 |
| Letzte Änderung: | 25 Okt 2024 14:25 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum