International Conference on Information Technology in Medicine and Education

Model Checking Quantum Key Distribution Protocols

Baichuan Huang, Yan Huang, Jiaming Kong, Xin Huang

Published Dec 1, 2016• 5 citations

Abstract

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.

DOI: 10.1109/itme.2016.0144

Related papers

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

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

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 ScienceJan 1, 20151 citation

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

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, 202626 citations