State separation for code-based game-playing proofs

Chris Brzuska*, Antoine Delignat-Lavaud, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

2 Sitaatiot (Scopus)

Abstrakti

The security analysis of real-world protocols involves reduction steps that are conceptually simple but still have to account for many protocol complications found in standards and implementations. Taking inspiration from universal composability, abstract cryptography, process algebras, and type-based verification frameworks, we propose a method to simplify large reductions, avoid mistakes in carrying them out, and obtain concise security statements. Our method decomposes monolithic games into collections of stateful packages representing collections of oracles that call one another using well-defined interfaces. Every component scheme yields a pair of a real and an ideal package. In security proofs, we then successively replace each real package with its ideal counterpart, treating the other packages as the reduction. We build this reduction by applying a number of algebraic operations on packages justified by their state separation. Our method handles reductions that emulate the game perfectly, and leaves more complex arguments to existing game-based proof techniques such as the code-based analysis suggested by Bellare and Rogaway. It also facilitates computer-aided proofs, inasmuch as the perfect reductions steps can be automatically discharged by proof assistants. We illustrate our method on two generic composition proofs: a proof of self-composition using a hybrid argument; and the composition of keying and keyed components. For concreteness, we apply them to the KEM-DEM proof of hybrid-encryption by Cramer and Shoup and to the composition of forward-secure game-based key exchange protocols with symmetric-key protocols.

AlkuperäiskieliEnglanti
OtsikkoAdvances in Cryptology – ASIACRYPT 2018 - 24th International Conference on the Theory and Application of Cryptology and Information Security, Proceedings
ToimittajatThomas Peyrin, Steven Galbraith
Sivut222-249
Sivumäärä28
ISBN (elektroninen)9783030033316
DOI - pysyväislinkit
TilaJulkaistu - 1 tammikuuta 2018
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on the Theory and Application of Cryptology and Information Security - Brisbane, Austraalia
Kesto: 2 joulukuuta 20186 joulukuuta 2018
Konferenssinumero: 24

Julkaisusarja

NimiLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vuosikerta11274 LNCS
ISSN (painettu)0302-9743
ISSN (elektroninen)1611-3349

Conference

ConferenceInternational Conference on the Theory and Application of Cryptology and Information Security
LyhennettäASIACRYPT
MaaAustraalia
KaupunkiBrisbane
Ajanjakso02/12/201806/12/2018

Sormenjälki Sukella tutkimusaiheisiin 'State separation for code-based game-playing proofs'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä