Formal Verification and Proof of Impossibility for Four-Card XOR Protocols Using Only Random Cuts

In card-based cryptography, which uses physical cards for secure computation, proving lower bounds on the number of cards and shuffles is an important research problem. There are two different approaches to demonstrate the impossibility of protocol construction: formal verification and proof using pen and paper. In card-based protocols, shuffles are the most important operations to ensure the correctness and security of protocols. A random cut, which randomly shifts a sequence of cards, is considered the easiest shuffle to implement. For this reason, many protocols using only random cuts as shuffle operations have been proposed, and proving lower bounds on the number of cards and shuffles in this setting is also recognized as an important problem. As for XOR protocols using only random cuts, Toyoda et al. constructed a six-card XOR protocol, but so far it is not clear whether there are protocols with fewer cards. In this paper, we prove the impossibility of a four-card XOR protocol using only random cuts, employing both formal verification and proof using pen and paper. In formal verification, we apply the verification method for AND protocols developed by Koch et al. to XOR protocols, and show that the number of shuffles is at least three. In the proof using pen and paper, we show that a four-card XOR protocol is impossible to construct even when allowing any number of shuffles.