Verification of Quantum Bit Commitment Protocols using Bisimulation Techniques

Given the current progress in the development of more and more performing quantum computers, the field of quantum cryptography is making a return, after its golden age in the 1990s. The main feature that made quantum cryptography so interesting is that, in certain cases, it can provide the so-called unconditional security, which is a security notion that declares that the system is secure against adversaries with unlimited computing resources and time. This allows the creation of cryptographic protocols based on the principles of quantum mechanics and mathematically verifiable. However, the security proof related to these protocols can often be tedious and very complicated, as demonstrated by the first proof of the BB84 protocol by Dominic Meyers. A different approach for the verification of quantum cryptographic protocols is given by the so-called process algebras. This method has been used successfully in the field of classical cryptographic protocols, for example to prove the security of El Gamal encryption from the Decision Diffie-Hellman (DDH). The main step of the process algebra approach is given by the use of the notion of bisimulation. In the last years, indeed, several quantum process algebras have been proposed, like qCCS and CQP, and they have been used to verify different types of quantum protocols, starting from quantum teleportation and arriving to quantum key distribution protocols like the BB84 and the EDP-based protocol. In this thesis, focusing on qCCS, we use the process algebra approach combined with different types of notions deriving from bisimulation, to analyze the security proprieties of two different types of quantum bit commitment protocols: the BB84 quantum bit commitment protocol and the Kent relativistic bit commitment protocol.