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.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.

arXiv:1904.04186Apr 8, 20191 citation

Symbolic Specification and Reasoning for Quantum Data and Operations

Mingsheng Ying

In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$ , which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.

cs.PLCross-listedarXiv:2512.22383Dec 30, 20250 citations

Formal methods for quantum cryptography

Ellie D’Hondt

Jan 1, 20080 citations

\mathbf{SOL}

, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into

\mathbf{SOL}

is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.