Security verification of BB84 protocol using PRISM model-checker

The fast developing theory of Quantum Communications describes the Quantum Mechanical based concepts. Considering their classical counterparts for information transmission securely through the Quantum Channel, we have to deal with Quantum Cryptography. Quantum key distribution is the most well-known application of quantum cryptography. While current analysis of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, a simpler probabilistic model checking is used to some extent which is compatible with classical implementation as an alternative. In this presentation the PRISM model checking tool - by Birmingham group - is employed inasmuch as details to measure the security of the full BB84 protocol when the presence of some additional parameters are taken into account while considering two eavesdropper's attacks.