Paper 2019/1037

Card-based Cryptography Meets Formal Verification

Alexander Koch, Michael Schrempp, and Michael Kirsten

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., clubs and hearts. 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 AND, 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 AND protocol to have a shortest run for protocols using this number of cards.

Note: This is the full version, with more detailed proofs for Theorems 1 and 2.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
A minor revision of an IACR publication in ASIACRYPT 2019
DOI
10.1007/978-3-030-34578-5_18
Keywords
secure multiparty computationcard-based cryptographyformal verificationbounded model checkingstandard decks
Contact author(s)
alexander koch @ kit edu
History
2019-11-22: revised
2019-09-16: received
See all versions
Short URL
https://ia.cr/2019/1037
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/1037,
      author = {Alexander Koch and Michael Schrempp and Michael Kirsten},
      title = {Card-based Cryptography Meets Formal Verification},
      howpublished = {Cryptology ePrint Archive, Paper 2019/1037},
      year = {2019},
      doi = {10.1007/978-3-030-34578-5_18},
      note = {\url{https://eprint.iacr.org/2019/1037}},
      url = {https://eprint.iacr.org/2019/1037}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.