Integration and formal security analysis of a quantum key distribution scheme within CHAP protocol

In a security context, to render a cryptosystem more resistant against man-in-the-middle and impersonation attacks, an authentication mechanism has to be considered. CHAP protocol (Challenge Handshake Authentication Protocol) is among the most widely spread authentication technique used within Local Area Networks. To offer greater robustness and privacy, we intend through our present paper to introduce a new quantum extension of CHAP that integrates quantum cryptography and takes advantage of its benefits such as eavesdropping detection, random secret key generation and unconditional security. A new scheme using a previously shared entangled qubits pairs with quantum unitary operators to ensure key agreement and mutual authentication is performed. To analyze the security of the proposed protocol, we use the PRISM tool as a model checker. We particularly focus on the security property of minimizing the quantity of information about the key that an enemy can obtain from applying a "man in the middle" attack. If we act on the parameters of the channel and the eavesdropper, we prove that this security property is affected by varying the efficiency of the channel as well as the power of the enemy. More interestingly, we show that the enemy could never be able to retrieve the value of the key.