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 encryption decryption 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.