Card-Based Cryptography Meets Formal Verification

@article{KochSchremppKirsten2019b,
  author                = {Alexander Koch and
                           Michael Schrempp and
                           Michael Kirsten},
  title                 = {Card-Based Cryptography Meets Formal Verification},
  journal               = {{IACR} Cryptology ePrint Archive},
  url                   = {https://eprint.iacr.org/2019/1037},
  volume                = {2019},
  number                = {1037},
  month                 = nov,
  year                  = {2019},
  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.
                           \newline

                           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.}
}