We are interested in applying formal verification techniques to prove security of quantum systems, in order to take advantage of the theories, techniques and tools of classical security analysis. In particular we focus on the process calculus approach. We review previous work on process calculus for classical and quantum systems, and identify a mismatch between typical security statements in the classical process calculus world and the quantum information-theoretic world. To bridge this gap, we define a new notion of information-theoretic indistinguishability in process calculus, and prove that is implied by an existing notion of probabilistic indistinguishability. Joint work with Pedro Adão and Paulo Mateus.