This thesis presents a formal model for quantum protocols, that is, cryptographic protocols based on quantum mechanics. It also develops a definition of security (which includes notions such as privacy and correctness) for quantum protocols.
First, existing classical (non-quantum) definitions of security are studied. There are essentially two approaches: one based on Turing Machines and simulation, the other using information theory. Both approaches are explored in detail and compared, then a particular variation of the first approach is chosen. Security is defined by introducing an interface (also called a simulator) which is capable of translating an attack on protocol 1 into an attack on protocol 2. The profile of a protocol is a stochastic variable, defined as the output of the participants and the view of the adversary who performs the attack. If an interface exists such that the profile of protocol 1 is indistinguishable from the profile of protocol 2 with the help of this interface, then protocol 1 is at least as secure as protocol 2. An absolute notion of security is obtained by comparing the protocol implementation with its 'ideal' equivalent.
In this approach, and in classical cryptography in general, indistinguishability of probability distributions is a crucial tool. The meaning of this notion is explored in the context of density matrices, the mathematical formalism which is used to describe the state of a quantum system. Various measures of distinguishability of quantum states relevant from a cryptographic point of view are investigated: probability of error, trace norm (related to the Kolmogorov distance), overlap (related to the Bhattacharyya coefficient) and Shannon distinguishability (defined through the mutual information). It is shown that if we require that the distinguishability between two families of quantum states vanish exponentially fast, these four distinguishability measures are equivalent.
Along the way upper and lower bounds for the Shannon distinguishability are obtained. This is a very useful result, because explicit computation of the Shannon distinguishability between two quantum states is often difficult (it requires solving a transcendental equation), whereas the other distinguishability measures, in particular the trace norm, are usually much easier to compute.
In the last chapter the two previous topics are combined. A formal model for quantum protocols is formulated. It uses Quantum Turing Machines to represent the participants, who communicate through a quantum channel. The different nature of quantum information as opposed to classical information is explored in detail, including the implications this has for the definition. As in the classical case, we introduce an interface to compare the security of two protocols for the same task. Subsequently some consequences of the proposed definition are investigated. In particular, strong evidence is given that one classical technique often used in proofs of security for classical protocols, called rewinding, is impossible in the quantum setting.
This thesis presents a formal model for quantum protocols, that is, cryptographic protocols based on quantum mechanics. It also develops a definition of security (which includes notions such as privacy and correctness) for quantum protocols.
First, existing classical (non-quantum) definitions of security are studied. There are essentially two approaches: one based on Turing Machines and simulation, the other using information theory. Both approaches are explored in detail and compared, then a particular variation of the first approach is chosen. Security is defined by introducing an interface (also called a simulator) which is capable of translating an attack on protocol 1 into an attack on protocol 2. The profile of a protocol is a stochastic variable, defined as the output of the participants and the view of the adversary who performs the attack. If an interface exists such that the profile of protocol 1 is indistinguishable from the profile of protocol 2 with the help of this interface, then protocol 1 is at least as secure as protocol 2. An absolute notion of security is obtained by comparing the protocol implementation with its 'ideal' equivalent.
In this approach, and in classical cryptography in general, indistinguishability of probability distributions is a crucial tool. The meaning of this notion is explored in the context of density matrices, the mathematical formalism which is used to describe the state of a quantum system. Various measures of distinguishability of quantum states relevant from a cryptographic point of view are investigated: probability of error, trace norm (related to the Kolmogorov distance), overlap (related to the Bhattacharyya coefficient) and Shannon distinguishability (defined through the mutual information). It is shown that if we require that the distinguishability between two families of quantum states vanish exponentially fast, these four distinguishability measures are equivalent.
Along the way upper and lower bounds for the Shannon distinguishability are obtained. This is a very useful result, because explicit computation of the Shannon distinguishability between two quantum states is often difficult (it requires solving a transcendental equation), whereas the other distinguishability measures, in particular the trace norm, are usually much easier to compute.
In the last chapter the two previous topics are combined. A formal model for quantum protocols is formulated. It uses Quantum Turing Machines to represent the participants, who communicate through a quantum channel. The different nature of quantum information as opposed to classical information is explored in detail, including the implications this has for the definition. As in the classical case, we introduce an interface to compare the security of two protocols for the same task. Subsequently some consequences of the proposed definition are investigated. In particular, strong evidence is given that one classical technique often used in proofs of security for classical protocols, called rewinding, is impossible in the quantum setting.
In general, it is difficult to verify security of cryptographic protocols.Indeed, flaws of designs and security proofs of some protocols were found after they had been presented.In deductive verification using formal methods, protocols and security properties are described in formal languages, and correctness of designs and security proofs are deduced by inference rules.While a number of formal frameworks and verification tools have been developed and applied to classical protocols, few formal methods have been applied to security proofs of quantum protocols.The contributions of this thesis consist of the following three results.First, we developed a software tool to verify bisimilarity of configurations (pairs of processes and quantum states) of qCCS, a quantum process calculus presented by Feng et al.Bisimilar configurations behave indistinguishably from the outside.We designed a formal framework for the verifier, which we call nondeterministic qCCS, on the basis of qCCS by Feng et al.While the transition system of qCCS is both nondeterministic and probabilistic, we presented a nondeterministic and non-probabilistic transition system for configurations, extending the definition of them.This allows the verifier to verify bisimilarity efficiently.Next, we designed the verifier to handle security parameters and quantum states symbolically.A purpose is to apply it to quantum cryptographic protocols, where the dimensions of quantum states depend on security parameters.When the verifier checks bisimulation relation of configurations, it uses user-defined equations on the symbolic representations to check the quantum states that the outsider can access are always equal.Besides, the verifier is sound with respect to qCCS, that is, when it runs with two configurations as input and returns true, a symbol representing success of the verification, the configurations are in bisimulation relation in the qCCS's definition.Second, we defined a notion of approximate bisimulation relation on configurations of nondeterministic qCCS, and extended the verifier to check the approximate bisimilarity.Approximately bisimilar configurations reveal quantum states with close trace distance to the outsider after transitions.This property is useful in security proofs of quantum key distribution protocols.We then proved the approximate bisimulation relation is closed under application of evaluation contexts of processes.Third, we formally verified Shor and Preskill's security proof of BB84 quantum key distribution protocol.They first considered another protocol (the EDP-based protocol) and proved the security of BB84 and the EDP-based protocol is equivalent.They next proved the latter is secure.For the first step of their proof, we formalized the two protocols as configurations and formally verified that they are bisimilar.For the second step, we defined a completely secure protocol (EDPideal) and formally verified that the configurations of it and the EDP-based protocol are approximately bisimilar.This is the first work where a security proof of a quantum cryptographic protocol is mechanically verified using a software tool.
This paper, mostly expository in nature, surveys four measures of distinguishability for quantum-mechanical states. This is done from the point of view of the cryptographer with a particular eye on applications in quantum cryptography. Each of the measures considered is rooted in an analogous classical measure of distinguishability for probability distributions: namely, the probability of an identification error, the Kolmogorov distance, the Bhattacharyya coefficient, and the Shannon (1948) distinguishability (as defined through mutual information). These measures have a long history of use in statistical pattern recognition and classical cryptography. We obtain several inequalities that relate the quantum distinguishability measures to each other, one of which may be crucial for proving the security of quantum cryptographic key distribution. In another vein, these measures and their connecting inequalities are used to define a single notion of cryptographic exponential indistinguishability for two families of quantum states. This is a tool that may prove useful in the analysis of various quantum-cryptographic protocols.
The emergence of quantum computing has provided new paradigms for cryptography. On the one hand, it poses significant new threats to existing classically cryptographic systems, requiring the community to define new security models that capture what a quantum adversary can do. On the other hand, it gives us new tools to design cryptographic protocols, with weaker assumptions than in the classical world, or even protocols that are impossible classically. In this survey, we first give an overview of new security definitions for classical cryptography, considering quantum adversaries who can either only use local quantum computation (post-quantum security), or even send quantum messages and in particular have access to oracle in superposition (quantum security). We explore these new notions through the examples of commitments, zero-knowledge proofs, encryption, and signatures. Then, we present what is arguably the most famous application of quantum cryptography: quantum key distribution (QKD) protocols that take advantage of unique properties of quantum mechanics to provide secure communication unconditionally. We also explore cryptography beyond QKD, focusing on unclonable cryptography: a family of cryptographic functionalities, built with quantum states, and designed to be resistant to counterfeit by leveraging the “no-cloning” theorem. We examine in particular quantum money, but also the recent notions of unclonable encryption and copy-protection, including related variants. By presenting a comprehensive survey of these topics, this paper aims to provide a thorough understanding of the current landscape and future potential of quantum cryptography.
Abstract Quantum computing promises unprecedented computational power, posing fundamental threats and offering novel solutions to modern cryptography and cybersecurity. This survey paper reviews the rapidly evolving landscape of quantum-resistant and quantum-native security protocols. By analyzing foundational computational security models and the unique vulnerabilities introduced by quantum algorithms, this work proposes a structured evaluation framework for assessing the robustness of cryptographic systems. Ultimately, this survey highlights the critical transition from classical cryptographic infrastructures to quantum-secure paradigms, ensuring data confidentiality and integrity in the post-quantum era. Keywords: Quantum Computing, Security Protocol, Vulnerabilities 1.Introduction The emergence of quantum computing represents a paradigm shift in both computational physics and information technology. Quantum algorithms, particularly Shor's and Grover's algorithms, inherently challenge the mathematical foundations of classical public-key cryptography. As a result, securing communication channels against quantum-empowered adversaries has become an urgent priority for global infrastructure and national security. The motivation for this survey stems from the immediate need to bridge the gap between theoretical quantum mechanics and applied cybersecurity, ensuring that secure communications can withstand the computational leaps expected in the next decade. The core problem addressed in this paper is the comprehensive evaluation of security protocols under the threat model of a fully scalable quantum computer. The scope encompasses both post-quantum cryptographic (PQC) protocols and inherently quantum protocols, such as those relying on physical quantum states for key distribution. Existing classical approaches are insufficient for two main reasons. First, classical computational security models often rely on mathematical hardness assumptions (like integer factorization) that are rapidly undermined by theoretical quantum algorithms. Second, current software tools for designing secure classical protocols fail to account for quantum state phenomena, such as superposition and entanglement, rendering classical verification methods inadequate for quantum threat models. To address these structural challenges, this paper presents the following contributions: We provide a comprehensive taxonomy of vulnerabilities in both classical and quantum security protocols, mapping specific algorithmic advantages to protocol failure points. We propose a structured, multi-module framework for simulating, attacking, and verifying the security of hybrid quantum-classical cryptographic architectures. 2.Foundations of Classical Protocol Analysis The rigorous analysis of security protocols has traditionally relied on well-defined computational and symbolic models (Toorani, 2016). Researchers have extensively mapped out the taxonomy of attacks on authenticated key exchange (AKE) protocols and password-authenticated key exchange (PAKE) systems, establishing the mathematical groundwork for secure communication. The core idea of these foundational works is to establish provable security bounds that distinguish between information-theoretic and computational security. While this traditional paradigm offers strong mathematical guarantees against classical adversaries, its primary weakness is the failure to incorporate quantum attack vectors into the adversary's capability profile. Our work builds upon these classical models by explicitly injecting quantum algorithmic capabilities into standard protocol verification routines. 2.1.Quantum Algorithm Development and Simulation A significant body of literature focuses on the theoretical development and computational simulation of quantum algorithms capable of compromising or enhancing network security. Academic overviews have formalized algorithms like Grover's and Shor's, demonstrating their theoretical efficiency over classical counterparts in breaking cryptographic primitives. Furthermore, researchers have developed advanced design automation tools, such as decision diagrams, to simulate and verify complex quantum circuits. The strength of these simulation tools lies in their ability to model complex quantum states without requiring expensive physical hardware. However, a notable weakness is that they often abstract away the physical noise and hardware constraints that exist in real-world cryptographic deployments. This survey contextualizes these simulation techniques specifically within the framework of adversarial security testing, bridging theoretical algorithms with practical protocol defense. 3.Physical Implementations and Hardware Considerations Beyond algorithmic theory, the physical realization of quantum states directly impacts the practical security of any quantum protocol. Research into cavity quantum electrodynamics (QED) has demonstrated the complete mathematical construction of fundamental quantum gates, such as the controlled-controlled NOT gate, operating in the weak coupling regime (Fujii et al., 2005). Additionally, methods like Quantum Computed Moments (QCM) address the hardware constraints and noise typical of Near-Term Intermediate Scale Quantum (NISQ) devices, estimating ground state properties even with suboptimal trial states. The strength of this hardware-focused research is its realism regarding current technological limits; however, it often lacks a direct bridge to high-level network protocol verification. Compared to these purely physical studies, our survey integrates physical noise models into a generalized, software-driven protocol verification framework. 4.Approach To systematically evaluate quantum computing security protocols, we propose a structured Quantum Protocol Verification Framework (QPVF). The first module is the "Threat Modeling Engine," which defines the adversary's capabilities, ranging from classical data interception to full quantum memory manipulation. The second module is the "Quantum Circuit Synthesizer," which leverages decision diagram-based tools to translate high-level cryptographic operations into verifiable quantum circuits. The final module is the "Vulnerability Analyzer," which subjects the synthesized circuits to simulated quantum attacks, effectively distinguishing between idealized computational security and realistic hardware-constrained security. This modular pipeline allows security engineers to isolate specific vulnerabilities at both the abstract algorithmic layer and the simulated physical implementation layer. A key design choice in the QPVF is the utilization of decision diagrams for circuit simulation. This choice is predicated on the fact that decision diagrams efficiently handle the exponential state space of quantum systems during complex verification tasks (Wille et al., 2021). Furthermore, our framework explicitly incorporates noise models derived from current NISQ hardware limitations, ensuring that the security evaluation reflects realistic physical constraints rather than purely idealized environments (Vallury & Hollenberg, 2023). To evaluate this framework, we propose a hypothetical benchmarking plan using an artificially generated dataset of 10,000 hybrid quantum-classical cryptographic key exchanges. We will measure the success rate of simulated Grover-based brute-force attacks against varying key sizes and simulated environmental noise levels. This evaluation will compare the theoretical vulnerability threshold of a protocol against the practical threshold observed when quantum noise severely degrades the adversary's computational capabilities. The operational flow of the QPVF is designed to provide end-to-end security verification for next-generation networks. It bridges the critical gap between abstract protocol design and simulated hardware execution. The methodology can be summarized by the following numbered pipeline: Protocol Ingestion: The classical or quantum protocol is parsed into a standardized symbolic representation. Adversary Assignment: The user assigns a precise computational profile, selecting between traditional classical algorithms or advanced quantum capabilities. Circuit Generation: Protocol steps are mapped to equivalent quantum decision diagrams for scalable software simulation. Execution & Attack: Simulated quantum algorithms are executed against the mapped circuits to test for cryptographic resilience. Output Generation: The system outputs a vulnerability score and highlights specific failure points caused by either algorithmic weaknesses or simulated hardware noise. 5.Discussion The transition to quantum-secure protocols carries profound practical implications for global information infrastructure and enterprise deployment. Deploying these advanced protocols requires immense updates to existing software toolkits, as current digital systems are not fundamentally designed to handle the complexity of quantum states. Furthermore, organizations must consider the massive educational and workforce development efforts needed to train software engineers in quantum cryptography, a requirement already highlighted by international hackathons and educational initiatives. Integrating quantum-resistant protocols into complex domains like high-energy physics networks or global banking systems will require bridging the gap between theoretical quantum mechanics and applied computer engineering. Consequently, practical deployment must occur in hybrid phases, maintaining classical cryptographic wrappers while dedicated quantum infrastructure matures. Despite the robust theoretical design of proposed quantum security frameworks, several limitations and failure modes persist in practical applications. First, physical implementation attacks, such as side-channel attacks on the lasers and cavities used in physical quantum gates can bypass theoretical software security guarant
We call quantum security the area of IT security dealing with scenarios where one or more parties have access to quantum hardware. This encompasses both the fields of post-quantum cryptography (that is, traditional cryptography engineered to be resistant against quantum adversaries), and quantum cryptography (that is, security protocols designed to be natively run on a quantum infrastructure, such as quantum key distribution). Moreover, there exist also hybrid models, where traditional cryptographic schemes are somehow `mixed' with quantum operations in certain scenarios. Even if a fully-fledged, scalable quantum computer has yet to be built, recent results and the pace of research in its realization call for attention, lest we suddenly find ourselves one day with an obsolete security infrastructure. For this reason, in the last two decades research in quantum security has experienced an exponential growth in interest and investments. In this work, we propose the first systematic classification of quantum security scenarios, and for each of them we recall the main tools and results, as well as presenting new ones. We achieve this goal by identifying four distinct quantum security classes, or domains, each of them encompassing the security notions and constructions related to a particular scenario. We start with the class QS0, which is `classical cryptography' (meaning that no quantum scenario is considered), where we present some classical constructions and results as a preliminary step. Regarding post-quantum cryptography, we introduce the class QS1, where we discuss in detail the problems arising when designing a classical cryptographic object meant to be resistant against adversaries with local quantum computing power, and we provide a classification of the possible quantum security reductions in this scenario when considering provable security. Moreover, we present results about the quantum security and insecurity of the Fiat-Shamir transformation (a useful tool used to turn interactive identification schemes into digital signatures), and ORAMs (protocols used to outsource a database in a private way). In respect to hybrid classical-quantum models, in the security class QS2 we discuss in detail the possible scenarios where these scenarios arise, and what a correct formalization should be in terms of quantum oracle access. We also provide a novel framework for the quantum security (both in terms of indistinguishability and semantic security) of secret-key encryption schemes, and we give explicit secure constructions, as well as impossibility results. Finally, in the class QS3 we consider all those cryptographic constructions designed to run natively on quantum hardware. We give constructions for quantum encryption schemes (both in the secret- and public-key scenario), and we introduce transformations for obtaining such schemes by conceptually simpler schemes from the class QS2. Moreover, we introduce a quantum version of ORAM, called quantum ORAM (QORAM), aimed at outsourcing in a private way a database composed of quantum data. In proposing a suitable security model and an explicit construction for QORAMs, we also introduce a technique of independent interest which models a quantum adversary able to extract information from a quantum system without disturbing it `too much'. We believe that the framework we introduce in this work will be a valuable tool for the scientific community in addressing the challenges arising when formalizing sound constructions and notions of security in the quantum world.
The ability to transfer information securely is essential in the modern world we live in. While the field of cryptography has long researched ways to do this, events over the last couple of years have brought the issues of secure information transfer squarely into the public eye. As a consequence, security and cryptography have quickly become issues of social and political importance, sparking debates about the values of privacy and the role of government. An essential ingredient of modern cryptography is the generation of randomness: cryptographic techniques are built on the premise that one has access to random bits. It is well known, however, that computers cannot produce algorithmically random sequences – that is, sequences with maximal algorithmic information content – but are doomed to produce ‘pseudorandomness’. This lack of randomness can be, and has been, exploited to compromise security, see [4]. The active field of quantum information theory has proposed approaches to provide supposedly ‘unbreakable’ security by exploiting various quantum phenomena. This security unfortunately relies on assumptions about the nature of quantum measurements and their ability to generate random bits. Anton Zeilinger summarises this by postulating that the simplest quantum systems, qubit, can hold only one bit of classical information [6]. This foundational principle is in line with a wider paradigm shift to view quantum information as an extension of classical information, but it is nonetheless unsatisfying to simply postulate this principle, given its importance in determining the practical advantages of quantum information theory. In order to understand better how quantum mechanics can help generate meaningful information, we instead look to relate the outcomes of quantum measurements to formal properties of the system based on more fundamental assumptions. Indeed, we have shown that a) some of the postulated properties of quantum information follow from the formal structure of the theory and b) a purely formal notion of information within a quantum world can generate, via measurement, meaningful and useful information in the macroscopic world (for example, in cryptography). The indeterminism of quantum measurements can be formalised via the notion of value indefiniteness. To explain this concept, let us consider an arbitrary quantum system and ask whether the outcome of a measurement of any observable quantity A (such as the energy of the system, its angular momentum (spin), etc.) is determined prior to the measurement. If this is the case, then we say the observable is value definite with value v(A); otherwise, the observable is value indefinite and v(A) is undefined. Mathematically, one can reduce all observable quantities to so-called projection observables, which can only take the values 0 or 1. Thus, the question of whether the outcome of several measurements can be simultaneously determined in advance can be rephrased in terms of the information ‘carried’ by a particular system in a definite quantum state. Classically, one expects that all quantities are determined in advance, and hence all observables are value definite. Quantum mechanically, however, the belief is that this is not the case, and the information content of quantum systems is limited. Formulating carefully the notion of value indefiniteness allows us to formalise the notion of (quantum) indeterminism; however, this doesn’t help clarify whether quantum systems are indeed value indefinite or not. Staying in this formal framework, the Kochen-Specker theorem [5] provides a first positive result, showing that at least some observables must be value indefinite if one makes the assumption known as non-contextuality, which states that any definite values that exist must be independent of other compatible measurements that may or may not be performed on the system. Under the same assumption, this theorem can be strengthened to show that only one single observable can have the definite value 1 (see [2]). Furthermore, only observables that can be measured simultaneously with this single one can have the definite value 0; the rest must all be value indefinite. Since the preparation of a system involves precisely ensuring that, usually via measurement, the system is in a definite state with respect to some desired observable, this result shows that no other incompatible observable can be value definite. That is, preparing a system in a definite state by making the ‘preparation’ observable value definite specifies completely the information content of the quantum system. This is an example of syntactical quantum information acquiring meaning at the level of the quantum itself. Can the syntactical information at the level of the quantum generate meaning outside the quantum, that is, at the macroscopic level? The results cited above hold in the Hilbert-space framework of quantum mechanics and are formulated only in terms of a syntactical notion of information. Their real importance becomes evident when one interprets them in the context of quantum measurements. Specifically, if we prepare a quantum system in a known state, they allow us to ‘locate’ observables which we can measure, but which are value indefinite; that is, observables whose measurement results are not specified by any pre-existing property of the quantum system. Furthermore, with respect to a mathematical model of unpredictability which we developed in [3], the results of these measurements can be shown to be absolutely unpredictable. In this way we get a mathematical explanation and justification of the largely accepted intuition that quantum mechanics is inherently unpredictable, and that this unpredictability arises from the phenomenon of indefiniteness within the quantum world. Furthermore, if one considers a hypothetical infinite sequence generated by the repeated measurement of a quantum value indefinite observable, one can prove that these sequences must be strongly incomputable, technically ‘bi-immune’ [1]. Such sequences cannot be generated by any Turing machine or classical computer, showing that value indefiniteness leads to a clear classical/quantum split in a purely algorithmic context. Importantly, bi-immunity is a property of observed, macroscopic quantities, quite separate from the quantum framework in which the value indefiniteness is formalised. This form of macroscopic meaning created from the lack of syntactic information is precisely the scenario that quantum random number generators try to create, and which is essential for the development and certification of quantum cryptographic systems. The fact that the macroscopic information created goes beyond anything classically obtainable serves as a valuable practical resource, outside of and removed from the quantum formalism. To conclude, quantum information creates meaning within the quantum and via measure- ment, the lack of information within the quantum, creates meaning and valuable information at the macroscopic level. Acknowledgments The second author thanks Prof. S. Marcus for useful conversations on quantum information theory. This work was supported in part by Marie Curie FP7-PEOPLE-2010-IRSES Grant RANPHYS. References and Notes Abbott, A.A.; Calude, C.S.; Svozil, K. Strong Kochen-Specker theorem and incomputability of quantum randomness. Physical Review A 2012, 86, 062109. Abbott, A.A.; Calude, C.S.; Svozil, K. Value-indefinite observables are almost everywhere. Physical Review A 2013, 89, 032109. Abbott, A.A.; Calude, C.S.; Svozil, K. On the unpredictability of individual quantum measurement outcomes. CDMTCS Research Report 2014, 458. Calude, C.S. Quantum randomness & cryptology. CyberTalk 2013, 3, 42–43. Kochen, S.; Specker, E. The problem of hidden variables in quantum mechanics. Journal of Mathematics and Mechanics 1967, 17, 59–87. Zeilinger, A. A foundational principle for quantum mechanics. Foundations of Physics 1999, 29(4),631–643.