Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Techniques for design and validation of quantum protocols

Nickolas K. Papanikolaou

Published Sep 11, 2026• 26 citations
Publisher

Abstract

Our objective in this thesis is to perform formal specification and automated validation of the class of protocols associated with quantum cryptography. Current analyses and proofs regarding quantum cryptographic protocols and their security are information-theoretic and also require in--depth understanding of the underlying physics. The alternative approach presented here involves the use of computer modelling languages and verification software. In particular, the logical model checker SPIN and the probabilistic model checker PRISM are used to analyse quantum key distribution, entanglement and quantum teleportation. The value of our approach lies not only in the fact that it is conceptually simpler than existing proofs, but in that it allows us to disambiguate protocol definitions and to assess their properties in various circumstances. By varying the values of certain parameters, different attacks on the protocols can be attempted and implementation-specific attributes can be analysed. The quantum key distribution protocol BB84 has been proved to be unconditionally secure against all types of eavesdropping. Although a general proof of this result is extremely hard to generate automatically, it is possible to develop specific protocol attacks and validate the protocol by computer. Assuming two types of eavesdropping attack (intercept-resend and random-substitute), we have used the PRISM tool to compute exactly the probability of successful eavesdropping, and found it to diminish as the number of transmitted qubits is increased. This result is linked to Mayers' security criteria for BB84. Also, we briefly describe a new quantum protocol definition language, named qSpec. The recent CQP process algebra, due to Nagarajan and Gay, is reviewed and examples of its application are provided. Alternative formalisms and validation tools are discussed, including QPAlg, PROBMELA and probUSM, the logic of knowledge and time for quantum systems due to Van der Meyden, and the QCSim simulator.

DOI
10.82444/warw.33642637

Related papers

Probabilistic Model--Checking of Quantum Protocols

Simon J. Gay, Rajagopal Nagarajan, Nickolas K. Papanikolaou

We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.

arXiv:quant-ph/0504007•Apr 1, 2005•54 citations

An Automated Analysis of the Security of Quantum Key Distribution

Rajagopal Nagarajan, Nickolas K. Papanikolaou, Garry Bowen +1 more

This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model-checking; we have used the PRISM model-checker to show that, as the number of qubits transmitted in BB84 is increased, the equivocation of the eavesdropper with respect to the channel decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. The results presented here are a testament to the effectiveness of the model-checking approach for systems where analytical solutions may not be possible or plausible.

arXiv:cs/0502048•Feb 9, 2005•18 citations

Specification and Verification of Quantum Protocols

Simon J. Gay, Rajagopal Nagarajan, Nickolas K. Papanikolaou

We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol. 11.1 Introduction Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose ( e.g. , linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).

Cambridge University Press eBooks•Nov 30, 2009•20 citations

APPLICATION OF FORMAL METHODS TO QUANTUM CRYPTOGRAPHY

貴大 久保田

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.

•Mar 24, 2014•0 citations

Modelling of Quantum Key Distribution Protocols in Communicating Quantum Processes Language with Verification and Analysis in PRISM

Satya Kuppam

Proof of security of cryptographic protocols theoretically establishes the strength of a protocol and the constraints under which it can perform, it does not take into account the overall design of the protocol. In the past model checking has been successfully applied to classical cryptographic protocols to weed out design flaws which would have otherwise gone unnoticed. Quantum cryptographic protocols differ from their classical counterparts, in their ability to detect the presence of an eavesdropper. Although unconditional security has been proven for both BB84 and B92 protocols, in this paper we show that identifying an eavesdropper's presence is constrained on the number of qubits exchanged. We first model the protocols in CQP and then explain the mechanism by which we have translated this into a PRISM model. We mainly focus on the protocols' ability to detect an active eavesdropper and the extent to which an eavesdropper can retrieve the shared key without being detected by either party. We then conclude by comparing the performance of the protocols.

arXiv:1612.03706•International Conference on Simulation and Modeling Methodologies, Technologies and Applications•Jan 1, 2018•12 citations

Analysis of the Security of BB84 by Model Checking

Mohamed Elboukhari, Mostafa Azizi, Abdelmalek Azizi

Quantum Cryptography or Quantum key distribution (QKD) is a technique that allows the secure distribution of a bit string, used as key in cryptographic protocols.When it was noted that quantum computers could break public key cryptosystems based on number theory extensive studies have been undertaken on QKD.Based on quantum mechanics, QKD offers unconditionally secure communication.Now, the progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years.Efforts are made to improve the performance and reliability of the implemented technologies.But several challenges remain despite this big progress.The task of how to test the apparatuses of QKD For example did not yet receive enough attention.These devises become complex and demand a big verification effort.In this paper we are interested in an approach based on the technique of probabilistic model checking for studying quantum information.Precisely, we use the PRISM tool to analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropping detection.We show that this property is affected by the parameters of quantum channel and the power of eavesdropper.

arXiv:1005.4504•International Journal of Network Security & Its Applications•Apr 12, 2010•19 citations
Our objective in this thesis is to perform formal specification and automated validation of the class of protocols associated with quantum cryptography. Current analyses and proofs regarding quantum cryptographic protocols and their security are information-theoretic and also require in--depth understanding of the underlying physics. The alternative approach presented here involves the use of computer modelling languages and verification software. In particular, the logical model checker SPIN and the probabilistic model checker PRISM are used to analyse quantum key distribution, entanglement and quantum teleportation. The value of our approach lies not only in the fact that it is conceptually simpler than existing proofs, but in that it allows us to disambiguate protocol definitions and to assess their properties in various circumstances. By varying the values of certain parameters, different attacks on the protocols can be attempted and implementation-specific attributes can be analysed. The quantum key distribution protocol BB84 has been proved to be unconditionally secure against all types of eavesdropping. Although a general proof of this result is extremely hard to generate automatically, it is possible to develop specific protocol attacks and validate the protocol by computer. Assuming two types of eavesdropping attack (intercept-resend and random-substitute), we have used the PRISM tool to compute exactly the probability of successful eavesdropping, and found it to diminish as the number of transmitted qubits is increased. This result is linked to Mayers' security criteria for BB84. Also, we briefly describe a new quantum protocol definition language, named qSpec. The recent CQP process algebra, due to Nagarajan and Gay, is reviewed and examples of its application are provided. Alternative formalisms and validation tools are discussed, including QPAlg, PROBMELA and probUSM, the logic of knowledge and time for quantum systems due to Van der Meyden, and the QCSim simulator.
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model-checking; we have used the PRISM model-checker to show that, as the number of qubits transmitted in BB84 is increased, the equivocation of the eavesdropper with respect to the channel decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. The results presented here are a testament to the effectiveness of the model-checking approach for systems where analytical solutions may not be possible or plausible.
We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol. 11.1 Introduction Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose ( e.g. , linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).
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.
Proof of security of cryptographic protocols theoretically establishes the strength of a protocol and the constraints under which it can perform, it does not take into account the overall design of the protocol. In the past model checking has been successfully applied to classical cryptographic protocols to weed out design flaws which would have otherwise gone unnoticed. Quantum cryptographic protocols differ from their classical counterparts, in their ability to detect the presence of an eavesdropper. Although unconditional security has been proven for both BB84 and B92 protocols, in this paper we show that identifying an eavesdropper's presence is constrained on the number of qubits exchanged. We first model the protocols in CQP and then explain the mechanism by which we have translated this into a PRISM model. We mainly focus on the protocols' ability to detect an active eavesdropper and the extent to which an eavesdropper can retrieve the shared key without being detected by either party. We then conclude by comparing the performance of the protocols.
Quantum Cryptography or Quantum key distribution (QKD) is a technique that allows the secure distribution of a bit string, used as key in cryptographic protocols.When it was noted that quantum computers could break public key cryptosystems based on number theory extensive studies have been undertaken on QKD.Based on quantum mechanics, QKD offers unconditionally secure communication.Now, the progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years.Efforts are made to improve the performance and reliability of the implemented technologies.But several challenges remain despite this big progress.The task of how to test the apparatuses of QKD For example did not yet receive enough attention.These devises become complex and demand a big verification effort.In this paper we are interested in an approach based on the technique of probabilistic model checking for studying quantum information.Precisely, we use the PRISM tool to analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropping detection.We show that this property is affected by the parameters of quantum channel and the power of eavesdropper.