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

Verification Of Quantum Cryptography Protocols By Model Checking

Mostafa Azizi and Abdelmalek Azizi Mohamed Elboukhari

Published Jul 19, 2018• 0 citations
Publisher

Abstract

Unlike classical cryptography which is based on mathematical functions, Quantum Cryptography or Quantum Key Distribution (QKD) exploits the laws of quantum physics to offer unconditionally secure communication. The progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years and efforts are made to improve the performance and reliability of the implemented technologies. But despite this big progress, several challenges remain. For example the task of how to test the devices of QKD did not yet receive enough attention. These apparatuses become heterogeneous, complex and so demand a big verification effort. In this paper we propose to study quantum cryptography protocols by applying the technique of probabilistic model checking. Using PRISM tool, we analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropper's information gain on the key derived from the implementation of this protocol. We show that this property is affected by the parameters of the eavesdropper’s power and the quantum channel.

DOI
10.5281/zenodo.1315476

Related papers

Verification of Quantum Cryptography Protocols by Model Checking

Mohamed Elboukhari, Mostafa Azizi, Abdelmalek Azizi

Unlike classical cryptography which is based on mathematical functions, Quantum Cryptography or Quantum Key Distribution (QKD) exploits the laws of quantum physics to offer unconditionally secure communication.The progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years and efforts are made to improve the performance and reliability of the implemented technologies.But despite this big progress, several challenges remain.For example the task of how to test the devices of QKD did not yet receive enough attention.These apparatuses become heterogeneous, complex and so demand a big verification effort.In this paper we propose to study quantum cryptography protocols by applying the technique of probabilistic model checking.Using PRISM tool, we analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropper's information gain on the key derived from the implementation of this protocol.We show that this property is affected by the parameters of the eavesdropper's power and the quantum channel.

International Journal of Network Security & Its Applications•Oct 22, 2010•11 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

Analysis of Security of Quantum Key Distribution Based on Entangled Photon Pairs by Model Checking

Surapol Rochanapratishtha, Wanchai Pijitrojana

Quantum key distribution is a technique to securely distribute a bit string between two parties by using the laws of quantum mechanics. The security of this technique depends on the basis of quantum mechanics rather than the difficulty of the mathematical calculation as in the classical encoding. Researches in this field have shown that the quantum key distribution will be fully functioning outside the laboratory in a few years. Due to the complexity and the high efficiency of the device, the verification is needed. In this article, we use PRISM to verify the security of the quantum key distribution protocol, which uses the entangled photon based on BB84 protocol.

Journal of Quantum Information Science•Jan 1, 2015•1 citation

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

Probabilistic Model-Checking of Quantum Protocols (Extended Abstract)

Rajagopal Nagarajan, Nickolas K. Papanikolaou

In the 1980s it was first realized that quantum–mechanical phenomena can be exploited directly for the manipulation, storage and transmission of information. The discovery of quantum algorithms for prime factorization [18] and unstructured search [7], which outperformed the best classical algorithms for these tasks significantly, opened up new vistas for computer science and gave an initial thrust to the emerging field of quantum computation. To implement a quantum algorithm, however, a large scale quantum computer is necessary and such a device has yet to be built. Research in quantum information, on the other hand, has shown that quantum effects can be harnessed to provide efficient and highly secure communication channels, which can be built using current technology. Entangled quantum states, superpositions and quantum measurement are among the characteristics of the subatomic world which nature puts at our disposal; these and related phenomena enable the development of novel techniques for computation and communication with no rival in classical computing and communication theory. The focus in this paper is on communication protocols involving the use of such phenomena. Quantum protocols have particularly important applications in cryptography. Several quantum protocols have been proposed for cryptographic tasks such as oblivious transfer, bit commitment and key distribution [8,13]. The BB84 protocol for quantum key distribution [2,14], which allows two users to establish a common secret key using a single quantum channel, has been shown to be unconditionally secure against all attacks [11]. Other quantum protocols include procedures for

•Jan 1, 2005•0 citations

Increasing the Protocol Gain of Quantum Cryptography

Firas A. Al-Juboori, Noor Kareem Juma, a Al-Mandilawi

Quantum cryptography is a technique to distribute a sequence of truly random and unconditionally secure bits over a secure communication by applying the phenomena of quantum physics. The distributed secret bits perform the secret key which is used later to encrypt messages with an encryption algorithm, usually the One-Time-Pad is used. Quantum Key Distribution solves the security problem in classical cryptography by depending on the laws of physics which is focusing on the physics of information. Quantum protocol gain usually is low due to the quantum channel noise and the difference between the photon polarization at the sender and receiver side; in this research, a method is proposed to increase the protocol gain without decreasing the security level of quantum key. BB84 quantum key distribution algorithm is implemented and simulated with MATLAB R2010a simulation; and a comparison is made with A. Singh and N. Sharma [14] results.

Engineering and Technology Journal•Sep 1, 2013•0 citations
Unlike classical cryptography which is based on mathematical functions, Quantum Cryptography or Quantum Key Distribution (QKD) exploits the laws of quantum physics to offer unconditionally secure communication. The progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years and efforts are made to improve the performance and reliability of the implemented technologies. But despite this big progress, several challenges remain. For example the task of how to test the devices of QKD did not yet receive enough attention. These apparatuses become heterogeneous, complex and so demand a big verification effort. In this paper we propose to study quantum cryptography protocols by applying the technique of probabilistic model checking. Using PRISM tool, we analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropper's information gain on the key derived from the implementation of this protocol. We show that this property is affected by the parameters of the eavesdropper’s power and the quantum channel.
Unlike classical cryptography which is based on mathematical functions, Quantum Cryptography or Quantum Key Distribution (QKD) exploits the laws of quantum physics to offer unconditionally secure communication.The progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years and efforts are made to improve the performance and reliability of the implemented technologies.But despite this big progress, several challenges remain.For example the task of how to test the devices of QKD did not yet receive enough attention.These apparatuses become heterogeneous, complex and so demand a big verification effort.In this paper we propose to study quantum cryptography protocols by applying the technique of probabilistic model checking.Using PRISM tool, we analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropper's information gain on the key derived from the implementation of this protocol.We show that this property is affected by the parameters of the eavesdropper's power and the quantum channel.
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.
Quantum key distribution is a technique to securely distribute a bit string between two parties by using the laws of quantum mechanics. The security of this technique depends on the basis of quantum mechanics rather than the difficulty of the mathematical calculation as in the classical encoding. Researches in this field have shown that the quantum key distribution will be fully functioning outside the laboratory in a few years. Due to the complexity and the high efficiency of the device, the verification is needed. In this article, we use PRISM to verify the security of the quantum key distribution protocol, which uses the entangled photon based on BB84 protocol.
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.
In the 1980s it was first realized that quantum–mechanical phenomena can be exploited directly for the manipulation, storage and transmission of information. The discovery of quantum algorithms for prime factorization [18] and unstructured search [7], which outperformed the best classical algorithms for these tasks significantly, opened up new vistas for computer science and gave an initial thrust to the emerging field of quantum computation. To implement a quantum algorithm, however, a large scale quantum computer is necessary and such a device has yet to be built. Research in quantum information, on the other hand, has shown that quantum effects can be harnessed to provide efficient and highly secure communication channels, which can be built using current technology. Entangled quantum states, superpositions and quantum measurement are among the characteristics of the subatomic world which nature puts at our disposal; these and related phenomena enable the development of novel techniques for computation and communication with no rival in classical computing and communication theory. The focus in this paper is on communication protocols involving the use of such phenomena. Quantum protocols have particularly important applications in cryptography. Several quantum protocols have been proposed for cryptographic tasks such as oblivious transfer, bit commitment and key distribution [8,13]. The BB84 protocol for quantum key distribution [2,14], which allows two users to establish a common secret key using a single quantum channel, has been shown to be unconditionally secure against all attacks [11]. Other quantum protocols include procedures for
Quantum cryptography is a technique to distribute a sequence of truly random and unconditionally secure bits over a secure communication by applying the phenomena of quantum physics. The distributed secret bits perform the secret key which is used later to encrypt messages with an encryption algorithm, usually the One-Time-Pad is used. Quantum Key Distribution solves the security problem in classical cryptography by depending on the laws of physics which is focusing on the physics of information. Quantum protocol gain usually is low due to the quantum channel noise and the difference between the photon polarization at the sender and receiver side; in this research, a method is proposed to increase the protocol gain without decreasing the security level of quantum key. BB84 quantum key distribution algorithm is implemented and simulated with MATLAB R2010a simulation; and a comparison is made with A. Singh and N. Sharma [14] results.