Quantum cryptography enables provably secure communication based on the principles of quantum mechanics [1]. However, research is hampered by the lack of good formalisms for modeling and verifying quantum protocols. One possible approach is based on extensions of process algebras, such as Milner’s calculus of communicating systems (CCS), which are used to model and analyze communication and concurrency in classical systems.

This paper presents a quantum process algebra, qCCS, that extends CCS by primitives for quantum communication, operator application, and measurement. After defining the syntax and operational semantics of qCCS and demonstrating its use by modeling several quantum protocols, the presentation proceeds along the lines of CCS: first, a notion of strong bisimulation of quantum processes is introduced, and the corresponding equivalence relation is shown to be a congruence, that is, preserved by all the combinators of qCCS. Then, a notion of weak bisimulation is defined that does not discriminate between internal actions. While the corresponding equivalence itself is not preserved by summation, a notion of process equality can be derived that is again a congruence. Furthermore, a notion of approximate strong bisimulation is introduced that captures the inherent imprecision of quantum processes and is more suitable in practice.

While the quantum aspects of the work are hard to digest for the layman, the reader familiar with process algebra will enjoy the correspondence of concepts known from a classical setting with those in the quantum world. An envisioned extension of the work to model and analyze security properties (analogous to the Spi calculus) promises interesting future results.