Symbolic Abstractions for Quantum Protocol Verification
This work addresses the need for scalable and formal verification methods for quantum protocols, which is crucial for ensuring their security in practical deployments, though it is an initial step in an unexplored area.
The paper tackles the problem of verifying quantum protocols like BB84, which currently rely on tedious manual proofs, by proposing a symbolic abstraction approach to enable automated, exhaustive security analysis.
Quantum protocols such as the BB84 Quantum Key Distribution protocol exchange qubits to achieve information-theoretic security guarantees. Many variants thereof were proposed, some of them being already deployed. Existing security proofs in that field are mostly tedious, error-prone pen-and-paper proofs of the core protocol only that rarely account for other crucial components such as authentication. This calls for formal and automated verification techniques that exhaustively explore all possible intruder behaviors and that scale well. The symbolic approach offers rigorous, mathematical frameworks and automated tools to analyze security protocols. Based on well-designed abstractions, it has allowed for large-scale formal analyses of real-life protocols such as TLS 1.3 and mobile telephony protocols. Hence a natural question is: Can we use this successful line of work to analyze quantum protocols? This paper proposes a first positive answer and motivates further research on this unexplored path.