Intrusion detection in zero knowledge system using model checking approach

The number of services provided to the modern users of todays' generation is countless and ever increasing. However, most of these services require the user to login with a username and a password. These sensitive information has to be sent across the network, which is highly insecure, and can be tapped by any unauthorized individual without much difficulty. The Zero Knowledge protocol provides authentication without the need to send any private and confidential information across the network. Only mathematical computations on these confidential information have to be sent across. In this paper, we have modeled the general working of the Zero Knowledge system by considering the various states that a prover (sender) and a verifier (receiver) will be in during the execution of the protocol, and have proved that the authentication of the prover is possible. Zero Knowledge system is usually considered to be unintrudeable, but that does not stop hackers from attempting to intrude this protocol. So in this paper, we have also considered the various states that an intruder will be in while intruding, and have shown that it is possible for the user to detect if somebody is trying to intrude the Zero Knowledge system. The tool used to model the system is NuSMV.