Simulation and Analysis of Bb84 Protocol by Model Checking
Quantum Cryptography or Quantum Key Distribution (QKD) is a technique to securely distribute a bit string, among two parties by using laws of quantum mechanics. Its security relies on foundations of quantum mechanics, where as classical cryptography relies on difficulty of certain mathematical problems that can not able to provide unconditional security. Progress of research in this field indicates that QKD will be available outside the laboratory within next few years. These devices have now become complex and more effort is needed for their verification. In this paper, the authors will use the PRISM tool to analyze the security of BB84 protocol and more specifically the property of eavesdropping detection by combining the parameters of quantum channel and power of eavesdropper.