International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Card-Based Cryptography Meets Formal Verification

Authors:
Alexander Koch
Michael Schrempp
Michael Kirsten
Download:
DOI: 10.1007/978-3-030-34578-5_18
Search ePrint
Search Google
Abstract: 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. For computing , we show that there is no protocol with finite runtime using four cards with distinguishable symbols and fixed output encoding, and give a four-card protocol with an expected finite runtime using only random cuts. (b) We provide a general translation of proofs for lower bounds to a bounded model checking framework for automatically finding card- and length-minimal protocols and to give additional confidence in lower bounds. We apply this to validate our method and, as an example, confirm our new protocol to have a shortest run for protocols using this number of cards.
BibTeX
@article{asiacrypt-2019-30025,
  title={Card-Based Cryptography Meets Formal Verification},
  booktitle={Advances in Cryptology – ASIACRYPT 2019},
  series={Advances in Cryptology – ASIACRYPT 2019},
  publisher={Springer},
  volume={11921},
  pages={488-517},
  doi={10.1007/978-3-030-34578-5_18},
  author={Alexander Koch and Michael Schrempp and Michael Kirsten},
  year=2019
}