Testing the quantum anonymous transmission protocol

Whereas most quantum protocols are described in natural language and rarely analysed through the lens of formal methods, modern quantum network infrastructures demand rigorous guarantees of correctness and security. Process calculi represents a natural candidate for quantum protocol verification, given their effectiveness in modeling and analysing distributed systems. In this paper, we put forward a testing semantics for a quantum extension of value-passing CCS, resorting to concrete experiments that a user can perform to investigate protocol properties. To guarantee strict adherence to the laws of quantum mechanics, we integrate an explicit treatment of non-determinism, thereby preventing unphysical behaviors such as extracting the state of a qubit without measurement-induced collapse. We put to work our formal development on a real-world case by analysing the Quantum Anonymous Transmission Protocol. This protocol leverages local operations and entangled state measurements to allow participants to broadcast classical bits anonymously. Using our approach, we formally prove the correctness of the protocol (showing that bits are broadcast as if over a standard classical channel) as well as its relevant security properties, namely anonymity under various attacker models.