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

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Forschungsbericht/Preprint
Publikationsdatum 16.09.2019
Sprache Englisch
Identifikator KITopen-ID: 1000120005
Serie Cryptology ePrint Archive ; 2019/1037
Externe Relationen Siehe auch
Schlagwörter secure multiparty computation, card-based cryptography, formal verification, bounded model checking, standard decks
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page