KIT | KIT-Bibliothek | Impressum | Datenschutz

Card-Based Cryptography Meets Formal Verification

Koch, Alexander 1; Schrempp, Michael 1; Kirsten, Michael ORCID iD icon 1
1 Karlsruher Institut für Technologie (KIT)

Abstract:

Card-based cryptography provides simple and practicable protocols for performing secure multi-party computation 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 also 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 threefold: (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


Verlagsausgabe §
DOI: 10.5445/IR/1000135138
Veröffentlicht am 08.07.2021
Originalveröffentlichung
DOI: 10.1007/s00354-020-00120-0
Scopus
Zitationen: 11
Web of Science
Zitationen: 8
Dimensions
Zitationen: 10
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Publikationsmonat/-jahr 04.2021
Sprache Englisch
Identifikator ISSN: 0288-3635, 1882-7055
KITopen-ID: 1000135138
Erschienen in New generation computing
Verlag Springer
Band 39
Seiten 115–158
Vorab online veröffentlicht am 02.04.2021
Nachgewiesen in Dimensions
Scopus
Web of Science
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page