A Process Algebra for Reasoning About Quantum Security

We present a process algebra for specifying and reasoning about quantum security protocols. Since the computational power of the protocol agents must be restricted to quantum polynomial-time, we introduce the logarithmic cost quantum random access machine (QRAM) similar to [S.A. Cook, R.A. Reckhow, Time bounded random access machines, Journal of Computer and System Sciences 7 (1973) 354–375, E. Knill, Conventions for quantum pseudocode, Technical Report LAUR-96-2724, Los Alamos National Laboratory (1996)], and incorporate it in the syntax of the algebra. Probabilistic transition systems give the semantic for the process algebra. Term reduction is stochastic because quantum computation is probabilistic and, moreover, we consider a uniform scheduler to resolve non-deterministic choices. With the purpose of defining security properties, we introduce observational equivalence and quantum computational indistinguishability, and show that the latter is a congruence relation. A simple corollary of this result asserts that any security property defined via emulation is compositional. Finally, we illustrate our approach by establishing the concept of quantum zero-knowledge protocol.