A Process Algebra for Reasoning About Quantum Security (joint work with Paulo Mateus)
Electronic Notes in Theoretical Computer Science, 170:3-21, 2007. © Elsevier. To Appear.

Abstract: 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), and incorporate it in the syntax of the algebra. Probabilistic transition systems give the semantic support 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 also 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.

Category / Keywords. Quantum process algebras, quantum polynomial-time machines, quantum zero-knowledge proofs.

Publication Info. Preliminary version presented at the 3rd International Workshop on Quantum Programming Languages (QPL). Affiliated Workshop of LICS'05, Chicago, IL, USA, June 30-July 1 2005.

Date: 04 April 2005, last revised 01 November 2005.