Verification of Quantum Protocols with a Probabilistic Model-Checker

Channel modeling is crucial for studying the behavior of quantum channels in order to build an efficient error correction scheme in addition to security verification of different protocols. While most current analyses of quantum protocols use a traditional mathematical approach, we employ a simpler probabilistic model checking which is more compatible with classical implementations to investigate the dependency of the security on the quantum channel noise. We also compare a couple of eavesdropping strategies from the security point of view.