Modeling and Verification of Aircraft Takeoff Through Novel Quantum Nets

Maryam Jamal,Nazir Ahmad Zafar,Atta-ur-Rahman,Dhiaa Musleh,Mohammed A.Gollapalli and Sghaier Chabani

1School of Systems and Technology,University of Management&Technology(UMT),C-II Block C 2 Phase 1 Johar Town,Lahore,54770,Punjab,Pakistan

2Department of Computer Science,COMSATS University Islamabad-Sahiwal Campus,Sahiwal,57000,Punjab,Pakistan

3Department of Computer Science(CS),College of Computer Science and Information Technology(CCSIT),Imam Abdulrahman Bin Faisal University(IAU),Dammam,31441,Saudi Arabia

4Department of Computer Information System(CIS),College of Computer Science and Information Technology(CCSIT),Imam Abdulrahman Bin Faisal University(IAU),Dammam,31441,Saudi Arabia

Abstract: The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed Quantum Nets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net (CPN)Tools.Moreover,reachability tree (RT) analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.

Keywords: Aircraft takeoff;BB84;quantum cryptography;petri-nets;quantum nets;formal modeling and verification

1 Introduction

Takeoff is the initial and critical phase of a flight as it raises the confidence level of overall flight safety.The task of safe aircraft takeoff is also distributed amongst various computer-based controllers.The intense communication between different controllers involved in aircraft takeoff needs to be secure which is perplexed by the dynamic,distributed,and concurrent nature of air traffic control system.These issues make the takeoff process a highly difficult and challenging domain [1].Furthermore,even a minor system error or abnormal system behavior may lead to severe consequences in term loss of precious human lives and heavy monetary penalties.Also,the possible intrusion of an eavesdropper during communication between aircraft and controller may put the whole takeoff process at a high security risk.Therefore,there is need of modeling and verification of aircraft takeoff process while focusing the overall system security.The BB84 quantum protocol was introduced in 1984 by Bennett et al.[2]that offers a secure way of communication by combining the cryptography with quantum principles[3].It is among the strongest techniques which guarantees safe transmission between a transmitter and receiver.The presence of an intrusion attack by an eavesdropper is identified through photon polarization [4].But petri-nets are graphical formal methods which underlies on strong mathematical foundations.Due to their robust expressivity,they are widely used for modeling concurrency and non-determinism.Furthermore,the petri-nets are enriched with strong verification support for inspecting correctness of a system [5].Undergoing research provides an integration of BB84 with petri-nets for formal modeling and verification of aircraft takeoff procedure while incorporating system security.As the BB84 is a quantum cryptographic protocol which provides the maximum level of security,and the petri-nets are a powerful notation for mathematical modeling and verification of distributed concurrent systems.This integration allows a secure and comprehensive mathematical modeling of aircraft takeoff.Moreover,it allows system verification for presence of potential errors and unexpected system behavior.While the errors spotted during modeling are easier and cheaper to be fixed.This research is important as it provides starting point for integration of quantum cryptography with petri-nets to integrate best features of both approaches.Since the petrinets offers only three basic notations (place,transition,and arcs) therefore,they cannot model all concepts of BB84 which is a quantum cryptographic protocol.The existing notations and properties of traditional petri-nets are enriched for quantum concepts through the development of a new variant of traditional petri-nets,named as the“Quantum Nets”.The existing work regarding integration of BB84 with petri-nets is novel in a sense that an existing work is found where the integration was performed at an abstract level [6],whereas some existing work just covers the model checking of BB84 protocol.In this study,the strong static foundations of quantum nets are developed to describe distributed network nodes,concurrent bi-directional communication,and flow of different types of data whereas the dynamic properties such as tokenization,external transitions,transition,enabling,and system dynamics are also formalized.Furthermore,the properties like reachability,boundedness,liveness,safety,and concurrency are abstractly defined in this research.The proposed Quantum Nets are applied to develop a formal model of aircraft takeoff which is composed of three quantum nets namely aircraft,runway controller,ground controller.The authentication process is defined through a public and a quantum channel also the secure communication between the quantum nets is modeled through external places and external transitions.To inspect its behavior,the proposed model is verified through CPN tools simulator.The proposed takeoff model is also verified by using mathematical proof technique of reachability tree (RT) analysis which ensures the correctness of proposed model which further makes the study unique.

The article is sectioned as:Section 2 covers a thorough literature survey,the mathematical foundations of proposed quantum nets are enclosed in Section 3.The mathematical properties of quantum network are specified in Section 4 and in Section 5,the practical applicability of quantum nets is demonstrated through the case study of an aircraft takeoff.Finally,Section 5 wraps up the articles with concluding remarks.

2 Literature Survey

Formal modeling and verification of quantum protocols using various mathematical techniques is among the hottest areas of research.The research in[7,8]focused the verification of B94 protocol through PRISM tool.Similarly,some quantum protocols were verified by using a decision procedure which integrates algebraic logic with operational semantics in[9].The application of a quantum model checker was shown in [10,11].In [12]process calculus was used to model BB84 protocol which was analyzed by concurrency workbench of the new century(CWB-NC)tool.A new language coined as Communicating Quantum Processes was proposed by combining pi-calculus with quantum theory in[13].In [14]a Hoare-style logic was proposed for quantum protocols and a semi-automated formal framework was defined for verification of quantum systems in [15].To analyze the bi-simulation relation of quantum processes a tool was developed in [16]and in [17]an entanglement sampling technique was applied to find the lower bound of entanglement which is required by an eavesdropper for attacking a quantum channel.The measurement in a quantum process calculus was described in[18]by using bi-simulation congruence and protocol equivalency.Distribution-based bi-simulation of quantum process by using process algebra was proposed in [19].The research in [20]presented an automation of unconditional security proof for quantum key distribution and the quantum information system based on B92 protocol.The process was performed by using PRISM tool in[21].In[22]a variant of BB84 was modeled by using discrete time Markov chain and probabilistic computation tree logic and its security properties were verified by using PRISM tool.BB84 and B94 were modeled by using Communicating Quantum Processes in [23]which were translated into PRISM model for its verification.IEEE 802.11 standard was integrated with BB84,and some security properties were analyzed by using PRISM tool in [24].Some important quantum bit commitment approaches were proposed in [25,26]and were reviewed in [27,28].In [29]the analysis of this protocol was done by using model checking to demonstrate its practical applicability.Few basic correctness properties of the protocol were verified in [30]by using PRISM tool to demonstrate the feasibility of automated verification techniques.A new formal execution technique called equivalence checking was presented in [31,32]for analysis of the protocol.It focused on communicating concurrent components which the authors claimed to be applicable on all input states.The use of PRISM tool was shown for identification of an eavesdropper in a quantum system in[33].Few ways to attack the quantum network were modeled and verified by using PRISM tool in [5].Focusing the parameter of eavesdropper and quantum channel,the security of BB84 was analyzed through PRISM tool in [34].Automated model checking PRISM tool was used in[35]and a direct relation was identified between number of transmitted qubits and evasion of an eavesdropper.The channel disturbance of a quantum channel was modeled and verified by using PRISM tool in[36].While the entangled photon pairs of BB84 protocol were focused for verification using PRISM tool in[37]and addressed in[38].Other than cryptosystems,digital watermarking and steganography also used for authentication and verification.Especially,in digital image transmission,the images need to be secure[39].In digital image watermarking mainly,proprietary,and medical images are watermarked for sake of authentication,integrity and information hiding[40-44].Similarly,steganography is used for secrecy[45-48].

Based on the extensive review of modeling and verification of BB84 quantum key distribution techniques,the undergoing research was conducted.In the literature,several approaches verified certain dimensions of this protocol but all of them mainly use the PRISM toolset for the verification.However,the investigation of petri-nets for modeling and verification of a quantum cryptographic system has been an uncovered arena of research.Only one related publication was found in which the petri nets were used to model quantum communication protocol at an abstract level[6].Since quantum cryptography offers a high level of security and it can detect an intrusion attack as well.Modeling and verification of a quantum cryptographic system has a potential benefit of revealing unexpected system behavior.Also,the errors identified before system implementation are easier and cheaper to be fixed.Therefore,the modeling and verification capabilities of petri nets may be fruitful in modeling of BB84 quantum protocol.

3 The Extended Petri-Nets

In this section the extension of Petri-nets is provided.The BB84 is a quantum key distribution protocol which exploits photon polarization state for transmission of qubits.Using this protocol,the sender and receiver are connected through a quantum channel and a classical channel.Both channels are not secure against intruder attack.The encoding of BB84 lays its foundation on the pairs of orthogonal states named as a basis.A basis can either be rectilinear with vertical polarization state or diagonal with horizontal polarization state.The two bases are used in this protocol as both are conjugate to one another.The conjugate pair of basis is known to both sender and receiver prior to their communication.The sender chooses one of the basis to encode a qubit and sends it to receiver,via its quantum channel.The receiver receives the qubit through its quantum channel,and it decodes the basis of a qubit on random guessing.Once the stream of qubit sent by the sender is decrypted by the receiver,it resends the decrypted basis values back to sender through its public channel for matching.If the number of matching decrypted and encrypted qubits is less than or equal to a threshold then the sender verifies the receiver and sends the secret message safely to receiver via its public channel.Petri-nets are robust graphical formal methods widely used by experts for modeling distributed and concurrent systems.The foundations of petri nets are based on firm mathematical semantics,and they offer strong verification techniques like reachability,boundedness etc.Further,they offer simple place-transition notations which can be extended for complex systems modeling.Subsequently,the integration of BB84 cryptography with petri-nets is provided.To model quantum key cryptography,a new variant of traditional petri-nets,coined as the“Quantum Nets”is defined.Basic petri-nets are mathematically enriched with quantum concepts as described in next section.

3.1 Quantum Nets

A quantum net is defined as,is the set of places defined aswhere PIis the set of internal places of a net and PEis the set of external places,is the set of transition,defined aswhereis the set of internal transitions of a net andis the set of external transitions.An external transition and an external place are not only visible to its resident quantum net but also to all other nets.They can be accessed by any non-resident quantum nets and can change marking of a quantum net.is the set of connections between place and transition or vice versa such thatand0is the initial marking of a quantum net such that.A flow arc f is an external arc,such that f( ,)3where transition is an external transition and is an external place.

3.2 Quantum Key Distribution System

A quantum key distribution system is defined as a tuple namedwhere QID3¤+which is unique identifier of a quantum net,is the source quantum net and its initial markingis the destination quantum net and its initial markingis the qubit interaction channel defined assuch thatandρis the message interaction channel defined assuch thatand

3.3 System Dynamics

The arc activation rules make the interaction of quantum net possible.These rules are triggered before transporting qubits and messages on their respective channels.The rules for arc activation within a quantum key distribution system QDS is a pair of marking (M,M’) such that M is the marking of source quantum net,and M’is the marking of destination quantum net,are defined as follows.

3.4 Quantum Key Distribution Network

A quantum key distribution network is defined as a tuple namedwhereis the set of all source quantum nets and defined asis the set of all destination quantum netsis defined as a total injective function and defined asψ:QDS?QDS such thatDom(ψ).q3QS andRan(ψ).q3QD.

3.5 Token Declaration

A token can be of two types:the qubits and bits.Thequbitis a specialized token meant to travel on a quantum channel.A qubit is defined as Bit2Basis2Polarization2.Abitrepresents a Boolean value of either 1 or 0 and defined as Bit:1|0,Basisis defined as Rectilinear or Diagonal.ARectilinear Basiscan have a value 0 for vertical and 90 for horizontal state.Likewise,aDiagonal Basiscan have a value 45,135 or a circular basis of left and right handedness.A Rectilinear basis is represented as V and a diagonal basis is represented as D.Polarizationrepresents a photon polarization which is generated from bit and basis value.For instance,basis V with bit 0 is represented as North,N and a bit 1 is shown as Right,R.A basis D with bit 0 is marked as North East,NE and a bit 1 is represented as South East,SE.is the time at which the qubit emits from the sender’s quantum channel.A bit token is designed to carry message on a classical public channel.A bit token can carry a stream of bits,so it is defined as ?Bits.At the receiver’s end when a qubit is received via quantum channel it appends the time with a delay factor,γsuch that at receiver’s end

3.6 External Transition

A transition of a petri-net allows token movement from one place to another.To allow external communication,we extend the transition with a new one called channel transition.Achannel transitionis a kind of transition which is not only visible to a quantum net to which it belongs to but also to outside nets.Any place can connect with it to transmit its tokens.It is important to note that the same transition is defined to work for incoming and outgoing token flow.Based on the flag,channel transition allows incoming flow if flag is set to true and outgoing flow is achieved if flag is set to false.Moreover,for each quantum net two external transitions are mandatory,i.e.,a quantum and public channel.The channel transition to represent a quantum channel is capable of transporting qubits whereas a channel transition which represents a public channel can carry public data.Any place with a qubit token can access quantum channel transition whereas any place with a bit token can access a public channel transition.

4 Properties of Quantum Network

After giving formal foundations to the quantum nets,in this sub-section we define some of its system properties.The system properties help to define overall system behavior.We have defined the following properties for the quantum system.The functions used to define such properties are described in Tab.1.The proof of following properties is left for the future work.

Table 1:Notations used in safety properties

4.1 Reachability

Every quantum net can send message to another quantum net at any time if the sender is idle and receiver is not a sender or receiver of any other communication.

?q1,q2:QN;t:¤.

IsIdle(q1)ù(? IsSender(q2)ú ?IsReceiver(q2))

4.2 Boundedness

Each quantum net of a quantum system must be in an idle state or communicating with another net either as a sender or a receiver.

?q:QN.q3Q ü

IsIdle(q)ú IsSender(q)ú IsReceiver(q)

4.3 Liveness

Every two quantum nets communicating at any time must end their communication after certain interval of time.

?q1,q2:QN;t,k:¤.Com(q1,q2)@

IsIdle(q1)@t+k ù IsIdle(q2)@t+k ù t ? t+k

4.4 Safety

A quantum system is safe if for every sender there is a single receiver and sum of all quantum nets must be equal to idle,sending and receiving nets.

?q:QN.|Receiver(q)|=1 ù

(|QN|=|Idle|+|Senders|+|Receivers|)

4.5 Concurrency

In a quantum system any two quantum nets can communicate simultaneously.

?q1,q2:QN;t:¤.q13Q ü

((IsSender(q1)@t ù IsSender(q2))ú

(IsReceiver(q1)@t ù IsReceiver(q2)))ùq1μ q2

5 Air Traffic Control System

Takeoff is the primary phase of aircraft journey and a safe takeoff raise the confidence level for overall safety.In an earlier study[49]also demonstrated the modeling and analysis of an aircraft takeoff process by using Vienna Development Method Specification Language(VDM-SL).Being the initial flight phase,takeoff should be a secure process to avoid intrusion of any malicious attack.The task of safe aircraft takeoff is also distributed amongst various computer-based controllers and requires secure coordination.Any security loophole may facilitate an intruder to cause immense damage to the whole system.Also,air traffic control system is a complex and highly distributed safety critical system.Its secure modeling and analysis become crucial because even a minor system flaw may lead to catastrophic effects such as monetary loss and risk of human lives.

5.1 Aircraft Takeoff Quantum Network

In this section we have developed a quantum network for an aircraft takeoff.To model takeoff process,as explained earlier,three quantum nets are defined.An aircraft is represented by an aircraft quantum net and the controllers of gate and runway are depicted through a gate controller quantum net and runway quantum net respectively as shown in Fig.1.The labels assigned to all transition of each quantum nets are shown in Tab.2.Theaircraft quantum nethas twenty-two internal places(pa1 to pa22) and two external places;qaiofor a quantum channel and paiofor a public channel.Also,the aircraft quantum net has four external transitions (ta1,ta13,ta7 and ta14) and the other nineteen are internal transitions.Thegate controller quantum nethas twenty-four internal places(pa1 to pa24)and two external places;qgiofor a quantum channel and pgiofor a public channel.Also,the gate controller quantum net has four external transitions(tg1,tg13,tg7 and tg14)and the remaining twenty are internal transitions.Therunway controller quantum nethas twenty-five internal places(pa1 to pa25)and two external places;qriofor a quantum channel and priofor a public channel.Also,the runway controller quantum net has four external transitions(tr1,tr13,tr7 and tr14)and the remaining twenty-one are internal transitions.

Figure 1:A quantum network for an aircraft takeoff

Table 2:Legends for transitions of the quantum nets defined in aircraft takeoff

When an aircraft quantum net is ready for takeoff,it contacts the gate controller quantum net.The controller net verifies identity of an aircraft net by encrypting a stream of qubit(tg8 to tg10)and sends them(tr12 to tr13)via its quantum channel qgio.The controller net also stores the basis values of sent qubits in pg5,for later matching.The aircraft net receives the qubits (ta1) via its quantum channel qaioand decrypts them (ta3 to ta4) on random basis.It then sends the decrypted values of qubits(ta6 to ta7)back to the controller net through its public channel paio.After receiving decrypted values (tg14) through its public channel pgio,the controller net matches the decrypted values with the sent qubit values.If the matching entries are less than or equal to a pre-decided threshold(tg15)then the controller net authenticates the aircraft net,otherwise the communication is aborted(tg18).Once an aircraft is successfully authenticated,the controller net looks for favorable weather condition and a vacant ramp.If both conditions are met,then it prepares a ramp route and grant permission to aircraft net (tg21 to tg24) through its public channel pgio.After receiving permission (ta14) via its public channel paio,the aircraft transits the defined area according to the route specified by the controller net(ta22 to ta23).

When an aircraft quantum net enters the ramp,it ends its communication with the gate controller and then it contacts the runway controller quantum net.The controller net verifies identity of an aircraft net by encrypting a stream of qubits(tr8 to tr10)and sends them(tr12 to tr13)via its quantum channel qrio.The controller net also stores the basis values of sent qubits in pr5,for later matching.The aircraft net receives the qubits(ta1)via its quantum channel qaioand decrypts them(ta3 to ta4)on random basis.It then sends the decrypted values of the qubits(ta6 to ta7)back to the controller net through its public channel paio.After receiving decrypted values(tr14)through its public channel prio,the controller net matches the decrypted values with the sent qubit values.If the matching entries are less than or equal to a pre-decided threshold(tr15)then the controller net authenticates the aircraft net,otherwise the communication is aborted(tr18).Once an aircraft is successfully authenticated,the controller net looks for favorable weather condition,a vacant taxiway,and a vacant runway.If all three conditions are met,then it prepares a runway route and grant permission to aircraft net(tr21 to tr25)through its public channel prio.After receiving permission(ta14)via its public channel paio,the aircraft transits through the defined area according to the route specified by the controller net(ta22 to ta23).Therefore,the visual representation of three communicating quantum nets namely aircraft,runway controller and gate controller are successfully shown in this section.The interaction between the three quantum nets for a successful takeoff is demonstrated through proposed BB84 quantum nets and results are demonstrated in Tab.3.

First row of Tab.3 shows the interaction between gate controller quantum net and an aircraft quantum net.The controller net being the sender sends an encrypted stream of seven qubits.The aircraft net being the receiver decodes the qubit on random basis and it successfully decrypts four qubit values yielding a result within threshold value.Therefore,the aircraft net is authenticated successfully by the gate controller net.In row two,the sender is a runway controller net,and the receiver is the aircraft net.Out of seven encrypted qubits,the aircraft net successfully decodes five qubits’values,yielding a result within threshold value.Therefore,the aircraft net is authenticated successfully by the runway controller net.In row third,the sender is a gate controller net,and the receiver is the aircraft net.Out of seven encrypted qubits,the aircraft net successfully decodes just two qubits’values,yielding a result out of the threshold value.Therefore,the aircraft net is not authenticated by the gate controller net and their communication is aborted.In row fourth,the sender is a runway controller net,and thereceiver is the aircraft net.Out of seven encrypted qubits,the aircraft net successfully decodes just one qubit value,yielding a result out of the threshold value.Therefore,the aircraft net is not authenticated by the runway controller net and their communication is aborted.The last two rows of Tab.3 show the intrusion detection scenarios.In row fifth,the sender is a gate controller net,and the receiver is the aircraft net.Out of seven encrypted qubits,the aircraft net wrongly decodes the pre-decided polarization values.For instance,the polarization decided for basis V and bit 1 was R which was wrongly decrypted in first qubit of fifth row as NE which shows the presence of an intruder who does not know the pre-set values.Therefore,the last two rows of Tab.3 are unsuccessful authentications,and their respective interactions are aborted.

5.2 Model Verification

In this section,the verification results of aircraft takeoff quantum network have been discussed.In the quantum network of an aircraft takeoff the encrypted qubit and decrypted values are matched for authentication purposes,the results are shown in Tab.3.In the takeoff quantum network,two types of communication are involved:firstly,between an aircraft and gate controllerand thenbetween an aircraft and runway controller.Let us assume that for both interactions the pre-decided threshold is 50%.The bit values are 0 and 1;the basis values are D for diagonal and V for vertical;and Polarization represents a photon polarization which is generated from bit and basis value.For instance,basis V with bit 0 is represented as North,N,and basis V with a bit 1 is shown as Right,R.A basis D with bit 0 is marked as North East,NE and basis D with a bit 1 is represented as South East,SE.

5.3 Reachability Tree(RT)Analysis

The reachability analysis for quantum network of an aircraft takeoff is presented in this subsection.It helps to find that the system under study is free from any unexpected behavior.The external transitions are also used to represent communication between nets labeled as T1,T2,and so on.First,a RT is constructed in Fig.2 to represent the successful authentication between a gate controller and an aircraft net.The nodes of the tree are based on places and transitions of either an aircraft net or a gate controller net.The external transitions defined are T1 to T3.The marking and labels are also narrated in Fig.2.

An RT is constructed in Fig.3 to represent the unsuccessful authentication between a gate controller and an aircraft net.The nodes of the tree are based on places and transitions of either an aircraft net or a gate controller net.The external transitions defined are T1 and T3.

The defined marking of the tree and their labels are also narrated in this Fig.4.An RT is constructed in Figs.4 and 5 to represent the successful and unsuccessful authentication between a runway controller and an aircraft net,respectively.The nodes of the trees are based on places and transitions of either an aircraft net or a gate controller net.The external transitions defined in Fig.4 are T1 to T3 and T1 and T2 in Fig.5,respectively.The defined marking of each tree and their labels are also narrated in their respective figures.Each RT shows that the system exhibits no unexpected error and there are no unreachable markings in the quantum network of an aircraft takeoff.

Table 3:Results of quantum network for an aircraft model

Figure 2:RT of successful authentication between aircraft and gate controller nets

Figure 3:RT of unsuccessful authentication between aircraft and gate controller nets

Figure 4:RT of successful authentication between aircraft and runway controller nets

Figure 5:RT of unsuccessful authentication between aircraft and runway controller nets

Tab.4 shows a qualitative comparison of the proposed approach with the scheme given in[6]and[29-37]in terms of analysis type,protocol properties and tool used for analysis.Mainly it is observed that the types of analysis are performed by means of model checking and model verification.

Table 4:Comparison

6 Conclusion

This research provides an integration of BB84 with petri-nets for formal modeling and verification of aircraft takeoff procedure.A new variant of traditional petri-nets,coined as the“Quantum Nets”are developed to integrate quantum characteristics of BB84.The strong static foundations of quantum nets are developed whereas the dynamic properties such as tokenization,external transitions,transition,enabling,and system dynamics are also formalized.Furthermore,the properties like reachability,boundedness,liveness,safety,and concurrency have been abstractly defined.By using the defined Quantum Nets formal model of aircraft takeoff is developed which constitute of three quantum nets namely aircraft,runway controller,ground controller and secure communication between them is described by using BB84 protocol.The model is checked through simulator of CPN Tools,and it is also verified through proof technique of RT analysis.This research reveals some fruitful outcomes and opens the horizons for future research of quantum cryptography.The expressivity of traditional petri-nets has been enhanced by developing its new variant,coined as a Quantum net,which can be used in future for modeling similar systems.The modeling and verification of a quantum system helps to identify errors and abnormal system behavior from a system to be built long before the system is physically implemented.Identification of errors and bugs spotted during modeling are easier and cheaper to be fixed.In this research only some properties of a quantum system are stated at an abstract level.Many more properties can be defined for further analysis and all the defined properties can also be extended for an intense and comprehensive verification.In this research we have only demonstrated the use of RT for verifying a quantum cryptographic system.Also,some more proof techniques like liveness,deadlock,simulations etc.,can be exploited to analyze various other dimensions of the cryptographic system such as an earlier work demonstrated the strength of agent-based mobile petri-nets in modeling security policy[50].The quantum nets proposed in this research also has some limitations.As the public channel is not secure,it is vulnerable to some kinds of security threats like eavesdrop,integrity etc.,any intruder can access the secure data.So,security of this channel needs to be focused for overall privacy of the system.Other limitation of quantum net is inherent in physical characteristics of a quantum channel.BB84 works on a photon polarization state and a quantum channel is designed to carry photons.Other than an intrusion attack,the state of a photon may change based on the environmental factors such as intense light and noise.It inhibits the receiver to correctly decode the qubits and authentication becomes unsuccessful,and communication is aborted since it takes time when exposed to the factors.More studies can be conducted to overcome these limitations by means of using quantum nets in contrast to CPN tool and RT analysis.

Acknowledgement:Acknowledged to our families whose unconditional support enabled us to work.

Funding Statement:The authors received no specific funding for this study.

Conflicts of Interest:The authors declare that they have no conflicts of interest to report regarding the present study.