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

Security and Communication Networks

Upgrade of a quantum scheme for authentication and key distribution along with a formal verification based on model checking technique

Aymen Ghilen, Mostafa Azizi, Ridha Bouallègue

Published Oct 26, 2016• 1 citation
Publisher

Abstract

Abstract In this paper, we review a previous research paper presenting a scheme for quantum key distribution that performs authentication using only quantum means. The authentication mechanism in the protocol runs along with an eavesdropping checking approach. To upgrade security properties, especially against man‐in‐the‐middle attack, we propose a revised and enhanced scheme, so that the probability of detecting eavesdropping is distinctly improved. We use prism tool as a model checker to analyze the security of the quantum system and to emphasize the extent of our contribution. We particularly focus on two security features: (i) the capability of the participants in the protocol to detect any eavesdropping attempt and (ii) any valid knowledge gained on the shared key must be minimized. Copyright © 2016 John Wiley & Sons, Ltd.

DOI
10.1002/sec.1666

Related papers

Integration and formal security analysis of a quantum key distribution scheme within CHAP protocol

Aymen Ghilen, Mostafa Azizi, Ridha Bouallègue

In a security context, to render a cryptosystem more resistant against man-in-the-middle and impersonation attacks, an authentication mechanism has to be considered. CHAP protocol (Challenge Handshake Authentication Protocol) is among the most widely spread authentication technique used within Local Area Networks. To offer greater robustness and privacy, we intend through our present paper to introduce a new quantum extension of CHAP that integrates quantum cryptography and takes advantage of its benefits such as eavesdropping detection, random secret key generation and unconditional security. A new scheme using a previously shared entangled qubits pairs with quantum unitary operators to ensure key agreement and mutual authentication is performed. To analyze the security of the proposed protocol, we use the PRISM tool as a model checker. We particularly focus on the security property of minimizing the quantity of information about the key that an enemy can obtain from applying a “man in the middle” attack. If we act on the parameters of the channel and the eavesdropper, we prove that this security property is affected by varying the efficiency of the channel as well as the power of the enemy. More interestingly, we show that the enemy could never be able to retrieve the value of the key.

IEEE/ACS International Conference on Computer Systems and Applications (AICCSA)•Nov 1, 2015•2 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

Techniques for design and validation of quantum protocols

Nickolas K. Papanikolaou

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.

•Sep 11, 2026•26 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

Verification Of Quantum Cryptography Protocols By Model Checking

Mostafa Azizi and Abdelmalek Azizi Mohamed Elboukhari

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.

•Jul 19, 2018•0 citations

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
Abstract In this paper, we review a previous research paper presenting a scheme for quantum key distribution that performs authentication using only quantum means. The authentication mechanism in the protocol runs along with an eavesdropping checking approach. To upgrade security properties, especially against man‐in‐the‐middle attack, we propose a revised and enhanced scheme, so that the probability of detecting eavesdropping is distinctly improved. We use prism tool as a model checker to analyze the security of the quantum system and to emphasize the extent of our contribution. We particularly focus on two security features: (i) the capability of the participants in the protocol to detect any eavesdropping attempt and (ii) any valid knowledge gained on the shared key must be minimized. Copyright © 2016 John Wiley & Sons, Ltd.
In a security context, to render a cryptosystem more resistant against man-in-the-middle and impersonation attacks, an authentication mechanism has to be considered. CHAP protocol (Challenge Handshake Authentication Protocol) is among the most widely spread authentication technique used within Local Area Networks. To offer greater robustness and privacy, we intend through our present paper to introduce a new quantum extension of CHAP that integrates quantum cryptography and takes advantage of its benefits such as eavesdropping detection, random secret key generation and unconditional security. A new scheme using a previously shared entangled qubits pairs with quantum unitary operators to ensure key agreement and mutual authentication is performed. To analyze the security of the proposed protocol, we use the PRISM tool as a model checker. We particularly focus on the security property of minimizing the quantity of information about the key that an enemy can obtain from applying a “man in the middle” attack. If we act on the parameters of the channel and the eavesdropper, we prove that this security property is affected by varying the efficiency of the channel as well as the power of the enemy. More interestingly, we show that the enemy could never be able to retrieve the value of the key.
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.
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.
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.
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.