Symbolic Abstractions for Quantum Protocol Verification

TL;DR

This paper explores the application of symbolic abstraction techniques to the formal verification of quantum protocols, aiming to improve scalability and automation in security analysis.

Contribution

It introduces a novel approach to analyze quantum protocols using symbolic abstractions, bridging a gap in formal verification methods for quantum security.

Findings

Demonstrates the feasibility of symbolic abstractions for quantum protocol analysis

Provides initial results supporting automated verification of quantum security properties

Suggests potential for scaling formal analysis to complex quantum protocols

Abstract

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.