Ebrahim Ardeshir-Larijani

Quantum communication offers a novel approach to secure transmission of information, where its security is based on the laws of quantum mechanics, rather than computational assumptions. The concept of such a system has been in existence since the 1980s, with the BB84 quantum key distribution protocol serving as a significant early example. Over the years, this innovative system has been industrialized and is now employed by various governmental and business organizations, showcasing its practical applications and importance in enhancing secure communications. Despite its success, the standardization of this technology is still underway. As a result, deploying quantum communication systems within the existing network infrastructure faces challenges, particularly due to the need for high levels of assurance and trust. Formal verification has been shown to be useful for building assurance in safety-critical systems at various levels, including both software and hardware. While some proofs of quantum and post-quantum security have been explored through formal verification and high-level descriptions, the investigation of lower-level subsystems remains less developed. In fact, the majority of attacks on quantum communication systems arise from implementation loopholes. Therefore, the verification of the corresponding system level remains essential for establishing assurance. With the current ETSI and ISO standards for QKD, along with certification methods, there is a significant basis for implementing formal verification techniques in quantum communication systems. In this work, we use the Algebra of Communication Process (ACP) and its associated tool, MCLR2, to specify two levels of a quantum communication system. The first level (1) consists of digital and software algorithms that directly control the electronics and optics, including their calibration. This level may include algorithms for maintaining the temperature of avalanche photodiodes (APDs), managing bias voltage, and controlling gating. The second level (2) involves software that determines which subroutine from level (1) to execute. For instance, it decides when the APDs should be cooled or when gating control should be initiated. Our aim in using such symbolic and formal verification techniques is to detect software vulnerabilities that potentially lead to known implementation loopholes and attacks on quantum communication systems. To achieve this, we first map levels (1) and (2) structures to the MCLR2 specification language. Next, we check for various properties, including deadlock, starvation, and livelocks. Finally, we examine which known attacks can be initiated in the presence of such malicious behavior.