Journal of Quantum Information Science, 2015, 5, 103-108
Published Online September 2015 in SciRes.
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, 103-108.
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,
Email: m,
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).
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.
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
{ }
0, 1
, 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 non-orthogonal bases. It is based on the assumption that only one photon can
be transmitted at a time.
In general the two non-orthogonal bases are:
a) Base + having horizontal polarization (0˚) and vertical p olarization (90˚), and we represent the base states
with intuitive notation:
. So, we have
{ }
b) Base × having diagonal polarizations (45˚) and (135˚). The two different base states are
. 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
{ }
b∈ +×
, 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. Bobs measurements pro-
duce a string
{ }
0,1 n
, while his c hoi ces of base s form
0, 1
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
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 Bobs 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,
{ }
0, 1
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
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
( )
112=⋅ +−−
; 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 Bobs 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
enemys 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 brute-force 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
{ }
By writing
( )
,, ,
M Mxxx=
, 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
→= +=++=
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
:(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→=+=
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 yesand nowhich 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 using84
This model consists of the following modules: a quantum channels module, Alices module, Bobs module
and Eves 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:
{ }
84 det
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
Pn MP=
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 intercept-resend . 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, Eves presence is made manifest as soon as the following event φ occurs:
() ( )
11for some
i ii
TA Bin
() ()
1for some
i ii
TA Bin
Therefore, we can give the expression of
as a classical probability:
( )
()( )
Pr1for some
i ii
P nTABin
= =∧=≤
Finally, the PCTL formula
corresponding to this formula is:
() ()
{ }
i ii
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 ;
′′ ′
=→= ==
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 ;
′′ ′
=→= ==
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.
1 30N≤≤
, 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 Eves 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
doesnt 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
′′ ′
=→= ==
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'=1-al_bas) & (c h_bit'=1-al_bit)
+0.1:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=1-al_bit)
+0.1:(ch_state'=1) & (ch_bas'=1-al_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'=1-al_bas ) & ( ch_bit’ '=1-al_bit)
+0.3:(ch_state'=1) & (ch_bas'=al_bas) & (ch_bit'=1-al_bit)
+0.3:(ch_state'=1) & (ch_bas'=1-al _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 model-based 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.
[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, 10-12 dEcember
1984, 175-179.
[2] Gerard, J.H. (1997) The Model Checker SPIN. IEEE Transactions on Software Engineering, 23, 279-295.
[3] prismmodelchecker.
[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, 2-4 April 2009, 361-365.
[5] Elboukhari, M., Azizi, M. and Azizi, A. (2010) Analysis of Quantum Cryptography Protocols by Model Checking.
IJUCS, 1, 34-40.
[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, 87-97.
[7] Papanikolaou, N.K. (2004) Techniques for Design and Validation of Quantum Protocols. University of Warwick, Co-
[8] Siddiqui, M.A. and Qureshi, T. (2014) Quantum Key Distribution with Qubit Pairs. Journal of Quantum Information
Science, 4, 129-132.
[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.