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., \(\clubsuit \) and \(\heartsuit \) . 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. 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 run-minimal (i.e., the protocol has a run of minimal length) 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 its shortest run for protocols using this number of cards. (c) We extend our method to also handle the case of decks on symbols \(\clubsuit \) and \(\heartsuit \), where we show run-minimality for two AND protocols from the literature.
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Introduction
Card-based cryptographic protocols allow to perform secure multi-party computation (MPC), i.e., jointly computing a function while not revealing more information about each individual input than absolutely necessary, with just a (regular) deck of playing cards, as long as they have indistinguishable backs. Let us start with an example. Assume that Alice and Bob meet in a bar and spend the evening together. After quite some chat, they would like to find out whether to have a second date. They are faced with the following problem: in case only one of them likes to meet again, this would cause an uncomfortable embarrassment if he or she is the first to come out.1 Fortunately, Alice is a notable cryptographer and likes card games, so she has with her a standard deck of cards. She remembers the protocol by Niemi and Renvall [26] for computing the AND function of two bits, here for outputting “yes”, if both players share this mutual interest, and “no” otherwise. Using this MPC protocol hides the input of the respective other player unless it is obvious from their own input and output, hence hiding a “yes”-choice given of only one player, from the other.
To get a feeling for how such card-based protocols work, let us introduce the said protocol by Niemi and Renvall. The protocol uses five cards with distinguishable symbols, which we denote—for simplicity2—as
and
. It is essential that the cards’ backs are indistinguishable, such that when they are put face-down on the table, the only thing observable
. With these cards, the two players can encode a commitment to a bit (yes or no) by the order of two cards
, \(i,j\in \{1,\dots ,5\}\) (with \(i \ne j\)) via the encoding
Alice inputs her bit by putting the cards
face-down and in the respective order on the table (she puts
for input 0, and
for input 1), while Bob does the same using his cards
. We need an additional helper-card, here a
, which is put to the left of the two players’ cards.
Advertisement
The protocol starts by swapping Alice’s second card with Bob’s first card in the card sequence (pile) on the table. The resulting card configuration has an interesting property, namely that the order of the cards
and
in this sequence already encodes the output of the protocol, i.e., it reads
if the output is 1, and
otherwise. Hence, by securely removing the cards
and
(which is explained below), one directly obtains the output. We see this by inspecting all possible cases:
Bits
Input sequence
After swap
Removing
(0, 0)
(0, 1)
(1, 0)
(1, 1)
We can remove the cards
and
, while keeping the relative order of all cards in the sequence intact, by cutting the cards, i.e., rotating the sequence by a random offset which is unknown to the players. We can then securely turn the first card and remove it in case it is a
or a
. Due to the cut, the turned card is random and hence does not reveal anything about the inputs. When both cards are removed, we reach a configuration where
is the first card by the same procedure where the two remaining cards encode the AND result. Here, the
played the crucial role of a separator that keeps the relative order of the remaining cards—starting from the separator—intact, when doing a random cut. (A formal version of this protocol is given in Protocol 2 and Fig. 7.)
In this paper, we are interested in whether we can do away with the helping card
, and whether there are simpler protocols. Moreover, to handle the increasing combinatorial state space (relative to protocols on decks of just \(\clubsuit \) and \(\heartsuit \) ), we introduce formal verification to the field of card-based cryptography.
Secure Multiparty Computation with Cards
In combining different protocols, one can do much more than just computing the AND function. For example, it is possible to compute arbitrary Boolean circuits by combining the well-known fact that any circuit can be expressed using only NOT and AND gates, with a method to duplicate the physically encoded bit in case of forking wires, which we make explicit by a COPY gate. In the encoding above, NOT simply inverts the order of the two cards, and a COPY protocol is given, e.g., by Mizuki [18]. Using this setup, we can do general MPC for any function without needing to trust a possibly corrupted computer.
Advertisement
A particular advantage of protocols using physical assumptions is that they can provide a bridge to reality. Examples are given by Glaser, Barak and Goldston as well as Fisch, Freund and Naor, who give a protocol for proving in zero-knowledge that a nuclear warhead (to be disarmed due to an international treaty) conforms to a prescribed template, without giving away anything about its internal design [9, 11]. In our setting of cryptography with cards, this bridge is used if the cryptographic protocol is embedded in a real card game, e.g., to prevent cheating.3 Here, using computers is not only cumbersome, but there is no guarantee that the card sequence on a player’s hand is the one he or she or he inputs into the software, hence we have no bridge to the physical world.
Another application of such protocols is to explain MPC in an interesting and motivating way to students in cryptography lectures. Card-based cryptography tries to find protocols for the above-mentioned AND and COPY functionalities which are card-minimal, simple and practicable. For simplicity, many protocols in card-based cryptography work with specially constructed decks, e.g., of only the two symbols \(\clubsuit \) and \(\heartsuit \) . This is easy for an explanation and there are nice and easily describable protocols, such as the five-card trick by den Boer [5] and the six-card AND protocol by Mizuki and Sone [21].
However, the setting where all cards are distinguishable, as described above, has several advantages. First, we assume little about the indistinguishability of cards, which leads to stronger security guarantees. (This is closer to the indistinguishable version of tamper-evident seals, e.g., scratch-off cards, by Moran and Naor [22].) We only need the backs (or envelopes wrapping the cards, if one wishes) to be indistinguishable. Second, these standard decks are more commonly available, in contrast to constructed decks. If one were to use standard decks for the protocols above, they would need multiple copies of the same card. Third, this setting may lead to protocols using less cards than the optimal ones in the two-color deck setting. In fact, as our paper shows, one may use less cards than in the two-color deck setting. For example, our new four-card Las Vegas AND protocol presented in “Card-Minimal Protocols for AND” uses only a very basic, practicable shuffling mechanism, namely random cuts, and uses one card less than the provably card-minimal Las Vegas AND protocol (restricted to certain types of practical shuffles) in the two-color deck setting. As of yet, there has only been little research in this direction, with Niemi and Renvall, and Mizuki [18, 26] being the only works that consider the setting where all cards have distinguishable symbols, called “standard deck” setting. Nothing is known about non-trivial lower bounds on the number of cards, which is likely due to the large state space, as there are many more distinguishable card re-orderings compared to the two-color case.
Within this paper, our interest is to find an automatic way of constructing compact card-based protocols which are secure and correct, based on only the two standard operations turn and shuffle, given the desired number of cards. We exploit the observation that, to the best of our knowledge, all findings in the literature employ only protocols with runs of comparatively small length using only a small number of cards. Based on the hypothesis that we may always find some number n which is greater than or equal to any run-minimal card-protocol, we apply the automatic off-the-shelf formal program-verification technique software bounded model checking (SBMC) [3]. This technique allows, given such a bound n, to encode a program verification task into a decidable set of logical equations, which can then be solved by a SAT or an SMT solver. In this work, we propose an automatic method based on SBMC that, given the desired numbers of cards and protocol length, either constructs such a protocol if and only if one exists, or proves the underlying SAT formula to be unsatisfiable, i.e., shows that no such protocol exists. Based thereon, we propose that the cumbersome and error-prone task of finding such protocols or proving their non-existence by hand may be supported or complemented by such an automatic approach which is flexibly adaptable to a variety of card-based protocols and desired restrictions.
Prior to our work, it was not yet clear which role the input encoding plays when devising new protocols. This is the question on whether it can make a difference regarding the possibility of a protocol if we provide, e.g.,
to Alice and
to Bob, or
to Alice and
to Bob. We provide an analysis of this question, showing that with certain restrictions, there is a relatively large freedom in choosing the input (and/or output) bases. This is a useful prerequisite in proving the impossibility of a protocol with a given number of cards.
Contribution
Our contribution consists in providing interesting new protocols and impossibility results, as well as a fully automatic method based on formal verification to support such findings. The specific advances therein are the following (cf. also Table 1 for a comparison to the literature):
1.
A four-card AND protocol in the standard deck setting, improving upon the work by Niemi and Renvall [26] by one card, and reaching the theoretical minimum on the number of cards. W.r.t. shuffling, this protocol only uses an expected number of 6 random cuts, compared to 7.5 random cuts in a (shortened) variant of Niemi and Renvall [26]. Additionally, the protocol has a natural interpretation and the fact that it uses only random cuts makes it particularly easy to implement in an actively secure way [16].
2.
We show that under certain conditions the cards for encoding input or output can be chosen freely. For one-bit output protocols and if five or more cards are available, we can freely choose both input and output bases by only extending the protocol by expected three shuffles and three turn steps. For this matter, we identify two protocols for converting a bit encoding if the new encoding shares one card with the old one.
3.
We show that there is no finite-runtime protocol for converting between bases with non-empty intersection using four cards. Moreover, there cannot be a finite-runtime AND protocol with four cards if we fix the basis in advance.
4.
We introduce formal verification to card-based cryptography by providing a technique which automatically finds new protocols using as few as possible operations and searches for lowest bounds on card-minimal protocols.
5.
We extend this technique to more general decks and show two AND protocols in the two-color (or two-symbol) deck setting, i.e., where the deck constitutes a multiset of cards on symbols \(\clubsuit \) and \(\heartsuit \) , to be run-minimal. Finally, we employ our formal verification method to give a formal guarantee that we may safely reduce the maximal permutation set size and thereby optimize the running time for our protocol-finding technique in “Verification of run-minimality in two-color deck protocols”. This is due to the fact that in the two-color setting the number of possible sequences in a protocol state may be significantly smaller than the number of possible permutations on the deck.
Table 1
Minimum number of cards required by AND and basis conversion protocols, subject to the running time and shuffle restrictions specified in the first two columns
Note that random cuts are a subclass of uniform closed shuffles
\(^{\mathrm{a}}\)Lower bound result only holds for fixed output basis, flexible case is still open
Related Work
The feasibility of card-based cryptographic MPC is due to den Boer [5], Crépeau and Kilian [7], Niemi and Renvall [25], with a formal model given by Mizuki and Shizuya [19]. The only two papers looking at standard deck solutions are by Niemi and Renvall [26], Mizuki [18]. Lower bounds on card-based cryptographic protocols are given by Koch et al. [17], Kastner et al. [12] and Koch [14] for the two-color deck setting. The card-minimal protocol for this setting, using only practicable (i.e., uniform closed) shuffles, is given by Abe et al. [1] and uses five cards. The state trees used for protocols in this paper are devised by Koch et al. [17], Kastner et al. [12].
To the best of our knowledge, this is the first work which applies formal methods to the field of card-based cryptography. However, a large range of research has been done using formal methods in the more general field of secure two-party and multiparty computations. This can be clustered into either analyzing security protocols given as high-level, abstract (and usually idealized) models, or program-based approaches targeting real(istic) protocol (software) implementations. Avalle et al. [2] further structure this into the two main approaches of automated model extraction and automated code generation. We refer the interested reader to overviews as given by Blanchet [4] or Avalle et al. and only go into a few selected works for which we identified closer links to our approach, e.g., using software bounded model checking (SBMC), SAT solvers on real(istic) protocol implementations, or relating in the analyzed security model. Standard cryptographic assumptions using lower-level computational models are—albeit more realistic—usually harder to formalize and automate. One notable line of research is CBMC-GC [10] which builds on top of the tool CBMC [6]. It uses SBMC in a compiler framework translating secure computations of ANSI C programs into an optimized Boolean circuit which can subsequently be implemented securely utilizing the garbled circuit approach. Another similar setting to ours is analyzed by Rastogi et al. [27], who also assume an “honest-but-curious” attacker model. Therein, a domain-specific language is built on top of the \(\hbox {F}^{\star }\) language, a full-featured, verification-oriented, effectful programming language by Swamy et al. [29]. Swamy et al. then implement MPC programs with enabled formal verification provided by the semantics of the language.
Outline
We give the computational model of card-based protocols, security definitions, etc. and the necessary preliminaries as well as a basic setup for software bounded model checking in “Preliminaries”. “On the choice of cards for input and output” discusses which freedom one has when choosing the specific cards for encoding inputs and outputs to card-based protocols and introduces a formal relabeling operation. We give lower bounds on the number of cards for AND and basis-conversion protocols in “Impossibility of finite-runtime four-card AND and basis conversion with overlapping bases”. A four-card Las Vegas AND protocol and two basis-conversion protocols are presented in “Card-minimal protocols for AND” and “Card-minimal protocols for basis conversion with overlapping bases”, respectively. “An illustration of our verification methodology” gives results from applying our formal verification setup based on SBMC to our new AND protocol. In “Verification of run-minimality in two-color deck protocols” and “Verification of shuffle set size maximality”, we describe our new results for the two-color deck case.
Preliminaries
In this section, we first formally introduce card-based protocols with their computational model (including some basic required notions), a convenient formal protocol representation, a suitable security notion, and the formal requirements for proving lower bounds. Secondly, we introduce our applied formal technique called software bounded model checking, on which, thirdly, we establish our general technique for automatically finding card- and run-minimal protocols.
Card-Based Protocols
Formally, a deck\(\mathcal {D}\) of cards is a multiset over a (deck) alphabet or symbol set \(\varSigma \). We denote multisets by \({\llbracket }{\cdot }{\rrbracket }\), e.g., \({\llbracket }{\heartsuit , \heartsuit , \clubsuit , \clubsuit }{\rrbracket }\) is a deck over \(\{\heartsuit , \clubsuit \}\). In this paper, except for “Verification of run-minimality in two-color deck protocols” and “Verification of shuffle set size maximality”, we focus mainly on decks \(\mathcal {D}= {\llbracket }{1,\dots ,n}{\rrbracket }\), \(n\in {\mathbb {N}} \), where each symbol occurs exactly once. Following Mizuki [18], we call these decks standard decks, because decks of common card games are a good representation of such formal decks.
A card that is lying on a table (as usual in card-based protocols) can have two orientations, namely face-up (showing the symbol of the card), or face-down. A special back symbol ‘?’ that is not part of \(\varSigma \) represents what is visible about a card that is turned face-down. In this way, we can describe a card lying on the table by a fraction symbol \(\frac{a}{b}\), where exactly one of a and b is ‘?’, and the other is a symbol from \(\varSigma \). Here, a represents a part that is visible from the card when it lies down, and hence \(\frac{a}{b}\) is a face-down card if \(a = \mathord {?}\), and a face-up card if \(a\in \varSigma \). As card-based protocols usually involve some turning-over of the cards, this status will likely change during a protocol, causing the numerator and denominator to be swapped.
Card-based protocols then proceed on sequences of such cards \((\alpha _1, \dotsc , \alpha _{{|}{\mathcal {D}}{|}})\) where all cards from the deck \(\mathcal {D}\) are lying on the table as just described and in the given order. The visible sequence of such a sequence then arises by just taking the “visible” numerator of all cards. For example, if the sequence is \((\frac{\mathord {?}}{\heartsuit }, \frac{\mathord {?}}{\heartsuit }, \frac{\clubsuit }{\mathord {?}}, \frac{\mathord {?}}{\clubsuit })\), the corresponding visible sequence of the cards is \((\mathord {?},\mathord {?},\clubsuit ,\mathord {?})\). The sequence trace of a finite protocol run, and analogously its visible sequence trace, is then the sequence of all card sequences and visible sequences, respectively, as they arise during the run. Let \({\textsf {Seq}}^{\mathcal {D}}\) denote the set of sequences on deck \(\mathcal {D}\).
In the following, we will often just use the symbol sequence that contains only the card symbols (\((\heartsuit ,\heartsuit ,\clubsuit ,\clubsuit )\) in the example above) as a shorthand for the corresponding face-down cards. This is due to Kastner et al. ([12], Cor. 2 and Lem. 4), who showed that it does not increase the computational power of card-based protocols to leave cards face-up longer than necessary, and that one can safely assume that any face-down cards that are turned over during a step in the protocol are directly turned back after learning its symbol.
For encoding a bit, we additionally assume a linear order on the card symbols in \(\varSigma \), which is the usual order on \({\mathbb {N}} \) for standard decks, and \(\clubsuit < \heartsuit \) for simple two-element decks. Two face-down cards with distinct symbols \(s_1,s_2\in \varSigma \) then encode a bit via the following encoding rule introduced by Niemi and Renvall [26]:
Card-based protocols proceed by mainly two actions on the sequence or pile of cards: We can introduce uncertainty (about which card is which) by shuffling them in arbitrary or in certain controlled ways, e.g., by cutting the cards in quick succession, so that players do not know which card ended up wherein the card sequence (or pile). Slightly more formal, a (uniform) shuffle is specified by a permutation set, from which one element is drawn uniformly at random and applied to the cards, without the players learning which one it was. Secondly, we may turn over cards and publicly learn their symbol, and act on the basis of this information. Moreover, we may deterministically permute the cards.
A protocol computes a Boolean function \(f:\{0,1\}^2 \rightarrow \{0,1\}\) if the possible start sequences, corresponding to the player inputs \(b\in \{0,1\}^2\), do encode these inputs as described above, and that the cards that are declared to contain the output value upon termination of the protocol, do encode the output value \(o=f(b)\) for each respective input \(b\in \{0,1\}^2\) as described above. A more formal definition in terms of the tree representation introduced in “Computational model and protocol state tree representation” is given at the end of that section.
Permutations and Groups
Let \(S_n\) denote the symmetric group on \(\{1,\dots ,n\}\). For elements \(x_1,\dots ,x_k\in \{1,\dots ,n\}\) the cycle\((x_1 \;x_2\;\dots \;x_k)\) is the cyclic permutation \(\pi \) with \(\pi (x_i) = x_{i+1}\) for \(1 \le i < k\), \(\pi (x_k) = x_1\) and \(\pi (x) = x\) for all x not occurring in the cycle. Every permutation can be written as a composition of pairwise disjoint cycles. For example, \((1\;3\;2)(4\;5)\) maps , and . The identity permutation is denoted as \({\textsf {id}}\).
Given permutations \(\pi _1,\dots ,\pi _k\in S_n\), \(\langle \pi _1,\dots ,\pi _k\rangle \) denotes the group generated by \(\pi _1,\dots ,\pi _k\). A shuffle is a random cut if its permutation set is the group \(\langle \pi \rangle = \{\pi ^0,\dots ,\pi ^{l-1}\}\) generated by a single element \(\pi \)which is a cycle\((x_1\;x_2\;\dots \;x_l)\). A shuffle is called a random bisection cut if its permutation set is generated by a \(\pi \) which is the composition of pairwise disjoint cycles of length 2. Finally, an \(S_k\)-shuffle is a shuffle with permutation set \(S_k\).
Computational Model and Protocol State Tree Representation
For our formal descriptions, we make heavy use of the KWH trees introduced by Koch et al. [17] and shown to be equivalent to the computational model by Mizuki and Shizuya [19, 20] in the work by Kastner et al. [12]. For this matter, let us first describe what a state during a run of card-based protocols is. We start by an example, namely the state of a protocol in the very beginning, i.e., after the players have put their cards encoding their inputs on the table:
×
As mentioned above, we resort to only write symbol sequences instead of full card sequences. Each line in the state as depicted by the above boxed information rows describes a card sequence that is possible at this point in time in the protocol, together with a certain type of polynomial in the variables \(X_{00}, X_{01}, X_{10}, X_{11}\). For example, the first line of the state can be read as “the sequence \((\frac{\mathord {?}}{1},\frac{\mathord {?}}{2},\frac{\mathord {?}}{3},\frac{\mathord {?}}{4})\) lies at the table with the symbolic probability \(X_{00}\)”, i.e., with the probability that (0, 0) is the input of the protocol (which is left as a variable, instead of a concrete value, as the input distribution can be arbitrary). Note that 12, and 34 encode 0 as required for input (0, 0) and that the order of the rows is of no significance in the above depiction. We capture the notion of a state more formally in the following definition:
Definition 2.1
(State) Let \(\mathcal {D}\) be a deck of a protocol \(\mathcal {P}\) computing a Boolean function \(f:\{0,1\}^2 \rightarrow \{0,1\}\). A state\(\mu \) of \(\mathcal {P}\) is a map \(\mu :{\textsf {Seq}}^{\mathcal {D}}\rightarrow \mathbb {X}_2\), where \(\mathbb {X}_2\) denotes the polynomials over the variables \(X_b\) for \(b\in \{0,1\}^2\) of the form \(\sum _{b\in \{0,1\}^2} \beta _b X_b\), for \(\beta _b\in [0,1]\subset \mathbb {R}\), and \(\mu (s)\) for \(s\in {\textsf {Seq}}^{\mathcal {D}}\) is interpreted as the probability that s is the actual sequence on the table, in terms of the symbolic probabilities on the inputs.
Defined this way, the boxes drawn throughout the paper are just depictions of such a (state) map, i.e., we just write down all sequences \(s\in {\textsf {Seq}}^{\mathcal {D}}\) that are not assigned probability 0, and annotate it to their right with the polynomial \(\mu (s)\). (An alternative characterization of a state is given by Koch ([13], Def. 7.1).)
Every standard-deck protocol starts by a state as above:
×
but we eventually add further cards (
, ...) if the deck is larger to the right of the players bits. The state (or KWH) tree of a protocol is then a directed tree where the nodes are states as above, with annotations at the outgoing edges of each state, specifying the action that is performed next. Let \(\mu \) be the state with the outgoing annotation, then the possible actions are defined as:
1.
\((\textsf {shuffle}, \varPi )\) leads to a \(\mu '\) as in Fig. 1, where \(\varPi \subseteq S_{{|}{\mathcal {D}}{|}}\) is a permutation set.
2.
\((\textsf {turn}, T)\) branches the tree into states \(\mu _v\) for each observation \(v\) possible by revealing the cards at positions from the set \(T\subseteq \{1,\dotsc , {|}{\mathcal {D}}{|}\}\), as in Fig. 2. \(\mu _v\) contains the sequences from \(\mu \) which are compatible with the observation \(v\). For each sequence \(s\) compatible with \(v\), we have \(\mu _v(s) :=\mu (s)/\Pr [v]\), where \(\Pr [v]\in (0,1]\) is the probability of observing \(v\). Note that we omit the implicit operation to turn the card back face-down, as motivated above.
3.
\((\textsf {perm}, \pi )\) permutes the sequences of \(\mu \) according to \(\pi \).
4.
\((\textsf {result}, p_1, p_2)\) stops the computation and returns the cards at \(p_1, p_2\) as output.
Fig. 1
A shuffle operation, given by example (left), and via the general rule (right)
Fig. 2
A turn operation. Here, \(v_1,\dots ,v_n\), are the possible observation by turning the cards at positions in T. For each \(i\in \{1,\dots ,n\}\) the \(s_{i,1},\dots ,s_{i,\ell _i}\) are the sequences from \(s_1,\dots ,s_{\ell }\) which are compatible with \(v_i\). Note that in secure protocols, the probability of observing \(v_i\), denoted as \(\Pr [v_i]\), is constant
×
×
A protocol computes a Boolean function \(f:\{0,1\}^2 \rightarrow \{0,1\}\) if the start state (tree root) encodes each \(b\in \{0,1\}^2\) in the first four cards (the remaining cards being at fixed positions), and in the leaf nodes of the protocol’s state tree, it holds for the positions given by the result operation that the cards at these positions encode a value \(o\in \{0,1\}\) if all \(X_i\) occurring in \(\mu (s)\) for sequence \(s\) satisfy \(f(i)=o\) (Correctness).
We say that a protocol has finite runtime if its tree is finite. It is a Las Vegas protocol, if it is not finite runtime, but the expected length of any path in its tree, i.e., the expected value of the length of an arbitrary descending path in the tree starting from the root (as a random variable, where the randomness is in the choice of the path), is finite. Note that while we consider looping protocols, we do not consider the case where a complete restart is necessary. For self-similar infinite trees, we simplify by drawing edges to earlier states.
Security of Card-Based Protocols
We slightly adjust the security notion from the literature to standard decks. For more details, we refer to Koch [13]. Since different encodings for the same bit are possible, we want the encoding basis of the output bit to not give away anything about the inputs. We say that a protocol is secure if at any turn operation the probability for each observation \(v\) is a constant \(\rho \in [0,1]\) (using \(\sum _{i\in \{0,1\}^2}X_i\) = 1), and additionally if at any result operation the probability of each output basis is constant in the same sense.
Similar to the work by Kastner et al. [12], for our impossibility proofs and formalizations with bounded model checkers, it is also useful to consider a weaker form of security, which is a necessary criterion for security as defined above: a protocol is possibilistically output-secure, if at any state of the protocol, every output can still be possible. This weakens the normal security guarantee, as the probability for a given input sequence could be higher in this state. One could even be able to exclude a specific input sequence, if the corresponding output can still be possible through another input sequence. Together with possibilistic input-security, this discussion leads to the following formal definition:
Definition 2.2
(cf. Kastner et al. [12]) A protocol \(\mathcal {P}=(\mathcal {D}, U, Q, A)\) computing a function \(f:\{0,1\}^2 \rightarrow \{0,1\}\) has possibilistic input security (possibilistic output security) if it is correct, i.e., the probability of the output being \(O = f(I)\) is 1, and for uniformly4 random input I and any visible sequence trace v with \(\Pr [v] > 0\) as well as any input \(i \in \{0,1\}^2\) (any output \(o \in \{0,1\}\)) we have \(\hbox {Pr}[{v}|{I = i}] > 0\) (\(\hbox {Pr}[{v}|{f(I) = o}]>0\)).
Proving Lower Bounds
Let us begin by defining an equivalence relation on the states that helps to greatly reduce the complexity of impossibility proofs by identifying states that are only a permuted version of each other:
Definition 2.3
(Similarity) We call two states, or analogously two reduced states as defined next, \(\mu \) and \(\mu '\)similar, if there is a permutation \(\pi \) such that applying \((\textsf {perm}, \pi )\) to \(\mu \) gives rise to \(\mu '\). For notation, let \(\left\langle \mu \right\rangle _{\sim }\) be the equivalence class of \(\mu \) up to similarity, i.e., the set of all states that are permuted versions of \(\mu \) as defined by similarity.
In other words, \(\mu \) is similar to \(\mu '\) if it is equal to \(\mu '\) up to column permutation on the sequences part of the state depiction.
As in the work by Kastner et al. ([12], Definition 3), we define reduced states, where states are not annotated by their symbolic probabilities, but by the result that is specified by their inputs—a formal definition follows below. This simplifies impossibility proofs by reducing information and the state space. Any such reduced tree captures only a weak form of security, possibilistic security, as discussed above where each output (reachable in principle) needs to be still possible. Showing that a protocol is impossible even in this weak setting implies its general impossibility.
To obtain a reduced state tree, we project all the symbolic probabilities of the sequences of all states in a state tree to a type (representing the possible future output associated with the sequence in a correct protocol, see below), which can be any \(o\in \{0,1\}\). For this, let \(\mathcal {P}\) be a protocol computing a function \(f:\{0,1\}^2 \rightarrow \{0,1\}\) and \(\mu \) be a state in the state tree. For any sequence \(s\) with \(\mu (s)\) being a polynomial with positive coefficients for the variables \(X_{b_1},\dots ,X_{b_i}\) (\(i \ge 1\)), set \(\hat{\mu }(s) :=o \in \{0,1\}\) if \(o = f(b_1) = f(b_2) = \dots = f(b_i)\) in the resulting reduced state\(\hat{\mu }\). We call sequences in \(\hat{\mu }\) according to their type o-sequences. Moreover, we introduce the additional type\(\bot \) for sequences s where \(\mu (s)\) does have positive coefficients for variables representing input that would map to different output, as in \(X_{00}+X_{11}\) when \(f(0,0) \ne f(1,1)\).5
Definition 2.4
(Reduced state) Let \(\mathcal {P}\) be a protocol computing a Boolean function \(f:\{0,1\}^2 \rightarrow \{0,1\}\) with deck \(\mathcal {D}\). Then a reduced state\(\hat{\mu }\) of \(\mathcal {P}\) is a map \(\hat{\mu }:{\textsf {Seq}}^{\mathcal {D}}\rightarrow \{0,1,\bot \}\) which maps a sequence \(s\in {\textsf {Seq}}^{\mathcal {D}}\) to its type (as defined above).
If \(\mu \) is a (non-reduced) state of \(\mathcal {P}\), we can map it to its reduced state as follows: The reduced state\(\hat{\mu }\) of \(\mathcal {P}\)arising from\(\mu \) is defined via \(\hat{\mu }(s) :=t_s\), where \(t_s\) is the type of \(\mu (s)\). Note that it is always possible to map a state to its reduced version.
As an example, let us look at the tree excerpt on the left of Fig. 1, and its reduced version (here, shown on the right), when assuming it is part of a protocol computing AND:
×
For example, the annotation of 1234 in the first state, \(X_{00} + X_{01}\), is mapped to its type 0, as it only contains variables representing inputs (namely (0, 0) and (0, 1)) that result in output 0. Note that by using reduced states, we bring the state space from the countably infinite to the finite, which is a necessary step for the impossibility proofs, albeit using it only allows us to show impossibility to the weaker notion of possibilistic security (which nevertheless is a necessary condition for full security, hence the even stronger impossibility claim).
A reduced state is turnable at position\(i\in \{1,\dotsc ,{|}{\mathcal {D}}{|}\}\), if for each symbol \(c\in \varSigma \), there is, among the sequences s with symbol c at position i, an r-sequence for each \(r\in \{0,1\}\) in the image of the function computed by the protocol, and/or a \(\bot \)-sequence. This essentially means that after the turn at i all outputs are still possible, capturing the notion of output-possibilistic security. The reduced state is turnable if it is turnable at a position \(i\in \{1,\dotsc ,{|}{\mathcal {D}}{|}\}\).
For proving impossibility results, we make use of the backwards calculus as given by Koch [14]. We highlight the main ideas here but refer to it for details.
Definition 2.5
(Backwards shuffle) Let \(\mathcal {G}\) be a non-empty set of reduced states of a protocol \(\mathcal {P}\). Then \(\textsf {shuf}^{-1}_{}(\mathcal {G})\) is the set of reduced states \(\mu '\) of \(\mathcal {P}\) such that there is a permutation set \(\varPi \) (containing \({\textsf {id}}\), and dependent on \(\mu '\)) such that \((\textsf {shuffle}, \varPi )\) applied to \(\mu '\) results in a reduced state in \(\mathcal {G}\). In other words, \(\textsf {shuf}^{-1}_{}(\mathcal {G})\) is the set of states that are transformed into a state in \(\mathcal {G}\) by a shuffle. Note that the trivial shuffle is allowed, i.e., \(\mathcal {G}\subseteq \textsf {shuf}^{-1}_{}(\mathcal {G})\).
For example, if \(\mathcal {G}\) would consist of just one state, \(\mu \), where \(o_1,\dotsc ,o_4\) are distinct symbols6:
×
then \(\textsf {shuf}^{-1}_{}(\mathcal {G})\) would contain exactly the following eight states:
×
To see this, observe that the first one is just \(\mu \), which is contained by definition, as the trivial shuffle \((\textsf {shuffle}, \{{\textsf {id}}\})\) will map it to itself. Moreover, all the other states in this list result in \(\mu \) by the \((\textsf {shuffle}, \{{\textsf {id}}, (3\;4)\})\). The above list is exhaustive as we cannot generate a 0-sequence or a 1-sequence via a shuffle if it was not already present in the state on which the shuffle was applied. (Note that in the generation of this list we make use of the assumption that \({\textsf {id}}\) is always contained in a shuffle, which is the case for closed shuffles anyway, but w.l.o.g. otherwise also, as in the case that \({\textsf {id}}\) would not be contained, we could replace the shuffle by a conjugated version that is pre-/postfixed by a corresponding deterministic \(\textsf {perm}\) operation, cf. Kastner et al. [12].)
Definition 2.6
(Backwards turn) Let \(\mathcal {G}\) be a non-empty set of reduced states of a protocol \(\mathcal {P}\). Then, \(\textsf {turn}^{-1}_{\text{ f }}(\mathcal {G})\) is the set of reduced states \(\mu '\) of \(\mathcal {P}\), such that \(\mu '\in \mathcal {G}\), or that there is a position \(i\in \{1,\dotsc ,{|}{\mathcal {D}}{|}\}\) such that \((\textsf {turn}, \{i\})\) applied to \(\mu '\) results in reduced states that are contained in \(\mathcal {G}\). In other words, it is the set of states being in \(\mathcal {G}\), or having a turnable position \(i\) such that all immediate successor states from a turn at \(i\) are in \(\mathcal {G}\).
For example, if \(\mathcal {G}\) would consist of three reduced states \(\mu _1,\dotsc ,\mu _3\), which each have a constant column at the fourth position:
×
Then \(\textsf {turn}^{-1}_{\text{ f }}(\mathcal {G})\) would contain, in addition to the states in \(\mathcal {G}\), exactly the following four reduced states:
×
Here, first observe that the first state is just a combination of all three states, whereas the second, third and fourth is a combination of \(\mu _1\) and \(\mu _2\), of \(\mu _1\) and \(\mu _3\) and of \(\mu _2\) and \(\mu _3\), respectively. When forming the “backwards turn” set, we can just combine states with a constant column of distinct symbols into one, as a turn at the position where these individual states had a constant column branches/gives rise to exactly these individual states.
We call \(\textsf {turn}^{-1}_{\text{ f }}(\cdot )\) and \(\textsf {shuf}^{-1}_{}(\cdot )\)backwards turn and backwards shuffle. Define by \(\textsf {cl}_{\text{ f }}(\mathcal {G})\)the closure of \(\textsf {turn}^{-1}_{\text{ f }}(\cdot )\) and \(\textsf {shuf}^{-1}_{}(\cdot )\) operations on \(\mathcal {G}\). Note here, that if a finite-runtime protocol exists for a given start state, then there exists a sequence of shuffle/turn operations which, applied to the start state, will result in a final state. Therefore if we assume \(\mathcal {G}\) to be the set of all possible final states for a deck \(\mathcal {D}\), then it holds that if the start state is not in \(\textsf {cl}_{\text{ f }}(\mathcal {G})\), then no finite-runtime protocol for \(\mathcal {D}\) can exist.
Automatic Formal Verification Using SBMC
In the following, we introduce an automatic technique from formal program verification, namely software bounded model checking (SBMC), to the field of card-based cryptography. We first describe the general technique of using SBMC to check for software properties, before we explain how we apply it to search for cryptographically secure card-based protocols. In a nutshell, we translate the task to a reachability problem in software programs (which will later-on be a program encoding operations on an abstract state tree as described above), which the SBMC tool encodes into an instance of the SAT problem.
We assume we are given an imperatively defined function f under the form of an imperative program (for example, written in the C language), that uses some parameter values taken among a set of possible start values I. An entry \(i \in I\) is a list of values, one value for each such parameter: it gives a value to everything that a run of f depends on, such as its input variables, or anything that is considered non-deterministic (i.e., of arbitrary, but fixed, value for any concrete evaluation of f) from the point of view of f. For this reason, those parameters are qualified as “non-deterministic”, to distinguish them from normal parameters used in a programming language to pass information around. Moreover, some values can be “derived”, thus, computed in f from the non-deterministic parameter values, or declared as constants in f, and both values of non-deterministic parameters or derived values can then be used as normal parameters in the program. We are also given a software property to be checked about f, in the form \(C^\text {ant}\Rightarrow C^\text {cons}\), where ant and cons stand for antecedent and consequence respectively. Both \(C^\text {ant}\) and \(C^\text {cons}\) are sets of Boolean statements. A Boolean statement is a statement of f that evaluates to a Boolean value, for example, a simple statement checking that some computed intermediate value is positive. An entry i is said to satisfy a set of Boolean statements if and only if all Boolean statements in the set evaluate to true during the execution of f using the non-deterministic parameter values i, and is said to fail the set of Boolean statements otherwise. The property \(C^\text {ant}\Rightarrow C^\text {cons}\) requires that for all possible entries \(i \in I\), ifi satisfies \(C^\text {ant}\), theni satisfies \(C^\text {cons}\). As an example, assume f computes, given i, two intermediate integer values \(v_1\) and \(v_2\), and then returns a third value \(v_3\). The property to be checked could, e.g., be: if\(v_1\) is negative, then\(v_2\) is positive and \(v_3\) is odd. A solver that is asked to check a software property \(C^\text {ant}\Rightarrow C^\text {cons}\) thus exhaustively searches for an entry i that satisfies \(C^\text {ant}\) but fails \(C^\text {cons}\). The property is valid if and only if there does not exist any such entry i, i.e., it is impossible to find.
SBMC is a fully-automatic static program analysis technique used to verify whether such a software property is valid, given a function and a property to be checked. It covers all possible inputs within a specified bound. It is static in the sense that programs are analyzed without executing them on concrete values or considering any side channels. Instead, programs are symbolically executed and exhaustively checked for errors up to a certain bound, restricting the number of loop iterations to limit runs through the program to a bounded length. This is done by unrolling the control flow graph of the program and translating it into a formula in a decidable logic that is satisfiable if and only if a program run exists which satisfies \(C^\text {ant}\) and fails \(C^\text {cons}\). The variables in the formula are the non-deterministic parameters of f, and their possible values are taken from I.
This reduces the problem to a decidable satisfiability problem. Modern SAT-solving technology can then be used to verify whether such a program run exists, in which case an erroneous input has been found, and the run is presented to the user. If the solver cannot find such a program run, it may be either because the property is valid, or because it is invalid only for some run which exceeds the bound. In some cases, SBMC is also able to infer statically which bound is sufficient to bring a definitive conclusion.
Automatic Formal Verification for Card-Based Protocols
Our approach employs a standardized program representation of the KWH trees introduced by Koch et al. [17] (and described in the beginning of this section). This allows a general programmatic encoding of both shuffle and turn operations, as well as of the fixed input state (indicated by the input card sequences from the table in the very beginning of this paper), the non-deterministic reachable states, and the logical function to be computed securely.
The input state is trivially derived from the specified numbers of cards as the size and order of the players’ commitments is fixed and the (without loss of generality) consecutively ordered card sequence of (distinguishable) helper-cards is simply prepended to the input card sequence, annotated with their respective input probabilities. Any input state thus consists of exactly four distinguishable card sequences. Based on this input state, the program performs a loop, which successively performs turn or shuffle operations based on the input state and computes the resulting states from which it continues performing turn or shuffle operations. The loop ends when the specified bound (representing the length of the protocol to be found) is reached, checks whether the final state is indeed a valid computation of the secure function, and (if and only if the check is successful) the found protocol is then presented to the user.
However, this task involves multiple computational complexities, most notably both the number of (possibly) reachable states, and the choice of the next operation, i.e., either choosing the card(s) to be turned or which shuffle to perform. We partially overcome the first computational complexity by not considering Las Vegas protocols as this relieves us from checking every reachable sequence of states to be finite. In fact, we compute all reachable states after every protocol operation, but only check each of them to be valid, and then proceed our operations on only one of them, which is non-deterministically chosen among them. The second computational complexity consists in first non-deterministically choosing whether to shuffle or to turn, and then to perform the respective operation. The turn operation is less interesting as it is mostly the obvious implementation for updating the computed state and its probabilities using mostly standard imperative program operations, except that the turn observations are again non-deterministically chosen, hence making the SBMC tool consider any of them to be possible. The more interesting operation is the shuffle operation, as it must randomly draw a set of permutations on which the thereby reachable states are computed. We implement this by non-deterministically choosing a set of permutations from a precomputed set of all generally possible permutations. Both the amount and the choices of the respective permutations are chosen non-deterministically. Moreover, we have the ability to restrict our experiments to only closed shuffles, and can even bound the shuffle set size to keep the running time of the verification time acceptable, if needed (albeit possibly reducing the strength of the results, cf. “Verification of shuffle set size maximality”). For example, in our analysis of the run-minimality of Protocol 1, we bounded the permitted size of the permutation sets by the (arguably quite reasonable) number 8, in order to keep the execution times still manageable for our experiments. Note that our technique from “Verification of shuffle set size maximality” shows that only a bound of 12 would be really safe to assume, leaving a small gap in the argumentation as we superficially exclude exactly the possible 12-element alternating groups \(A_4\) as shuffles steps from the possible protocol candidates, when showing that no shorter protocol can exist. We leave it for future work to tweak the code such that the looser bound of 12 is within reach with our technique.
Finally, after iterating the afore-mentioned loop for the specified bound number with the described operations and restricting that final state indeed computes the secure function, we specify the software property \(C^\text {cons}\) to be checked simply as the Boolean value false. This trivially unsatisfiable property implies that the verification task always fails once there exist input and non-deterministic parameters such that the respective program run reaches the statement in the program which checks this property. The SBMC tool exhaustively searches for a run of the specified length through the program which leads from the starting state to a correct and secure state which satisfies the given security notion, i.e., reaches the above-metioned statement. Hence, if there exists any protocol of the specified length which computes the secure function and for which the specified operations and valid intermediate states (representing KWH-trees) exist, such a protocol is presented by our method. If no such protocol can be found, we know there is no card-based protocol of the specified length satisfying all our restrictions on permitted turn and shuffle operations, as well as intermediate and final states. This means there exists no model for the SAT formula which encodes the set of all permitted program runs given our specified requirements.
Hence, assuming our translation of KWH trees and respective protocol operations into a simple imperative program are correct, this method can then be used in an iterative manner to strengthen the bounds from the literature. Note that this is largely based on the so-called “small-scope hypothesis”, i.e., a large number of bugs are already exposed to small program runs. We apply this hypothesis to the setting of card-based security protocols as all protocols in the literature only use a small number of turn and shuffle operations and the length of any found protocol is below ten operations.
This approach can be generalized to search for card-based protocols using a pre-defined number of actions and adhering to a given formal security notion. We have written a general program7 to search for such situations parameterized in the desired restrictions on actions and security notions. Note that, to cope with the still considerable state space size, we use the refined security notion of output-possibilistic security.
On the Choice of Cards for Input and Output
We essentially show that the choice of input basis (or output basis, but not necessarily both) is irrelevant for the functioning of the protocol. In rare cases, one has to append two operations to existing protocols to make them fully basis flexible. In the Niemi–Renvall protocol shown above, the protocol description specifies Alice’s cards to be of symbols \(1, 2\), and Bob’s to be of symbols \(3, 4\) and the helping card to be a \(5\). To simplify later proofs and to demonstrate an interesting symmetry in card-based protocols, we show that this choice is irrelevant for the functioning of the protocol.
For this, we define a relabeling from deck alphabet \(\varSigma \) to a deck alphabet \(\varSigma '\), i.e., a bijective function \(\lambda :\varSigma \rightarrow \varSigma '\).8 A relabeling of a sequence \(s=(s_1,\dots ,s_n)\) is a relabeling of each of its symbols, i.e., \(\lambda (s) := (\lambda (s_1),\dots ,\lambda (s_n))\). A relabeling of a state is given by the relabeling of all its sequences, a relabeling of a protocol/state (sub)tree is the relabeling of all its states as described by Figs. 3 and 5.
Fig. 3
Example of the relabel action, swapping the card symbols of 1 and 3, and of 2 and 4, respectively. This action is for abbreviated writing only, it does not actually relabel the physical cards, which seems impossible without learning their symbols. Hence, the tree on the left is virtually translated to the right. Note that the relabeling only affects the sequences, the observations at edges belonging to turn actions and may swap the order of the indices in result operations
Fig. 4
Example of making the basis deterministic, cf. Lemma 3.2. On the left, you can see a tree part with one-bit output and randomized basis, i.e., the output basis may be \(\{1,2\}\) or \(\{3,4\}\), each with a probability of . We can make it known to the players, i.e., deterministic, by splitting up the state via an \(S_k\)-shuffle (here: \(k=2\)) on the remaining cards (so that they no longer contain any information), turning these and then doing the result operation. By what is visible in the turn, one can derive the output basis
Fig. 5
The formal rule for relabeling leaf nodes of one-bit output protocols. Let \(r_1=s_k[i], r_2=s_k[j]\in \mathcal {D}\) be the output symbols (before relabeling) of some arbitrary sequence \(s_k\) of \(\mu \). Then, \(\tau ={\textsf {id}}\), if \(r_1 < r_2\) implies \(\lambda (r_1) < \lambda (r_2)\) (\(\lambda \) is monotone on \(r_1\), \(r_2\)) and \(\tau =(i\;j)\) otherwise
×
×
×
Lemma 3.1
If \(\mathcal {P}\) is a protocol with deterministic output basis, one can relabel the cards without affecting the functioning.
Note that the deterministic output basis restriction is important, because if we have a randomized output encoding such as in Fig. 4 on the left, a relabeling might affect the monotonicity of the encoding of only one of the possible output bases. In this case, we make use of the following lemma, as illustrated in Fig. 4.
Lemma 3.2
Every protocol with one-bit output and a randomized output basis can be transformed into a protocol with deterministic output basis, by inserting a shuffle and a turn before any result operation with randomized output basis.
Impossibility of Finite-Runtime Four-Card AND and Basis Conversion with Overlapping Bases
In this section, we give our main impossibility results.
Theorem 4.1
There is no four-card finite-runtime basis conversion protocol for overlapping bases with deck \(\mathcal {D}={\llbracket }{1,2,3,4}{\rrbracket }\).
Proof
We proceed using the backwards calculus technique by Koch [14], as described in “Proving lower bounds”. That is, we start with the set of final states \(\mathcal {G}\) of basis conversion protocols. Then, we iteratively build a (possibly) larger set by adding states which reach the states of the current set by a shuffle or a turn, in order to obtain the closure \(\textsf {cl}_{\text{ f }}(\mathcal {G})\). As we consider only reduced states (cf. “Proving lower bounds”), the set of possible states is finite, hence, applying \(\textsf {turn}^{-1}_{\text{ f }}(\cdot )\) and \(\textsf {shuf}^{-1}_{}(\cdot )\) operations to the (growing) set of states, starting from \(\mathcal {G}\), will become stationary. Finally, it remains to be shown that the start state is not contained in the derived closure.
We assume w.l.o.g.9 the input basis \(\{1,2\}\) with helping cards 3 and 4, and the output basis \(\{o_1 < o_2\} \subset \{1,2,3,4\}\). For the basis conversion impossibility, we will require \(|\{1,2\} \cap \{o_1, o_2\}|=1\) (which we call basis intersection requirement in the following). However, whether we use this requirement or not, the closure \(\textsf {cl}_{\text{ f }}(\mathcal {G})\) remains the same.10 Hence, we will use this requirement only in the last step of the proof when we show that the start state is not in \(\textsf {cl}_{\text{ f }}(\mathcal {G})\), and reuse the closure for the AND protocol impossibility proof in Theorem 4.2.
After setting the stage, we start by describing the set \(\mathcal {G}_0\) from which we will derive the closure \(\textsf {cl}_{\text{ f }}(\mathcal {G}_0)\) according to the backwards calculus technique described above. Let \(o_3 < o_4\) be the remaining two symbols, i.e., \(\{o_3,o_4\}= \{1,2,3,4\}{\setminus } \{o_1,o_2\}\). Thus, the final state is (up to similarity11) any choice of at least one 1-sequence and one 0-sequence of the states on the left set12:
×
The state set on the right contains the template for final states with output basis \(\{o_3 < o_4\}\), which we will include in the starting set \(\mathcal {G}_0\), as they are reachable from final states with output basis \(\{o_1,o_2\}\) by the backwards calculus anyway, due to the existence of the disjoint basis conversion protocol by Mizuki [18] (again, with any choice of at least one 1- and one 0-sequence). As long as we can still show that the start state is not in \(\textsf {cl}_{\text{ f }}(\mathcal {G}_0)\), it is okay to enlarge \(\mathcal {G}_0\), since our claim is only made stronger (using the monotonicity property of the backwards operations \(\textsf {turn}^{-1}_{\text{ f }}(\cdot )\) and \(\textsf {shuf}^{-1}_{}(\cdot )\)).
We have \(\textsf {shuf}^{-1}_{}(\mathcal {G}_0) = \mathcal {G}_0\), because any subset of a state from \(\mathcal {G}_0\) which contains at least one 1-sequence and one 0-sequence (which is required as otherwise 1-/0-sequences cannot be generated out of thin air by a shuffle) is already in \(\mathcal {G}_0\). Hence, we consider \(\mathcal {G}_1 := \textsf {turn}^{-1}_{\text{ f }}(\mathcal {G}_0)\), i.e., the states which are turnable at a position i, where all immediate child nodes after turning at i are in \(\mathcal {G}_0\). W.l.o.g.13 we fix the turn to be at position 4. Following Koch ([14], Lemma 3), we use that \(\mathcal {G}_1 = \textsf {turn}^{-1}_{\text{ f }}(\mathcal {G}_0) = \mathcal {G}_0 \mathop {\cup } \textsf {turn}^{-1}_{\text{ f }}(\textsf {cc}(\mathcal {G}_0))\) holds, where \(\textsf {cc}(\mathcal {G}_0)\) is the set of states in \(\mathcal {G}_0\) that have a constant column, i.e., the union of these four equivalence classes up to similarity:
×
The states from \(\mathcal {G}_1{\setminus } \mathcal {G}_0\) look as follows:
×
where at least two of the four (two-sequence) blocks are present, and \(a,b,c,d\in \mathcal {D}\) are pairwise distinct. We show that a further backwards turn does not enlarge the set by showing \(\textsf {cc}(\mathcal {G}_1) = \textsf {cc}(\mathcal {G}_0)\). For this, note that the states from \(\textsf {cc}(\mathcal {G}_0)\) (i.e., the blocks, considered in isolation) have exactly two constant columns, but with the specific pairing that if one of the constant columns consists of \(o_1\), the other one consists of \(o_2\) and vice versa, or if one consists of \(o_3\), the other one consists of \(o_4\) and vice versa.
Using this structure, we can deduce that states from \(\mathcal {G}_1{\setminus }\mathcal {G}_0\)with a constant column, say w.l.o.g.14 at position 3, have the respective paired symbol (of the \(o_1\)-\(o_2\) or \(o_3\)-\(o_4\) constant-column symbol pairing) in the fourth column. Therefore,15 these states can have at most two sequences in total, i.e., they are already in \(\mathcal {G}_0\). This shows \(\textsf {turn}^{-1}_{\text{ f }}(\mathcal {G}_1) = \mathcal {G}_1\).
Now, for the main step of the proof, we define \(\mathcal {G}_2 := \textsf {shuf}^{-1}_{}(\mathcal {G}_1)\) and \(\mathcal {G}_3 := \textsf {turn}^{-1}_{\text{ f }}(\mathcal {G}_2)\). Since the shuffling is unrestricted, applying another backwards shuffle to \(\mathcal {G}_2\) cannot produce a larger set, as we can always replace two consecutive shuffles by an equivalent single shuffle. The remaining proof will show \(\mathcal {G}_3 = \mathcal {G}_2\), in which case no further enlargement is possible. Finally, showing that the start state is not in \(\mathcal {G}_2\) finishes the proof.
As \(\mathcal {G}_2\)’s states are subsets of \(\mathcal {G}_1\)’s states,16\(\textsf {cc}(\mathcal {G}_2)\)’s general form is as on the left, from which we can leave out further sequences, as long as we still have at least one \(1\)-sequence and one \(0\)-sequence:
×
where \(t_i\in \{0,1\}\) (\(i=1,2,3\)) are the types of the sequences and \(\overline{t_i}=1-t_i\) their inverses. To see this, observe that states of the form on the left are subsets of the form on the right, where x, y are either both set to a, or one is set to b and the other to c, and, where we leave out at least all sequences interfering with our wish of a constant column in this position (i.e., the sequences in parentheses in the form on the right). With the variables introduced above, we assume a (constant-column symbol) pairing between a and d, and between b and c.17 This is the only way to obtain a maximal number of sequences with a d in column 3 for a state in \(\mathcal {G}_1\). Hence, states in \(\textsf {cc}(\mathcal {G}_2)\) have at least 2 but at most 4 sequences.
Our aim is to show that the set of these states is \(\textsf {cc}(\mathcal {G}_0)\) again, i.e., that \(\textsf {cc}(\mathcal {G}_2) = \textsf {cc}(\mathcal {G}_0)\). (In other words, we show that it is impossible to reach any state in \(\mathcal {G}_1\) via a shuffle from a state of \(\textsf {cc}(\mathcal {G}_2) {\setminus } \textsf {cc}(\mathcal {G}_0)\), which will be shown to be empty.) In the following, we do a case distinction on the number of sequences of states \(\mu \in \textsf {cc}(\mathcal {G}_2)\).
Let us prepend this case distinction with two general observations that will be used in the following. First, every shuffle set \(\varPi \) that is used to map \(\mu \in \textsf {cc}(\mathcal {G}_2)\) to a state \(\mu '\in \mathcal {G}_1\) will contain a permutation \(\pi \) with \(\pi (3)\ne 3\), i.e., one that moves the constant (third) column, as otherwise we cannot generate necessary additional sequences with a non-\(d\) symbol at position \(3\). As defined by Koch et al. [17], we call a state \(i/j\)-state if it has i 0-sequences and j 1-sequences. Using this notation, we have that, if \(\mu \in \textsf {cc}(\mathcal {G}_2)\) is an \(i/j\)-state, then the reached \(\mu '\in \mathcal {G}_1\) after the shuffle will be a \(i'/j'\)-state with \(i'\ge 2i\) and \(j'\ge 2j\), as the shuffle generates \(i+j\) new sequences with \(d\) at a position \(\pi (3)\ne 3\).
Now, let us first consider (a) the case that \(\mu \) has three or four sequences. In this case, there cannot be a permutation \(\pi \in \varPi \) with \(\pi (3) = 4\), as there are only two possible sequences with a \(d\) in position \(4\) in states of \(\mathcal {G}_1\), and this (i.e., having a permutation that maps the d-column to column 4) is the only way to obtain these two sequences ending with \(d\), as no other column contains a d in \(\mu \). Hence, in this case, we have \(i'+j' \le 6\) due to the two unreachable sequences ending with d. Moreover, as \(\mathcal {G}_1\) is built from blocks with one \(0\)- and one \(1\)-sequence, we know that \(i' = j'\). But this allows us already to exclude the case of \(i+j>2\), because if, e.g., \(i=1\) and \(j=2\) (or vice versa), then \(i' \ge 2\) and \(j' \ge 4\), but \(j'=i'\) yields \(i'+j' = 8\), and if \(i=j=2\), then we also have \(i'+j'=8\), both contradicting \(i'+j' \le 6\). Hence, \(\textsf {cc}(\mathcal {G}_2)\) cannot contain any state with three or four sequences.
Now, let (b) \(\mu \) contain two sequences. For this case, we consider choices of two sequences from a state in \(\mathcal {G}_1{\setminus } \mathcal {G}_0\) of (\(*\)) with d in column 3. (We will show below that in the current case we can choose these more specifically from the state on the right of (\(\star \)), without the parentheses.)18 If we choose both sequences to end with da, the state would be in \(\textsf {cc}(\mathcal {G}_0)\), which is, however, inconsistent with the state being in \(\mathcal {G}_1{\setminus } \mathcal {G}_0\). Hence, there is at most one sequence of each of the following types: sequences ending with da, with db and with dc. If we choose to include a sequence ending with da, then it is inconsequential whether we choose one ending with db or with dc (only the d-a constant-column symbol pairing assigns a a special role). W.l.o.g. we choose a sequence ending with db in the following. This leaves us with two choices, either to include a sequence ending with da or to exclude it. In total, we can obtain three states that are not already in \(\textsf {cc}(\mathcal {G}_0)\):
×
where \(t\in \{0,1\}\) is the type of the sequence. However, the third state is similar to the second one via the permutation \((1\;4)\), so we do not need to consider this case. Each of these states needs one \(1\)- and one \(0\)-sequence, which we can fix w.l.o.g. in the first state. This is because the first state is similar to the first state with swapped 0 and 1 types, also via the permutation \((1\;4)\).
We want to show that there is no way to shuffle these two states into a state of \(\mathcal {G}_1{\setminus }\mathcal {G}_0\) as given in (\(*\)). As a first step, we show that, more specifically, it suffices to demonstrate the slightly stricter claim that there is no way to shuffle these two states into a state of \(\mathcal {G}_1{\setminus }\mathcal {G}_0\) as given on the right of (\(\star \)) (including the sequences with parentheses). This is because of the following: as the two-sequence states considered here each have a sequence ending with da, our shuffle needs to reach the other sequence ending with da, in order to complete the block ending with a in \(\mathcal {G}_1{\setminus }\mathcal {G}_0\). Because of the d-a pairing, this sequence also has a d in the third column. Hence, the state reached by the shuffle has at least three ds in the third column. However, as we start with two sequences with distinct types (and all symbols are distinct in the standard deck setting) any permutation \(\pi \in \varPi {\setminus }\{{\textsf {id}}\}\) that increases the number of ds in that column (by \(\pi (3)=3\)) at least doubles the number of sequences. Hence, the resulting state in \(\mathcal {G}_1{\setminus }\mathcal {G}_0\) has at least four ds in column 3 and is therefore of the form in (\(\star \)).
Consequently, for the first state, we have the following scenario:
×
Reaching the state on the left by a shuffle contains at least \(\{{\textsf {id}}, (1\;4\;3), (1\;4\;2)\}\). But applying \((1\;4\;2)\) to the first sequence yields a sequence cadb, which is not possible in the scheme on the left side due to being the third sequence with a trailing b.
The case of the second state is as follows:
×
Reaching the state on the left by a shuffle contains at least \(\{{\textsf {id}}, (2\;4), (1\;4\;3\;2)\}\). But if we apply \((2\;4)\) to the first sequence, we obtain badc, and if we apply \((1\;4\;3\;2)\) to the second sequence, this gives the sequence adbc. The two additional sequences both end with a c, hence they would form a block in the scheme on the left, which is not possible, as the resulting block would miss a constant b-column. This shows that \(\textsf {cc}(\mathcal {G}_2) = \textsf {cc}(\mathcal {G}_0)\).
The start state of base conversion protocols is (up to similarity)
×
with the basis intersection requirement \(|\{1,2\} \cap \{o_1, o_2\}|=1\). Because of this, the state is not in \(\mathcal {G}_0\). As it has a constant column, it would need to be in \(\textsf {cc}(\mathcal {G}_2)\) which is equal to \(\textsf {cc}(\mathcal {G}_0)\) by the argument above. Hence, the state is not in \(\mathcal {G}_2\). \(\square \)
Theorem 4.2
There is no four-card finite-runtime AND protocol with deck \(\mathcal {D}={\llbracket }{1,2,3,4}{\rrbracket }\) with fixed-in-advance output basis.
Proof
As the final states are (without the basis intersection requirement) the same as in the proof of Theorem 4.1, we use the closure \(\textsf {cl}_{\text{ f }}(\mathcal {G}_0)\) derived there, and show that the start state of an AND protocol is not contained in \(\textsf {cl}_{\text{ f }}(\mathcal {G}_0)\). For this, observe that the start state of an AND protocol is (up to similarity) as from the following set:
×
In particular, it has three 0-sequences and one 1-sequence, which excludes it from being in \(\mathcal {G}_0\) or \(\mathcal {G}_1\) (derived in the proof of Theorem 4.1 above), as the numbers of 0- and 1-sequences differ. Moreover, observe that it has in each column exactly two distinct symbols, each exactly twice. For states in \(\mathcal {G}_2\) (which are subsets of \(\mathcal {G}_1\)) it holds that each symbol occurs at most twice in the turn column 4, where each (two-sequence) block ending with one such symbol consists of one \(1\)-sequence and/or one \(0\)-sequence. If we try to leave out sequences from the \(\mathcal {G}_1\) template (for the subsets of \(\mathcal {G}_2\)) to obtain a state of type \(3/1\), we lose the property of having each occurring symbol exactly twice. Hence, the start state cannot be in \(\mathcal {G}_2\). \(\square \)
Card-Minimal Protocols for AND
Theorem 5.1
There is a four-card Las Vegas AND protocol with deck \(\mathcal {D}={\llbracket }{1,2,3,4}{\rrbracket }\) using only random cuts.
Four-card Las Vegas AND protocol using random cuts, cf. Protocol 1. Here, \(X_0 :=X_{00} + X_{01} + X_{10}\) and \(X_1 :=X_{11}\). The relabel operations are not actual actions to be performed but help abbreviate the write-up of the protocol, see “On the choice of cards for input and output”
×
To get a better understanding of why the protocol works and how it is related to the protocol by Niemi and Renvall [26], let us consider exemplarily the case that the first card to be revealed is a 1, the other cases are analogous. In this situation, let us look at the different cases, given in Table 2. Using the method as before, we can remove
by performing a random cut while leaving the relative order intact (
here is assigned the role of the
in Niemi and Renvall’s protocol) and waiting until it appears when turning. Later we can remove the
from the remaining cards, to get the output encoded using the cards
and
. A closer analysis of the situation after removing
shows that one can take a shortcut when one is not bound to the output being cards
(which is not our goal, because in the other cases besides the first turn being 1 it is different anyway, and one would have to add conversion protocols to ensure this). The situation is as follows: The remaining three cards are either a cyclic rotation (cut) of the sequence
, if the output is 0, or a cyclic rotation of the sequence
, otherwise. A cut cannot rotate a sequence of the former type to become the other, or vice versa. After the cut, we can safely turn any card and, from the resulting symbol, deduce in which order the other cards must be output to encode the protocol result.
Table 2
The different states of Protocol 1 after
was revealed in the first turn. The permutation to be applied in this case is \((3\;4)\). The situation is similar in all other cases
Bits
Sequence
After permutation
Removing
(0, 0)
(0, 1)
(1, 0)
(1, 1)
×
For an analysis of the number of shuffle steps in the protocol, observe that we have performed two shuffles until we reach the loop condition, which holds with probability . After the loop, we have one additional shuffle step. Hence, the expected number of shuffles is \(3 + \sum _{n=1}^{\infty }{\left( 1-\frac{1}{4}\right) ^n} = 6\).
The previous protocol, using five cards, was described in the introduction. For a pseudo-code description, see Protocol 2.
×
As Niemi and Renvall state, their running time in the number of shuffle steps is calculated as follows: their protocol starts with a shuffle and repeats this with probability . The second loop contains a shuffle and has a repeating probability of . The shuffle in the final loop is repeated with probability . In total, the expected running time is \(3 + \sum _{n=1}^{\infty }{\left( \frac{3}{5}\right) ^n} + \sum _{n=1}^{\infty }{\left( \frac{3}{4}\right) ^n} + \sum _{n=1}^{\infty }{\left( \frac{2}{3}\right) ^n} = 3 + 1.5 + 3 + 2 = 9.5\). However, for a fair comparison to our protocol, we eliminate the last loop from their protocol, as its only function is to ensure that the output is in basis \(\{1,4\}\), which our protocol does not guarantee. In this case, the modified Niemi–Renvall protocol has an expected number of \(3+1.5+3=7.5\) shuffle steps. Hence, our four-card AND protocol needs one card less and outperforms the Niemi–Renvall protocol by an expected number of 1.5 shuffle steps.
Card-Minimal Protocols for Basis Conversion with Overlapping Bases
In this section, we give two protocols for converting a basis encoding in the case where the old and the new encoding share a card. The first protocol has an expected (finite) running time of three shuffles and turn operations. While it has not been explicit in the literature, it is in a way implicit in the protocol by Niemi and Renvall [26], as the authors aimed to get a fixed-in-advance output basis.
Fig. 7
KWH tree of the five-card AND protocol given by Niemi and Renvall [26] with \(\mathcal {D}= {\llbracket }{1,2,3,4,5}{\rrbracket }\) using only random cuts, cf. Protocol 2. Note that \(X_0 :=X_{00} + X_{01} + X_{10}\) and \(X_1 :=X_{11}\). The output is in basis \(\{1,4\}\)
Fig. 8
Three-card Las Vegas basis conversion for \(\mathcal {D}= {\llbracket }{1,2,3}{\rrbracket }\) with uniform closed shuffles
×
×
Theorem 6.1
There is a three-card Las Vegas basis-conversion protocol for overlapping bases with deck \(\mathcal {D}={\llbracket }{1,2,3}{\rrbracket }\) and uniform closed shuffles.
There is a five-card finite-runtime basis conversion protocol for overlapping bases with deck \(\mathcal {D}={\llbracket }{1,2,3,4,5}{\rrbracket }\). It only uses two random bisection cuts as shuffle operations.
×
Proof
This is just applying the basis conversion by Mizuki [18] twice, cf. Protocol 4. \(\square \)
An Illustration of Our Verification Methodology
In the following, we exemplify our translation of card-based cryptographic AND protocols using standard decks to the bounded model checker CBMC, which takes programs in the C language. For our experiments, we used CBMC 5.11 with the built-in solver based on the SAT-solver MiniSat 2.2.0 [6, 8]. All experiments are performed on an AMD Opteron(tm) 6172 CPU at 2.10 GHz with 48 cores and 256 GB of RAM.
×
We translate KWH trees in the C language using a simple encoding into a bounded C program with only static structures and no pointers, e.g., we employ C structs (see Listing 1) holding an array of card sequences for the sequence \(s\), attached with their respective values for each probability (for the probabilistic security notion) or dependency (for output-possibilistic security) \(X_i\) occurring in \(\mu (s)\), which is simply encoded by another C struct
. The sequences are constructed using non-deterministic values restricted by respective software conditions to enforce a lexicographic ordering. Moreover, we assign the starting values in \(\mu (s)\) with fixed (i.e., deterministic) values based on the constructed sequences. Subsequently, an array of (consecutively) reachable states is constructed non-deterministically using simple implementations of the turn and the shuffle operation as explained in “Preliminaries”. We then repeatedly (after each turn/shuffle) check whether all possible resulting (non-deterministic) states correctly and securely compute the specified function, e.g., here a secure AND.
×
An example shuffle operation is shown in Listing 2 for the case of output-possibilistic security. Therein, the keyword
is used by the bounded model checker to restrict all program runs passing this statement to satisfy the specified (Boolean) condition. By assigning values using the special function
, we assign a non-deterministic non-negative integer number, which is restricted to values greater than zero and at most of value
(which is a variable computed by the pre-processor and is the maximum number of sequences possible with the given deck) in the following program statement. In the shown example, the non-determinism is used to construct a set of permitted permutation sets (to be used by the shuffle operation), which makes the SBMC tool inspect the following program code for all possible assignments of this value. If necessary, this may result in a fully exhaustive search, however, the prover is often able to restrict the domain based on further program statements and dependencies seen in the rest of the program. A similar trick is used when computing the concrete permutations using the non-deterministic value of
in order to check all possible permutations which possibly move the values, but preserve all existing numbers in the sequence itself. This is done using the
-array
, which is first initialized to zero and, when choosing a concrete permutation, assumed to be zero at position
, however set to the number one right afterwards (such that it is not permitted to be chosen again). In the subsequent inner loop, the permutations are assigned choosing the according cards from the sequences in the start state using the non-deterministic value
. Finally, the shuffle is applied, resulting in the state variable
, which is then checked using a further method
to not contain any sequences with impermissible values for \(X_i\), which would result in incorrect computations of the AND function.
Table 3
Running times for showing/disproving protocol existence for standard and two-color decks. While all rows having “✓” in the column “Protocol” indicate that a protocol run is output by our method with the CBMC running time as indicated in the table, these do not automatically feature probabilistic security. Hence, we add references to protocols with the given parameters, which should not (generally) be understood as having been discovered using our method
\(^{\mathrm{a}}\)This holds only w.r.t. protocols with shuffle size of at most 8, excluding subgroups of size 12
\(^{\mathrm{b}}\)For this, we had to strengthen the security to input-possibilistic security
Fig. 9
The four-card protocol by Koch et al. [17], with placeholders as specified in the text to define two similar variants of the same protocol. The contracted, non-closed variant has a shortest run of length 4, while the closed variant has a shortest run of length 6
×
×
We applied our approach to the computation of a secure AND protocol using four cards to, first, substantiate our proof that no protocol of a length below six can be found, and, secondly, automatically find a permitted protocol using six operations. For the running times and formula size (i.e., numbers of variables and clauses) generated by our method, we refer to Table 3.
Verification of Run-Minimality in Two-Color Deck Protocols
For the two-color deck setting, a card-minimal Las Vegas AND protocol using only four cards was given by Koch et al. [17]. While they use only closed shuffles, some of the shuffles are non-uniform and hence, the protocol is rather difficult to implement. However, we argue that it is insightful to analyze whether the protocol features a shortest run. For this, let us note that there are two possible versions of this protocol: by contracting two subsequent closed shuffles, we can generate a protocol with fewer but non-closed shuffles. Both protocols are given in Fig. 9 and Protocol 5, where \(\varPi _1, \mathcal {F}_1, \varPi _2, \mathcal {F}_2\) are permutation groups and probability distributions are as follows:
and \(\alpha _1,\alpha _2,\alpha _3\) are placeholders for one or two actions, which are for the full protocol as follows:
and for the protocol using contracted shuffles as below:
Run-minimality results To summarize our run-minimality results derived from our adaption of the program to the two-color setting, we showed by formal verification that the closed AND protocol variant has a shortest run of 6 steps, relative to all closed four-card AND protocols. This is because our method excluded the possibility of an input-possibilistic19 closed four-card AND protocol with a run of length 5. Moreover, our contracted AND protocol is run-minimal in that no (output-possibilistic) four-card AND protocol with a run of length 3 exists. See also Table 3. In the following, we describe the changes in our verification method.
×
×
As the program by Koch et al. [15] is already very general, the adaptions for covering the two-color settings required only little changes. The programs mainly differ in the assignment of the start state, in the following code snippets identified by
, for the protocol. In the following, the variable
specifies the number of distinct card symbols, which was not needed in the standard deck setting, as there it was identical to the total number of cards. In Listing 3, the variable
specifies this total number of cards.
In the standard deck setting, each player gets distinct symbols 1 and 2, or 3 and 4, respectively (as shown in the first two lines in Listing 3). For the two-color deck setting, it suffices to require that the individual cards for each player are pairwise distinct as shown in the first two lines in Listing 4. Moreover, we simply numbered the helper cards consecutively for the standard deck setting (see the loop in Listing 3), but allowed an arbitrary assignment of valid card symbols in the two-color deck setting (see the loop in Listing 4).
Besides the introduction of the variable
, these are the main changes that were needed to cover the two-color deck setting. Note that we moreover adapted the script that calls the SBMC tool together with our C program to compute the new number of possible sequences. For the standard deck setting, the number was simply the factorial of the total number of cards. In the two-color deck setting, this is the binomial coefficient of the two different amounts of cards with distinct symbols.
Verification of Shuffle Set Size Maximality
In the following, we exploit the fact that the number of possible sequences in a protocol state may be significantly smaller than the number of possible permutations on the deck for the two-color setting. We, therefore, extend our formal verification technique to additionally establish a formal guarantee that it suffices to search protocols with a smaller permutation set size (i.e., also the shuffle set size). Hence, the number of possible shuffles gets significantly smaller, which reduces the work for the SBMC tool and thus leads to significantly smaller running times.
We can write a simple program—via some simple adaptions from the program in “An illustration of our verification methodology”—that serves as an input for the SBMC tool to verify the maximality of a given shuffle set size. The shuffle operation from Listing 2 is adapted such that we can specify a lower bound for the non-deterministic variable
. We search for a single shuffle operation such that a valid output state is reached from a “minimal state”, i.e., a state that has at most one 1-sequence and one 0-sequence (that should not be mixed together in the shuffle). In Listing 5 this is done by setting the probabilities of two arbitrary distinct sequences in that state to be the inverse of each other, i.e., \((1\ 0)\) and \((0\ 1)\). In the end, we check whether, after performing a shuffle operation on this state, we can still reach a valid state afterwards. Note that, since we are looking for worst-case maximality bounds, it suffices to employ the output-possibilistic setting (see Definition 2.2) which reduces the search complexity.
For the verification of a maximal shuffle set size, we can run the SBMC tool on this program for various lower bounds for
until we find the smallest value such that no valid state is reachable anymore. This gives us a guarantee that larger shuffle set sizes cannot produce smaller protocol runs and we can hence use this value for an upper bound on the shuffle set size in the approach from “Verification of run-minimality in two-color deck protocols”.
×
The described functionality in the C program is shown in Listing 5. Therein,
and
are the non-deterministically chosen indices for the zero- and one-sequence, which are assumed to be distinct. The minimal start state is given by the variable
(which contains an array of sequences). We perform a non-deterministic shuffle operation on
by calling the method
. Finally, we ask the SBMC tool to check whether the produced
is a valid state using the final
statement.
Note that the results of this section in determining the maximal useful shuffle set size hold not only for AND but also for all Boolean functions that have at least two possible outputs. The results are summarized in Table 4.
Table 4
Running times for proving shuffle set size maximality
For some of the settings with closedness requirement we specify ranges, which should indicate that the larger range is already impossible due to the size restrictions of subgroups. See Naik [23, 24] for reference
\(^{\mathrm{a}}\)As the largest proper subgroup is of size 12, there is nothing to show. (\(S_4\) creates \(\bot \)-sequences)
\(^{\mathrm{b}}\)This run did not finish in time, or ran into the self-set timeout bound of 5 days.
\(^{\mathrm{c}}\)\(>\!48\) permutations is impossible even non-closed, and 60 is the only proper subgroup size \(>\!24\)
As an example, see Fig. 10 (left) for the maximal shuffle set size (of 12) that is useful in four-card two-color protocols in general. Here, the shuffle starts from a minimal 2-sequence state that was chosen arbitrarily and non-deterministically by our SAT solver, but is likely to have maximal Hamming distance among their sequences. For protocols using only closed shuffles, our method showed that this bound is 8 permutations, as there is no larger closed permutation set that can result in a valid state, cf. Fig. 10 (right). These bounds are fully tight.
Fig. 10
Situation discovered by our formal method to find a minimal state and a maximal permutation set (of size 12 (left) and 8 (right), respectively), such that applying this shuffle to the minimal state does not generate an invalid state (with \(\bot \)-sequences). Our method showed that larger shuffle sets (left) or groups (right) cannot result in valid states, allowing us to reduce the shuffle set size in verification steps without loosing generality. Here, \(D_8^\text {conj}\) denotes a dihedral group of order 8
×
In the five-card two-color setting, closed protocols can make use of shuffle groups of at most 24 permutations. It is an open question whether this is a tight bound, but we know that there is a 12 element shuffle that is valid. However, it still allows us to restrict the maximal shuffle group size to 24 when searching protocols. For this five-card case and arbitrary non-closed shuffle sets, the maximal shuffle set size that does not introduce \(\bot \)-sequences on a minimal state is 48. This is a tight bound.
Fig. 11
Situation discovered by our formal method to find a minimal state and a maximal permutation set (of size 12, namely the alternating group \(A_4\)), such that applying this shuffle to the minimal state does not generate an invalid state (with \(\bot \)-sequences), in the standard deck setting
×
Additionally, we have adapted this method to the standard deck setting as well and have determined that the largest permutation set permissible in a protocol on four cards is 12. This also holds for the closed case, i.e., there is a group with 12 elements, namely the alternating group \(A_4\), that, if performed on a minimal state, can result in a state that does not contain any \(\bot \)-sequences.
Conclusion
In this paper, we proposed a new method to search card-based protocols for any secure computation, by giving a general formal translation applicable to be used by the formal technique of software bounded model checking (SBMC). This method allows us to find new protocols automatically, and prove lower bounds on required shuffle and turn operations for any protocol, and provide an example for the computation of a minimal AND protocol. We also found a new protocol that only uses the theoretical minimum of four distinguishable cards for an AND computation. Moreover, we supported this finding by our automatic method in showing the impossibility of any protocol using less shuffle and turn operations using only practicable shuffles (random cuts). The protocol is hence optimal w.r.t. the running time restriction “restart-free Las-Vegas”. For the four-card standard deck setting, we showed that there is no finite runtime protocol, regardless of the shuffle operations used. This result completes the picture of tight lower bounds for the four-card setting. Additionally, we showed tight lower bounds on basis conversions for single bits and proposed the missing protocols, and establish the theorem that using a minimum of five cards, both input- and output-bases can be chosen freely, which fosters our impossibility result for the four-card setting.
Finally, we extended our verification method to the case of decks using only two colors, which is more common in the field of card-based cryptography. In this setting, we were able to show two variants of a card-minimal Las Vegas AND protocol to be also run-minimal, i.e., the protocol has a run of minimal length. Moreover, for the case of 4 cards, we derived tight upper bounds on the size of the maximal usable permutation set, of 12 and 8 for general and closed protocols, respectively. As this is not restricted to AND protocols, but applies more generally, we believe this to be of independent interest for researchers in the field of card-based cryptography.
Open Problems
Let us point out some open problems in the card-based security area that could be approached based on the findings in this paper: (1) for finite-runtime protocols, there exist no proven tight lower bounds on the required number of cards (five to eight cards). We recommend more research applying computer-aided formal methods at this point, as the state space for five or more cards is very large. (2) Our verification approach is fast for finding protocols and/or lower bounds on the operations needed in a protocol for given shuffle-restrictions. However, this is based on the assumption that protocols exist already for a given predefined length to find or confirm impossibility results. Investigating computer-aided formal methods for universal impossibility results might be worthwhile. (3) The two most common settings in card-based cryptography are the standard deck setting with only distinguishable cards and the two-color decks using \(\clubsuit \) and \(\heartsuit \). However, it may be possible that by mixing these settings (e.g., only distinguishable cards with one pair of identical cards), we might find more efficient protocols (especially in the finite runtime setting). For such a mixed setting, Shinagawa and Mizuki [28] provide nice results to use in further research.
Acknowledgements
The authors would like to thank the anonymous reviewers for their detailed and helpful comments and suggestions.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This appendix contains the 8-card AND protocol by Mizuki [18] (Fig. 12) and a second four-card protocol which uses a number of 4.5 shuffles in expectation, which are, however, non-closed and hence, more impractical to implement, cf. Fig. 13. Moreover, we have added a variant of the protocol by Abe et al. [1] where we save one permutation step in the beginning, in Fig. 14.
Fig. 12
The eight-card finite-runtime AND protocol by Mizuki [18], with \(\mathcal {D}= {\llbracket }{1,\dots ,8}{\rrbracket }\) and uniform-closed shuffles. Output is in basis \(\{5,6\}\) or \(\{7,8\}\), each with probability 1/2
Fig. 13
A four-card Las Vegas AND protocol with deck \(\mathcal {D}= {\llbracket }{1,2,3,4}{\rrbracket }\) and uniform shuffles. Note that \(X_0 :=X_{00} + X_{01} + X_{10}\) and \(X_1 :=X_{11}\). The output is in one of the bases \(\{1,3\}, \{1,4\}, \{2,3\}, \{3,4\}\), determined by the position of the final state in the tree, and can be converted as needed
Fig. 14
A slightly shorter version of the five-card two-color Las Vegas AND protocol with uniform closed shuffles given by Abe et al. [1]. Here, we save one initial permutation step at the cost of using the slightly more complex shuffle \(\varPi _1\) that is not as easy to perform as just cutting the cards (albeit still a “random cut”, i.e., a cyclic group generated by a cycle). As our counting method for the number of steps assumes single-card turns, observe that the two-card turn step in the end can be split into two single-card turns, where turning the first card can already result in the final state on the left. Hence, its shortest run consists of only four steps. (This protocol version was found when trying to prove the run-minimality of the protocol by Abe et al. [1] w. r. t. closed five-card two-color AND protocols – whether a protocol with these parameters and a run of only three steps exists, remains open.)
As an example, in a Duplicate Bridge tournament, one might prove that all sessions are handed the same cards, eliminating the need of a trusted dealer (no pun intended).
It is clear that if a state with a \(\bot \) sequence arises, then the protocol has to abort later, as if this sequence would actually lie on the table, it is no longer clear whether an input sequence encoding (0, 0), or an input sequence encoding (1, 1) was on the table at the start.
While we chose for the example the same state as depicted on p. 21 in the impossibility proof where it is later used, note that there, \(\mathcal {G}\) also already includes all the depicted eight states including any deterministic permutations (via the similarity relation) of all these, and hence is a much larger set to start with.
In case of the decks being a subset of \({\mathbb {N}} \), we may use usual permutation notation. We require that if \(\lambda \) maps \(x\) to \(y\), then the cardinalities of \(x\) and \(y\) are equal in the deck.
For the impossibility result, the symbols of the cards are irrelevant, as we could prepend a relabel operation to any protocol, to bring it into this form.
Refer to Definition 2.3. We do not want to assume anything on at which positions the output lies, hence we include all permutations of the states into the discussion.
As we consider states up to similarity, we can just permute each of these states constituting the full turnable state in such a way that their constant column is at position 4
Analogous to before, as all constituting states of the set are up to similarity, we have free choice in choosing a position at which the constant column should be.
As both sequences in a block have identical symbols in column 4, and given the pairwise distinctiveness of these symbols between blocks, there are at most two such sequences within a state.
We assume w.l.o.g. that any shuffle contains the \({\textsf {id}}\) permutation, hence, non-trivial shuffling generates new sequences. Consequently, backwards shuffling then only leaves out sequences, which we describe in set-theoretic terms, by abuse of notation.
To see that this is not already immediate, observe that the state on the right of (\(\star \)) was chosen to maximize the number of d’s in column 3, and is not as general as saying that the state is of (\(*\)) with a d in column 3. However, this loss of generality does not restrict the general form of \(\textsf {cc}(\mathcal {G}_2)\) on the left of (\(\star \)).
Because it found a possible output-possibilistic (but not input-possibilistic) protocol run, we had to strengthen the search criteria to protocols which are at least input-probabilistic.
and
. It is essential that the cards’ backs are indistinguishable, such that when they are put face-down on the table, the only thing observable
. With these cards, the two players can encode a commitment to a bit (yes or no) by the order of two cards
, \(i,j\in \{1,\dots ,5\}\) (with \(i \ne j\)) via the encoding
Alice inputs her bit by putting the cards
face-down and in the respective order on the table (she puts
for input 0, and
for input 1), while Bob does the same using his cards
. We need an additional helper-card, here a
, which is put to the left of the two players’ cards.
and
in this sequence already encodes the output of the protocol, i.e., it reads
if the output is 1, and
otherwise. Hence, by securely removing the cards
and
(which is explained below), one directly obtains the output. We see this by inspecting all possible cases:
and
, while keeping the relative order of all cards in the sequence intact, by cutting the cards, i.e., rotating the sequence by a random offset which is unknown to the players. We can then securely turn the first card and remove it in case it is a
or a
. Due to the cut, the turned card is random and hence does not reveal anything about the inputs. When both cards are removed, we reach a configuration where
is the first card by the same procedure where the two remaining cards encode the AND result. Here, the
played the crucial role of a separator that keeps the relative order of the remaining cards—starting from the separator—intact, when doing a random cut. (A formal version of this protocol is given in Protocol 2 and Fig. 7.)
, and whether there are simpler protocols. Moreover, to handle the increasing combinatorial state space (relative to protocols on decks of just \(\clubsuit \) and \(\heartsuit \) ), we introduce formal verification to the field of card-based cryptography.
to Alice and
to Bob, or
to Alice and
to Bob. We provide an analysis of this question, showing that with certain restrictions, there is a relatively large freedom in choosing the input (and/or output) bases. This is a useful prerequisite in proving the impossibility of a protocol with a given number of cards.
, and
. The identity permutation is denoted as \({\textsf {id}}\).
, ...) if the deck is larger to the right of the players bits. The state (or KWH) tree of a protocol is then a directed tree where the nodes are states as above, with annotations at the outgoing edges of each state, specifying the action that is performed next. Let \(\mu \) be the state with the outgoing annotation, then the possible actions are defined as: 
. We can make it known to the players, i.e., deterministic, by splitting up the state via an \(S_k\)-shuffle (here: \(k=2\)) on the remaining cards (so that they no longer contain any information), turning these and then doing the result operation. By what is visible in the turn, one can derive the output basis
by performing a random cut while leaving the relative order intact (
here is assigned the role of the
in Niemi and Renvall’s protocol) and waiting until it appears when turning. Later we can remove the
from the remaining cards, to get the output encoded using the cards
and
. A closer analysis of the situation after removing
shows that one can take a shortcut when one is not bound to the output being cards
(which is not our goal, because in the other cases besides the first turn being 1 it is different anyway, and one would have to add conversion protocols to ensure this). The situation is as follows: The remaining three cards are either a cyclic rotation (cut) of the sequence
, if the output is 0, or a cyclic rotation of the sequence
, otherwise. A cut cannot rotate a sequence of the former type to become the other, or vice versa. After the cut, we can safely turn any card and, from the resulting symbol, deduce in which order the other cards must be output to encode the protocol result.
was revealed in the first turn. The permutation to be applied in this case is \((3\;4)\). The situation is similar in all other cases
. After the loop, we have one additional shuffle step. Hence, the expected number of shuffles is \(3 + \sum _{n=1}^{\infty }{\left( 1-\frac{1}{4}\right) ^n} = 6\).
. The second loop contains a shuffle and has a repeating probability of
. The shuffle in the final loop is repeated with probability
. In total, the expected running time is \(3 + \sum _{n=1}^{\infty }{\left( \frac{3}{5}\right) ^n} + \sum _{n=1}^{\infty }{\left( \frac{3}{4}\right) ^n} + \sum _{n=1}^{\infty }{\left( \frac{2}{3}\right) ^n} = 3 + 1.5 + 3 + 2 = 9.5\). However, for a fair comparison to our protocol, we eliminate the last loop from their protocol, as its only function is to ensure that the output is in basis \(\{1,4\}\), which our protocol does not guarantee. In this case, the modified Niemi–Renvall protocol has an expected number of \(3+1.5+3=7.5\) shuffle steps. Hence, our four-card AND protocol needs one card less and outperforms the Niemi–Renvall protocol by an expected number of 1.5 shuffle steps.
. The sequences are constructed using non-deterministic values restricted by respective software conditions to enforce a lexicographic ordering. Moreover, we assign the starting values in \(\mu (s)\) with fixed (i.e., deterministic) values based on the constructed sequences. Subsequently, an array of (consecutively) reachable states is constructed non-deterministically using simple implementations of the turn and the shuffle operation as explained in “Preliminaries”. We then repeatedly (after each turn/shuffle) check whether all possible resulting (non-deterministic) states correctly and securely compute the specified function, e.g., here a secure AND.
is used by the bounded model checker to restrict all program runs passing this statement to satisfy the specified (Boolean) condition. By assigning values using the special function
, we assign a non-deterministic non-negative integer number, which is restricted to values greater than zero and at most of value
(which is a variable computed by the pre-processor and is the maximum number of sequences possible with the given deck) in the following program statement. In the shown example, the non-determinism is used to construct a set of permitted permutation sets (to be used by the shuffle operation), which makes the SBMC tool inspect the following program code for all possible assignments of this value. If necessary, this may result in a fully exhaustive search, however, the prover is often able to restrict the domain based on further program statements and dependencies seen in the rest of the program. A similar trick is used when computing the concrete permutations using the non-deterministic value of
in order to check all possible permutations which possibly move the values, but preserve all existing numbers in the sequence itself. This is done using the
-array
, which is first initialized to zero and, when choosing a concrete permutation, assumed to be zero at position
, however set to the number one right afterwards (such that it is not permitted to be chosen again). In the subsequent inner loop, the permutations are assigned choosing the according cards from the sequences in the start state using the non-deterministic value
. Finally, the shuffle is applied, resulting in the state variable
, which is then checked using a further method
to not contain any sequences with impermissible values for \(X_i\), which would result in incorrect computations of the AND function.
and \(\alpha _1,\alpha _2,\alpha _3\) are placeholders for one or two actions, which are for the full protocol as follows:
and for the protocol using contracted shuffles as below:
Run-minimality results To summarize our run-minimality results derived from our adaption of the program to the two-color setting, we showed by formal verification that the closed AND protocol variant has a shortest run of 6 steps, relative to all closed four-card AND protocols. This is because our method excluded the possibility of an input-possibilistic19 closed four-card AND protocol with a run of length 5. Moreover, our contracted AND protocol is run-minimal in that no (output-possibilistic) four-card AND protocol with a run of length 3 exists. See also Table 3. In the following, we describe the changes in our verification method.
, for the protocol. In the following, the variable
specifies the number of distinct card symbols, which was not needed in the standard deck setting, as there it was identical to the total number of cards. In Listing 3, the variable
specifies this total number of cards.
, these are the main changes that were needed to cover the two-color deck setting. Note that we moreover adapted the script that calls the SBMC tool together with our C program to compute the new number of possible sequences. For the standard deck setting, the number was simply the factorial of the total number of cards. In the two-color deck setting, this is the binomial coefficient of the two different amounts of cards with distinct symbols.
. We search for a single shuffle operation such that a valid output state is reached from a “minimal state”, i.e., a state that has at most one 1-sequence and one 0-sequence (that should not be mixed together in the shuffle). In Listing 5 this is done by setting the probabilities of two arbitrary distinct sequences in that state to be the inverse of each other, i.e., \((1\ 0)\) and \((0\ 1)\). In the end, we check whether, after performing a shuffle operation on this state, we can still reach a valid state afterwards. Note that, since we are looking for worst-case maximality bounds, it suffices to employ the output-possibilistic setting (see Definition 2.2) which reduces the search complexity.
until we find the smallest value such that no valid state is reachable anymore. This gives us a guarantee that larger shuffle set sizes cannot produce smaller protocol runs and we can hence use this value for an upper bound on the shuffle set size in the approach from “Verification of run-minimality in two-color deck protocols”.
and
are the non-deterministically chosen indices for the zero- and one-sequence, which are assumed to be distinct. The minimal start state is given by the variable
(which contains an array of sequences). We perform a non-deterministic shuffle operation on
by calling the method
. Finally, we ask the SBMC tool to check whether the produced
is a valid state using the final
statement.