  Several quantum process algebras have been proposed and successfully applied
in verification of quantum cryptographic protocols. All of the bisimulations
proposed so far for quantum processes in these process algebras are
state-based, implying that they only compare individual quantum states, but not
a combination of them. This paper remedies this problem by introducing a novel
notion of distribution-based bisimulation for quantum processes. We further
propose an approximate version of this bisimulation that enables us to prove
more sophisticated security properties of quantum protocols which cannot be
verified using the previous bisimulations. In particular, we prove that the
quantum key distribution protocol BB84 is sound and (asymptotically) secure
against the intercept-resend attacks by showing that the BB84 protocol, when
executed with such an attacker concurrently, is approximately bisimilar to an
ideal protocol, whose soundness and security are obviously guaranteed, with at
most an exponentially decreasing gap.
