KIT | KIT-Bibliothek | Impressum | Datenschutz

Card-Based Cryptography Meets Formal Verification

Koch, Alexander; Schrempp, Michael; Kirsten, Michael

Card-based cryptography provides simple and practicable protocols for performing secure multi-party computation (MPC) with just a deck of cards. For the sake of simplicity, this is often done using cards with only two symbols, e.g., ♣ and ♡. Within this paper, we target the setting where all cards carry distinct symbols, catering for use-cases with commonly available standard decks and a weaker indistinguishability assumption. As of yet, the literature provides for only three protocols and no proofs for non-trivial lower
bounds on the number of cards. As such complex proofs (handling very large combinatorial state spaces) tend to be involved and error-prone, we propose using formal verification for finding protocols and proving lower bounds. In this paper, we employ the technique of software bounded model checking (SBMC), which reduces the problem to a bounded state space, which is automatically searched exhaustively using a SAT solver as a backend.
Our contribution is twofold: (a) We identify two protocols for converting between different bit encodings with overlapping bases, and then show them to be card-minimal. This completes the picture of tight lower bounds on the number of cards with respect to runtime behavior and shuffle properties of conversion protocols. ... mehr

Open Access Logo

Postprint §
DOI: 10.5445/IR/1000120008
Frei zugänglich ab 26.11.2020
DOI: 10.1007/978-3-030-34578-5_18
Zitationen: 1
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2019
Sprache Englisch
Identifikator ISBN: 978-3-030-34577-8
KITopen-ID: 1000120008
Erschienen in Advances in Cryptology – ASIACRYPT 2019 : 25th International Conference on the Theory and Application of Cryptology and Information Security, Kobe, Japan, December 8–12, 2019, Proceedings. Part I. Ed.: S.D. Galbraith
Auflage 1st ed.
Verlag Springer, Cham
Seiten 488–517
Serie Security and Cryptology ; 11921
Vorab online veröffentlicht am 25.11.2019
Schlagwörter Secure multiparty computation, Card-based cryptography, Formal verification, Bounded model checking, Standard decks
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page