This is an extended summary submitted in order to rapidly disseminate our ideas. We expect to replace this summary with a longer version in the near future; meanwhile, any feedback would be appreciated
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).
While feedback control has many applications in quantum systems, finding optimal control protocols for this task is generally challenging. So-called "verification theorems" and "viscosity solutions" provide two useful tools for this purpose: together they give a simple method to check whether any given protocol is optimal, and provide a numerical method for finding optimal protocols. While treatments of verification theorems usually use sophisticated mathematical language, this is not necessary. In this article we give a simple introduction to feedback control in quantum systems, and then desc…
This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a framework from formalizing basic quantum phenomena, which are utilized to achieve communication tasks. We also present an example of applying this framework to the modeling and analyzing quantum communication protocols to show how it works.
Analog quantum simulation is expected to be a significant application of near-term quantum devices. Verification of these devices without comparison to known simulation results will be an important task as the system size grows beyond the regime that can be simulated classically. We introduce a set of experimentally-motivated verification protocols for analog quantum simulators, discussing their sensitivity to a variety of error sources and their scalability to larger system sizes. We demonstrate these protocols experimentally using a two-qubit trapped-ion analog quantum simulator and numerica…
Instantaneous nonlocal quantum computation (INQC) evades apparent quantum and relativistic constraints and allows to attack generic quantum position verification (QPV) protocols (aiming at securely certifying the location of a distant prover) at an exponential entanglement cost. We consider adversaries sharing maximally entangled pairs of qudits and find low-dimensional INQC attacks against the simple practical family of QPV protocols based on single photons polarized at an angle $θ$. We find exact attacks against some rational angles, including some sitting outside of the Clifford hierarchy (…
We use the entanglement sampling techniques developed by Dupuis, Fawzi and Wehner to find a lower bound on the entanglement needed by a coalition of cheater attacking the quantum position verification protocol using the four BB84 states in the scenario where the cheaters have no access to a quantum channel but share a (possibly mixed) entangled state $\tildeΦ$. For a protocol using n qubits, a necessary condition for cheating is that the max- relative entropy of entanglement $E_{\max}(\tildeΦ)\ge n-O(\log n)$. This improves previously known best lower bound by a factor $\sim4$, and it is essen…
Quantum inspired protocols e.g. [AAV13,AG17] attempt to achieve a single-prover interactive protocol where a classical machine can verify quantum computations in an information-theoretically secure manner. We define a family of protocols which seem natural for verifying quantum computations and generalizes such known protocols, namely those of [AAV13,AG17]. We show that any protocol from this family is bound to require an extremely powerful prover, much like the classical protocols of [LFKN92] and [Sha92]. Using our analysis, we also hint at possible ways one might try to realize a protocol wh…
Boson sampling is a sub-universal model used to show quantum speed-up. However, the methods of validation to prove quantum speedup are not robust and accurate. All verification methods involve additional or little studied assumptions. Here, we use the protocols given in the paper [arXiv:2006.03520] to construct a boson sampling experiment using discrete quantum states on IBM quantum computer and verify the fidelity of the output states using heterodyne detection. We demonstrate the protocols for single mode fidelity estimation, multi mode fidelity estimation and a verification protocol using I…
We propose practical and efficient protocols for verifying bipartite pure states for any finite dimension, which can also be applied to fidelity estimation. Our protocols are based on adaptive local projective measurements with either one-way or two-way communications, which are very easy to implement in practice. They can extract the key information much more efficiently than known protocols based on tomography or direct fidelity estimation, and their efficiencies are comparable to the best protocols based on entangling measurements. These protocols highlight the significance of mutually unbi…
With experimental quantum computing technologies now in their infancy, the search for efficient means of testing the correctness of these quantum computations is becoming more pressing. An approach to the verification of quantum computation within the framework of interactive proofs has been fruitful for addressing this problem. Specifically, an untrusted agent (prover) alleging to perform quantum computations can have his claims verified by another agent (verifier) who only has access to classical computation and a small quantum device for preparing or measuring single qubits. However, when t…
The efficient and reliable characterization of quantum states plays a vital role in most, if not all, quantum information processing tasks. In this work, we present a universally optimal protocol for verifying entangled states by employing the so-called quantum nondemolition measurements, such that the verification efficiency is equivalent to that of the optimal global strategy. Instead of being probabilistic as the standard verification strategies, our protocol is constructed sequentially, which is thus more favorable for experimental realizations. In addition, the target states are preserved…
In this article, we propose an interactive protocol for one party (the verifier) holding a quantum computer to verify the quantum computation power of another party's (the prover) device via a one-way quantum channel. This protocol is referred to as the dihedral coset problem (DCP) challenge. The verifier needs to prepare quantum states encoding secrets (DCP samples) and send them to the prover. The prover is then tasked with recovering those secrets with a certain accuracy. Numerical simulation demonstrates that this accuracy is sensitive to errors in quantum hardware. Additionally, the DCP c…
We present two verification protocols where the correctness of a "target" computation is checked by means of "trap" computations that can be efficiently simulated on a classical computer. Our protocols rely on a minimal set of noise-free operations (preparation of eight single-qubit states or measurement of four observables, both on a single plane of the Bloch sphere) and achieve linear overhead. To the best of our knowledge, our protocols are the least demanding techniques able to achieve linear overhead. They represent a step towards further reducing the quantum requirements for verification…
Quantum cloud computing is emerging as a popular model for users to experience the power of quantum computing through the internet, enabling quantum computing as a service. The question is, when the scale of the computational problems becomes out of reach of classical computers, how can users be sure that the output strings sent by the server are really from a quantum hardware? In 2008, Shepherd and Bremner proposed a cryptographic verification protocol based on a simplified circuit model called IQP (instantaneous quantum polynomial-time), which can potentially be applied to most existing quan…
The classical channel remote state preparation (ccRSP) is an important two-party primitive in quantum cryptography. Alice (classical polynomial-time) and Bob (quantum polynomial-time) exchange polynomial rounds of classical messages, and Bob finally gets random single-qubit states while Alice finally gets classical descriptions of the states. In [T. Morimae, arXiv:2003.10712], an information-theoretically-sound non-interactive protocol for the verification of quantum computing was proposed. The verifier of the protocol is classical, but the trusted center is assumed that sends random single-qu…
We discuss quantum position verification (QPV) protocols in which the verifiers create and send single-qubit states to the prover. QPV protocols using single-qubit states are known to be insecure against adversaries that share a small number of entangled qubits. We introduce QPV protocols that are practically secure: they only require single-qubit states from each of the verifiers, yet their security is broken if the adversaries share an impractically large number of shared entangled qubits. These protocols are a modification of known QPV protocols in which we include a classical random oracle…
Verifying quantum states is central to certifying the correct operation of various quantum information processing tasks. In particular, in measurement-based quantum computing, checking whether correct graph states are generated is essential for reliable quantum computing. Several verification protocols for graph states have been proposed, but none of these are particularly resource efficient: multiple copies are required to extract a single state that is guaranteed to be close to the ideal one. The best protocol currently known requires $O(n^{15})$ copies of the state, where $n$ is the size of…
Blind quantum computing is a new secure quantum computing protocol where a client who does not have any sophisticated quantum technlogy can delegate her quantum computing to a server without leaking any privacy. It is known that a client who has only a measurement device can perform blind quantum computing [T. Morimae and K. Fujii, Phys. Rev. A {\bf87}, 050301(R) (2013)]. It has been an open problem whether the protocol can enjoy the verification, i.e., the ability of client to check the correctness of the computing. In this paper, we propose a protocol of verification for the measurement-only…
Statistical verification of a quantum state aims to certify whether a given unknown state is close to the target state with confidence. So far, sample-optimal verification protocols based on local measurements have been found only for disparate groups of states: bipartite pure states, GHZ states, and antisymmetric basis states. In this work, we investigate systematically optimal verification of entangled stabilizer states using Pauli measurements. First, we provide a lower bound on the sample complexity of any verification protocol based on separable measurements, which is independent of the n…
Efficient Verification of Entangled Measurements with Local States
Independent Researcher（独立研究者）；School of Data Science, The Chinese University of Hong Kong, Shenzhen（香港中文大学（深圳）数据科学学院）；International Quantum Academy (SIQA)（国际量子学院）
Quantum processes, such as quantum circuits, quantum memories, and quantum channels, are essential ingredients in almost all quantum information processing tasks. However, the characterization of these processes remains a daunting task due to the exponentially increasing amount of resources required by traditional methods. Here, by first proposing the concept of quantum process verification, we establish two efficient and practical protocols for verifying quantum processes which can provide an exponential improvement over the standard quantum process tomography and a quadratic improvement over…
An experiment based on a trapped Ytterbium ion validates the inertial theorem for the SU(2) algebra. The qubit is encoded within the hyperfine states of the atom and controlled by RF fields. The inertial theorem generates analytical solutions for non-adiabatically driven systems that are `accelerated' slowly, bridging the gap between the sudden and adiabatic limits. These solutions are shown to be stable to small deviations, both experimentally and theoretically. As a result, the inertial solutions pave the way to rapid quantum control of closed, as well as open quantum systems. For large devi…
Device-independent quantum cryptography allows security even if the devices used to execute the protocol are untrusted - whether this is due to unknown imperfections in the implementation, or because the adversary himself constructed them to subvert the security of the protocol. While device-independence has seen much attention in the domain of quantum key distribution, relatively little is known for general protocols. Here we introduce a new model for device-independence for two-party protocols and position verification in the noisy-storage model. For the first time, we show that such protoco…
Loss of inputs can be detrimental to the security of quantum position verification (QPV) protocols, as it may allow attackers to not answer on all played rounds, but only on those they perform well on. In this work, we study \textit{loss-tolerant} QPV protocols. We propose a new fully loss-tolerant protocol QPV$_{\textsf{SWAP}}$, based on the SWAP test, with several desirable properties. The task of the protocol, which could be implemented using only a single beam splitter and two detectors, is to estimate the overlap between two input states. By formulating possible attacks as a semi-definite…
Graph states are entangled resource states for universal measurement-based quantum computation. Although matter qubits such as superconducting circuits and trapped ions are promising candidates to generate graph states, it is technologically hard to entangle a large number of them due to several types of noise. Since they must be sufficiently cooled to maintain their quantum properties, thermal noise is one of major ones. In this paper, we show that for any temperature $T$, the fidelity $\langle G|ρ_T|G\rangle$ between an ideal graph state $|G\rangle$ at zero temperature and a thermal graph st…
Quantum protocols such as the BB84 Quantum Key Distribution protocol exchange qubits to achieve information-theoretic security guarantees. Many variants thereof were proposed, some of them being already deployed. Existing security proofs in that field are mostly tedious, error-prone pen-and-paper proofs of the core protocol only that rarely account for other crucial components such as authentication. This calls for formal and automated verification techniques that exhaustively explore all possible intruder behaviors and that scale well. The symbolic approach offers rigorous, mathematical frame…
We consider an information reconciliation protocol for quantum key distribution (QKD). In order to correct down the error rate, we suggest a method, which is based on symmetric blind information reconciliation for the low-density parity-check (LDPC) codes. We develop a subsequent verification protocol with the use of $ε$-universal hash functions, which allows verifying the identity between the keys with a certain probability.
With today's quantum processors venturing into regimes beyond the capabilities of classical devices [1-3], we face the challenge to verify that these devices perform as intended, even when we cannot check their results on classical computers [4,5]. In a recent breakthrough in computer science [6-8], a protocol was developed that allows the verification of the output of a computation performed by an untrusted quantum device based only on classical resources. Here, we follow these ideas, and demonstrate in a first, proof-of-principle experiment a verification protocol using only classical means …
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which …
Chandran et al. (SIAM J. Comput.'14) formally introduced the cryptographic task of position verification, where they also showed that it cannot be achieved by classical protocols. In this work, we initiate the study of position verification protocols with classical verifiers. We identify that proofs of quantumness (and thus computational assumptions) are necessary for such position verification protocols. For the other direction, we adapt the proof of quantumness protocol by Brakerski et al. (FOCS'18) to instantiate such a position verification protocol. As a result, we achieve classically ver…
The position of a device or agent is an important security credential in today's society, both online and in the real world. Unless in direct proximity, however, the secure verification of a position is impossible without further assumptions. This is true classically, but also in any future quantum-equipped communications infrastructure. We show in this work that minimal quantum resources, in the form of a single qubit, combined with classical communication are sufficient to thwart quantum adversaries that pretend to be at a specific position and have the ability to coordinate their action wit…
Bipartite and multipartite entangled states are basic ingredients for constructing quantum networks and their accurate verification is crucial to the functioning of the networks, especially for untrusted networks. Here we propose a simple approach for verifying the Bell state in an untrusted quantum network in which one party is not honest. Only local projective measurements are required for the honest party. It turns out each verification protocol is tied to a probability distribution on the Bloch sphere and its performance has an intuitive geometric meaning. This geometric picture enables us…
We present a methodology for the automated verification of quantum protocols using MCMAS, a symbolic model checker for multi-agent systems The method is based on the logical framework developed by D'Hondt and Panangaden for investigating epistemic and temporal properties, built on the model for Distributed Measurement-based Quantum Computation (DMC), an extension of the Measurement Calculus to distributed quantum systems. We describe the translation map from DMC to interpreted systems, the typical formalism for reasoning about time and knowledge in multi-agent systems. Then, we introduce dmc2i…
In this paper, we extend the protocol of classical verification of quantum computations (CVQC) recently proposed by Mahadev to make the verification efficient. Our result is obtained in the following three steps: $\bullet$ We show that parallel repetition of Mahadev's protocol has negligible soundness error. This gives the first constant round CVQC protocol with negligible soundness error. In this part, we only assume the quantum hardness of the learning with error (LWE) problem similar to the Mahadev's work. $\bullet$ We construct a two-round CVQC protocol in the quantum random oracle model (…
Recently it has been shown how the use of quantum entanglement can lead to the creation of real-time communication channels whose viability can be made location dependent. Such functionality leads to new security paradigms that are not possible in classical communication networks. Key to these new security paradigms are quantum protocols that can unconditionally determine that a receiver is in fact at an a priori assigned location. A limiting factor of such quantum protocols will be the decoherence of states held in quantum memory. Here we investigate the performance of quantum location verifi…
The posthoc verification protocol [J. F. Fitzsimons, M. Hajdu{\v s}ek, and T. Morimae, Physical Review Letters {\bf120}, 040501 (2018)] enables an information-theoretically-sound non-interactive verification of quantum computing, but the message from the prover to the verifier is quantum and the verifier has to do single-qubit measurements. The Mahadev protocol removes these quantum parts, but the soundness becomes the computational one. In this paper, we construct an information-theoretically-sound non-interactive classical verification protocol for quantum computing with a trusted center. Th…
We construct optimal protocols for verifying qubit and qudit GHZ states using local projective measurements. When the local dimension is a prime, an optimal protocol is constructed from Pauli measurements only. Our protocols provide a highly efficient way for estimating the fidelity and certifying genuine multipartite entanglement. In particular, they enable the certification of genuine multipartite entanglement using only one test when the local dimension is sufficiently large. By virtue of adaptive local projective measurements, we then construct protocols for verifying GHZ-like states that …
We present a classical interactive protocol that verifies the validity of a quantum witness state for the local Hamiltonian problem. It follows from this protocol that approximating the non-local value of a multi-player one-round game to inverse polynomial precision is QMA-hard. Our work makes an interesting connection between the theory of QMA-completeness and Hamiltonian complexity on one hand and the study of non-local games and Bell inequalities on the other.
Affleck-Kennedy-Lieb-Tasaki (AKLT) states are an important class of many-body quantum states that are useful in quantum information processing, including measurement-based quantum computation in particular. Here we propose a general approach for constructing efficient verification protocols for AKLT states on arbitrary graphs with local spin measurements. Our verification protocols build on bond verification protocols and matching covers (including edge coloring) of the underlying graphs, which have a simple geometric and graphic picture. We also provide rigorous performance guarantee that is …
We present two protocols for classical verification of quantum depth. Our protocols allow a purely classical verifier to distinguish devices with different quantum circuit depths even in the presence of classical computation. We show that a device with quantum circuit depth at most d will be rejected by the verifier even if the prover applies additional polynomial-time classical computation to cheat. On the other hand, the verifier accepts a device which has quantum circuit depth d' for some d'>d. In our first protocol, we introduce an additional untrusted quantum machine which shares entangle…
