Journal of Quantum Information Science

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

Surapol Rochanapratishtha, Wanchai Pijitrojana

Published Jan 1, 2015• 1 citation

Abstract

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.

DOI: 10.4236/jqis.2015.53012

Related papers

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.4504International Journal of Network Security & Its ApplicationsApr 12, 201019 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 ApplicationsOct 22, 201011 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, 20180 citations

Model Checking Quantum Key Distribution Protocols

Baichuan Huang, Yan Huang, Jiaming Kong +1 more

Quantum key distribution protocols use quantum information theories to guarantee the security of key exchange procedure, and model checking is a verification technique which could be used to test the security of it. In this paper, a new group quantum key distribution protocol is designed based on BB84 protocol, which is a possible solution to handle the security issue in communication between multi-users. Discrete time Markov chain and probabilistic computation tree logic are used to model the protocol procedure and verify its security properties in PRISM. Also, we provide the theoretical proof for this group protocol, which supports the model checking results from PRISM. Our study gives an insight into some of the major difficulties of quantum security protocol design and analysis.

International Conference on Information Technology in Medicine and EducationDec 1, 20165 citations

Simulating the BB84 Protocol

Kirti Kushwah, Akanksha Akanksha, Aniket Varshney +2 more

Abstract: Quantum Key Distribution (QKD) is a cryptographic technique that allows two parties to establish a secure communication channel by using the laws of quantum mechanics. The BB84 protocol is one of the earliest and most widely used QKD protocols that uses the properties of quantum entanglement and superposition to securely exchange cryptographic keys[3] . In this paper, we provide a detailed overview of the BB84 protocol and its implementation. We also discuss the security aspects of the protocol and its vulnerabilities. Finally, we conclude with a discussion of the future prospects and challenges in the field of quantum cryptography

International Journal for Research in Applied Science and Engineering TechnologyMay 29, 20230 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/0502048Feb 9, 200518 citations