Formal Verification of the Security of a Free-Space Quantum Key Distribution System

The security of a free-space Quantum Key Distribution (QKD) system is analyzed by using PRISM, a probabilistic model checker. Disturbances and misalignments causing an imperfect channel are considered. The security of the system is formally demonstrated against intercept-resend and random substitution eavesdropping attacks for a particular range of transmitted photons. implemented in an experimental QKD system. We will consider the influence of possible disturbances in the free- space between Alice and Bob, and misalignments in the optics to calculate the probability of detection of the eavesdropper as a function of the number of photons transmitted (or equivalently, the length of the bit sequence generated by Alice). The rest of the paper is organized as follows. Section II includes some preliminaries and definitions. Section III briefly outlines the BB84 protocol, describes the actual free-space QKD system under development in our labs, and exposes the model checking methodology used to analyze its security. The calculated results are presented and discussed in section IV and, finally, conclusions are derived in section V.