TITLE: Formal Verification of Quantum Protocols using the Proof Assistant Coq
SPEAKER: Jaap Boender (Middlesex University), this is a joint work with Florian Kammueller and Rajagopal Nagarajan.

ABSTRACT:

Quantum computing and quantum communication are exciting areas of
research at the intersection of physics and computer science, which
have great potential for influencing the future development of
information processing systems. Quantum cryptography, in particular,
is well developed. Commercial Quantum Key Distribution systems are
easily available and several QKD networks have been built in various
parts of the world. However, the security of the protocols rely on
information-theoretic proofs, which may or may not reflect actual
system behaviour, and testing of the implementations. We will present
a novel framework for modelling and proving quantum protocols using
the proof assistant Coq. We provide a Coq library for quantum bits
(qubits), quantum gates, and quantum measurement. We implement and
prove a simple quantum coin flipping protocol. As a step towards
verifying practical quantum communication and security protocols, such
as Quantum Key Distribution, we support multiple qubits, communication
and entanglement.