Modelling and Analysis of Quantum Key Distribution Protocols, BB84 and B92, in Communicating Quantum Processes(CQP) language and Analysing in PRISM

TL;DR

This paper models BB84 and B92 quantum key distribution protocols in CQP and PRISM to analyze their security features, especially their ability to detect eavesdroppers and the limitations on eavesdropper's information gain.

Contribution

It introduces a formal modeling approach of quantum protocols in CQP and PRISM, focusing on eavesdropper detection and protocol comparison.

Findings

Eavesdropper detection depends on the number of exchanged qubits.

Both protocols can detect active eavesdroppers under certain conditions.

Performance comparison highlights strengths and limitations of BB84 and B92.

Abstract

Proof of security of cryptographic protocols theoretically establishes the strength of a protocol and the constraints under which it can perform, it does not take into account the overall design of the protocol. In the past model checking has been successfully applied to classical cryptographic protocols to weed out design flaws which would have otherwise gone unnoticed. Quantum cryptographic protocols differ from their classical counterparts, in their ability to detect the presence of an eavesdropper. Although unconditional security has been proven for both BB84 and B92 protocols, in this paper we show that identifying an eavesdropper's presence is constrained on the number of qubits exchanged. We first model the protocols in CQP and then explain the mechanism by which we have translated this into a PRISM model. We mainly focus on the protocols' ability to detect an active eavesdropper and the extent to which an eavesdropper can retrieve the shared key without being detected by either party. We then conclude by comparing the performance of the protocols.