Journal of Quantum Information Science, 2015, 5, 103108 Published Online September 2015 in SciRes. http://www.scirp.org/journal/jqis http://dx.doi.org/10.4236/jqis.2015.53012 How to cite this paper: Rochanapratishtha, S. and Pijitrojana, W. (2015) Analysis of Security of Quantum Key Distribution Based on Entangled Photon Pairs by Model Checking. Journal of Quantum Information Science, 5, 103108. http://dx.doi.org/10.4236/jqis.2015.53012 Analysis of Security of Quantum Key Distribution Based on Entangled Photon Pairs by Model Checking Surapol Rochanapratishtha, Wanchai Pijitrojana Department of Electrical and Computer Engineering, Faculty of Engineering, Thammasat University, Bangkok, Thailand Email: r.surapol@gmail.co m, pwanchai@engr.tu.ac.th Received 14 July 2015; accepted 13 September 2015; published 16 September 2015 Copyright © 2015 by authors and Scientific Research Publishing Inc. This work is licensed under the Creative Commons Attribution International License (CC BY). http://creativecommons.org/licenses/by/4.0/ 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 func tioning 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 quan tum key distribution protocol, which uses the entangled photon based on BB84 protocol. Keywords Cryptography, Quantum Cryptography, Quantum Key Distribution, Model Checking 1. Introduction Security has currently become an important topic of research. Confidential information, e.g. financial and credit card information, requires the h ighest s ecurity. Ther efore the cryptog raphy has be en used to pro tect the info rma tion. Nowadays the quantum cryptography is proposed as an alternative approach for security. The quantum cryptography is based on the quantum physics. The first protocol of the quantum key distribution was proposed in 1984 by Bennett and Brassard as BB84 protocol [1]. After that, so many quantum key distribution protocols have been p r o posed. However, BB84 protocol is still the most widely used protocol till date. The mathematical verifications of the security of the quantum key distribution are currently not sufficient. Therefore computer science researcher developed a technique and a device for analyzing protocols. For example,
S. Rochanapratishtha, W. Pijitrojana the model checker SPIN [2] can test the model for the compatibility with the temporal formula. However the model checker PRISM [3] is a probabilistic symbolic model checker which calculates the probability of compa tibility using the formula. The reason that the quantum mechanics is used is due to its random nature. Therefore, in this article, we proposed the analysis of the security of QKD using PRISM. This work is similar to [4][7]. The distinct difference is that we have collected the efficiency parameters of the quantum channel and the parameters of the rate of attack in [6] and applied to the quantum key distribution protocol with entangled photon pai rs. The idea is similar to [8] but here we use the e nt a ngled photon pairs i ns t e a d of the qubi t pairs. The structure of th e article is as follows . Section 2 presents the d etails of the BB84 protocol w ith Qubit pairs. In Section 3, we propose the basic technique of model checking and show the needs of this technique for the analysis of QKD. In Section 4, we present the result of the security analysis of the EEBB84 protocol that uses the efficiency parameters and the rate of attack to analyze the eavesdropping detection function. Lastly, we dis cuss the conclusion in the Section 5. 2. Quantum Key Distribution: BB84 with Entangled Photon Pairs Quantum Key Distribution (QKD) uses quantum mechanics to guarantee secure communication. It is only used to produce and distribute a key , not to transmit any message data. This key can then be used with any chosen encryption algorithm to encrypt (and decrypt) a message, which can then be transmitted over a stan dard communication channel. The protocol BB84 [1], named after its inventors and year of publication, uses four photon polariz ation states grouped together in two different nonorthogonal bases. It is based on the assumption that only one photon can be transmitted at a time. In general the two nonorthogonal bases are: a) Base + having horizontal polarization (0˚) and vertical p olarization (90˚), and we represent the base states with intuitive notation: and . So, we have . b) Base × having diagonal polarizations (45˚) and (135˚). The two different base states are and with and . So, we have . The association between the information bit and basis are described in the Table 1. The protocol can be de s c ribed as fol lows: 1) Quantum Transmissions (First Phase) a) Sources of entangled photon pairs randomly to create a pair of photons, then separate the photon qubit partner forwarded to Alice and Bob. Alice chooses a random string of bases , where n > N. b) Alice prepares a photon in quantum state aij for each bit di in d and bi in b as in Table 1, and sends it to Bob over the quantum channel. c) With respect to either + or ×, chosen at random, Bob measures each aij received. Bob’s measurements pro duce a string , while his c hoi ces of base s form . 2) Public D i s c uss i on (Seco nd Phase) a) For each bit di in d i) Alice over the classical channel sends the value of bi to Bob. ii) Bob responds to Alice by stating whether he used the same basis for the measurement. Both di and are discarded if bi ≠ . b) Alice chooses a random subset of the remaining bits in d and discloses their values to Bob over the classic al channel. If the result of Bob’s measurements for any of these bits does not match the values disclosed, eave sdropping is detected and communication is aborted. c) The string of bits r emaining in d once the bits disclosed in step 2b) are removed is the common secret key, . Measuring with the incorrect basis yields a random result, as predicted by quantum theory. Thus, if Bob Table 1. Coding scheme for the BB84 protocol. Table Head 0 1
S. Rochanapratishtha, W. Pijitrojana chooses the × basis to measure a photon in state 1, the classical outcome will be either 0 or 1 with equal proba bility because ; if the + basis was chosen instead, the classical outcome would be 1 with certainty because . To detect Eve, Alice and Bob perform a test for eavesdropping in step 2b) of the protocol. The idea is that, wherever Alice and Bob’s bases are identical (i.e. bi = ), the corresponding bits should match (i.e. di = ). If not, an external disturbance is produced or there is noise in the quantum channel, we suppose all that is caused by Eve. In our article we are interested in analyzing this important property assured by quantum mechanics: the enemy’s presence is always made manifest to the legitimate users. 3. The Model Checking for Our Work Designing the hardware and software for a complicated system requires a lot of time and effort to ensure the correctness. A technique that can help reduce the time and ensure the complete validity of a system is the formal verification. This technique can prove the correctness of the algorithm of the system required. The formal veri fication also includes the model checking. Model checking is the technique of the bruteforce verification of the system correctness. The model checking is used in the problem regarding the model that needs the automatic checking of the specification. We write the model checking using PRISM of model M with the specification pi as . The probability is calculated by (1) By writing , we can write the probability in Equation (1) for each of the . The result ing plot will show the de s cript i on of Equation (1). The model in PRISM consists of modules. Each module has its own working process and variables. The working mechanisms of each module are shown as follower [] () () ( ) 1 11222 : varvaluevarvalue: varvalue;: nn n action aaa →= +=++= (2) In Equation (2), the variable vari is defined by valuei with a probability equal to ai = 1. In case of n = 1 we have a symbolic 11111 :(varvalue )(varvalue )a== = with 1 and a = 1. The model checker PRISM allows for us defined a probability is an action. For instant: in case n = 2 we have modelling tends of protocol EEBB84 of Alice in choice of state of quantum by module as component the action: [ ] () ( ) 0.7 :10.3:0; stateofAlice trueEtatAliceEtatAlice→=+= (3) In Equation (3), Alice tends to choose one type of encoding data 1 in Table 1. 4. Analysis of the Entangled Photon Based on the BB84 Protocol by PRISM 4.1. The Detailed of the Model EEBB8 in PRISM The tool PRISM is the device for checking the probability. It was developed at the University of Birmingham. The characteristic of the model checker is that the input of the module represents the state change of the system and the general rule is in the form of temporal logic. The answer can be “yes” and “no” which shows the compa tibility with the specif ica tion . The testing of the probability model refers to th e analysis of the probability arises from the transition of states and the analysis with the analytical metho d. We setup the model of BB84 in PRISM started by setting the source to be an entangled photon using84 symbol. This model consists of the following modules: a quantum channel’s module, Alice’s module, Bob’s module and Eve’s module. This is consistent with quantum key distribution. We want to study the properties of security protocols EEBB84 with PRISM. We define the models that the model has to detect intercept them. So if Alice and Bob know that Eve was eavesdropping attempts. They have agreed to stop the process of creating a secret key code immediately. By using our model of EEBB84 calculate the probability as follows: (4) where represents a formula PCTL which its Boolean value is TRUE if the eavesdropper is detected. We
S. Rochanapratishtha, W. Pijitrojana can adjust the value of n to change the number of photons transmitted to the communication channel between Alice and Bob. So in our PRISM model this probability is a function of n. We write the probability of d etecting the eavesdropper as follows: ( ) { } det84 det Pr EEBB Pn MP= (5) We can see that PRISM will calculate the exact value of the probability of detecting an eavesdropper Eve. But we need to set definitions for . In order to determine the precise detection Eve, will allow us to write similar to the traditional values of a probability . 4.2. The Detailed of Pdet The model MEEBB84, we assume that Eve is a type of attack “interceptresend ”. So, Eve to trap photons passed in quantum communication channel. Eve will measure the photon with basis vectors (+ or x), and Eve to have measurable results given by . Then Eve sends photons to Bob with the same type of basis vectors. When Bob receives the photons by Eve and then Bob will be measured by a vector based on the measurement results is set by Ti. In order to detect Eve, it is necessary to compare the bits of Alice and Bob (which are respectively Ai and Bi) when the test of Bob is Ti = 1; if in such case then we are sure that a disturbance take place and it be caused certainly by the enemy, Eve. Let us note here that we suppose that the quantum channel is perfect; an imperfect channel can cause additional disturbances. In such case, for the need of the security we suppose all noise is due to Eve. So, Eve’s presence is made manifest as soon as the following event φ occurs: () ( ) 11for some i ii TA Bin ϕ ==∧≠−≤ (6) () () 1for some i ii TA Bin ϕ ==∧≤= (7) Therefore, we can give the expression of as a classical probability: ( ) ()( ) {} det Pr1for some i ii P nTABin = =∧=≤ (8) Finally, the PCTL formula corresponding to this formula is: () () { } det 1 i ii PTRUETAB=∪=∧ = (9) 4.3. The Probability of Detection of the Eavesdropper Here it is based on the assumption that the channel can store only one photon at a time and the quantum channel is ideal. We model this in the quantum channel module by the line: [ ] ()() ()() aliceputch_state0ch_state1 &ch_basal_bas&ch_bital_bit ; ′′ ′ =→= == (10) But, the eavesdropper intercepts all the photons passing through the channel. We model this in the quantum channel module by the line: [ ] () () () () eveputch_state3ch_state4 & ch_baseve_bas & ch_biteve_bit ; ′′ ′ =→= == (11) We use ch_state, ch_bas, ch_bit, al_bas, al_bit for respectively state, base and bit of the channel and base and bit of Alice. This line shows that the information sent by Alice (base and bit) remain unchanged before it re ceived by Eve. For , PRISM calculates , this produces the curve of (noted as ) as in Fig ure 1. We note from the above curve, if we increase the number of photons emitted by Alice over the quantum channel, the probabi l i ty of Eve’s detection increases and tends towards 1. 4.4. The Effect on Quantum Channel’s Performance and Rate of Attack In our model MBB84, the quantum channel is represented by a module called Quantum Channel which can be in
S. Rochanapratishtha, W. Pijitrojana Figure 1. The probability to detect Eve where the no of photons transmitted by Alice. reality optical fiber or free air. We expect that the probability of detecting Eve increases when the quantum channel becomes noisy and also the probability of detecting Eve increases when the rate of attack increases. To achieve this we have consider 3 cases. 1) channel(no noise) and weak attack As the channel is ideal channel we can model this in module quantum channel as Equation (9). When Eve doesn’t intercept most of the photons, we simulate a weak attack. We can write this line as: [ ] ()()() () ch _state3ch _state4&ch _ basal_&ch_bital_bit;eveput bas ′′ ′ =→= == (12) 2) Little noisy channel and medium attack When there is little noise in the channel we can model this in the module quantum channel as: [aliceput] (ch_state=0) → 0.7:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=al_bit) +0.1:(ch_state'=1) & (ch_bas'=1al_bas) & (c h_bit'=1al_bit) +0.1:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=1al_bit) +0.1:(ch_state'=1) & (ch_bas'=1al_bas) & (ch_bit'=al_bit); (13) As Eve performs a medium attack here we can model this line as: [eveput] (ch_state=3) → 0.5:(ch_state'=4) & (ch_bas'=eve_bas) & (ch_bit'=eve_bit) +0.5:(ch_state'=4) & (ch_bas'=al_bas) & (ch_bit'=al_bit); (14) 3) Much noisy channel and strong attack When there are very much noise in the channel we can model this in the quantum channel as: [aliceput] (ch_state=0) → 0.1:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=al_bit) +0.3:(ch_state'=1) & (ch_bas'=1al_bas ) & ( ch_bit’ '=1al_bit) +0.3:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=1al_bit) +0.3:(ch_state'=1) & (ch_bas'=1al _bas) & (ch_bi t'=al_bit); (15) As Eve intercepts all the photons passing through the channel we can model this in quantum channel as Equ ation (11). In the above situations PRISM provides a curve of Pdet noted Pdetch(i)Eve(i). The curv es Pdetch(i)Eve(i), for i = 0, 1, 2 are illustrated in Figure 2. In the above figure we mark that 1) When the quantum channel is ideal and the rate of attack is weak the probability of detection of eave sdroppe r i nc reases as we increas e the n umber of p hotons, 2) When the quantum channel is little noisy and the rate of attack is medium the probability of detection of eavesdropper increases more rapidly as we increase the number of photons, 3) When the quantum channel is very noisy and the rate of attack is strong the probability of detection of ea vesdropper increases even more rapidly as we increase the number of photons. 5. Conclusions As the need of Quantum cryptography is raised, it is very much necessary to test and analyze such systems with more effort. In this article we chose a modelbased technique for security analysis of the most widely used protocol
S. Rochanapratishtha, W. Pijitrojana Figure 2. The probability {Pdet ch(i); i = 0, 1, 2} to detect Eve where the no of photons transmitted by Alice. BB84. We are interested in studying the property of eavesdropper. By using the PRISM tool, we get the follow ing four results: First, if we want to increase the probability of the detection of eavesdropper, it is necessary to increase the number of transm i t ted photons. Second, in the case when the quantum channel becomes noisy then the probability of detecting the eave sdropper increases too. Third, when the power of Eve becomes much stronger, the probability of her detection is higher. Fourth, when comparing the results of the graph in Figure 2 with the [9] I can see that if the source of entan gled phot on pairs photons, the system has the probability to detect the eavesdropper higher. So, from the above results, we have seen a trend of security quantum key distribution protocols, and have de tected the eavesdropper is highly effective, according to the theory. And, when we change the source photons, they are entang led photon pairs. It showed that the rate of d etecting Eve was w ith even higher rates. This article is just presenting the analysis, model checking techniques for protocol EEBB84 (the source of photons w ith en tangled photon pairs). And we hope that the information in this article is a guide to the application of this tech nique to analyze other quantum protocols and so on. References [1] Bennett, C. H. and Brassard, G. (1984) Quantum Cryptography: Public Key Distribution and Coin Tossing. Proceed ings of the IEEE International Conference on Computers, Systems and Signal Processing, Bangalore, 1012 dEcember 1984, 175179. [2] Gerard, J.H. (1997) The Model Checker SPIN. IEEE Transactions on Software Engineering, 23, 279295. [3] prismmodelchecker. http://www.prismmodelchecker.org/ [4] Elboukhari, M., Azizi, M. and Azizi, A. (2009) Implementation of Secure Key Distribution Based on Quantum Cryp tography. Proceedings of IEEE International Conference on Multimedia Computing and Systems (ICMCS’09), Oua rzazate, 24 April 2009, 361365. [5] Elboukhari, M., Azizi, M. and Azizi, A. (2010) Analysis of Quantum Cryptography Protocols by Model Checking. IJUCS, 1, 3440. [6] Elboukhari, M., Azizi, M. and Azizi, A. (2010) Analysis of the Security of BB84 by Model Checking. International Journal of Network Security & Its Applications (IJNSA), 2, 8797. [7] Papanikolaou, N.K. (2004) Techniques for Design and Validation of Quantum Protocols. University of Warwick, Co ventry. [8] Siddiqui, M.A. and Qureshi, T. (2014) Quantum Key Distribution with Qubit Pairs. Journal of Quantum Information Science, 4, 129132. http://dx.doi.org/10.4236/jqis.2014.43014 [9] Sahoo, J. R. and Satapathy, S. (2011) Simulation and Analysis of BB84 Protocol by Model Checking. International Journal of Engineering Science and Technology, 3, 5695.
