Expanding Human knowledge through research at the highest levels of their disciplines.

Modeling and Verification of Fiat-Shamir Zero Knowledge Authentication Protocol

Prof. Murari Singh Choudhary
(Department of Information and Communication Technology, GGESTC)

Book Title: Advances in Computer Science and Information Technology. Computer Science and Engineering

Abstract: Model checking is a multi-purpose, automatic technique for verifying finite-sate concurrent systems. Formal verification methods have quite recently become usable by industry. Presently model checking has been widely used in hardware, software validation and security protocol analysis. Finite-Shamir is one of the many zero-knowledge authentication protocol which is used for security autonation purpose. In this paper, we have proposed a formal model of Fiat-Shamir authentication protocol using Finite State klachine (FSM). Security requirements are represented using Computation Tree Logic (CTL). These security re-quirements are verified arid analyzed using symbolic model checker tool NuSMV. Based on our verification we have identified one of the security flaw of Flat-Shamir protocol using the Nu.SMV model checker.

Introduction: An authentication protocol is a type of cryptographic protocol with the pur-pose of authenticating entities wishing to communicate securely. In password authentication, the claimant needs to send her secret to the verifier. It leads to a problem of eavesdropping. In addition, a dishonest verifier could reveal the password to others or use it to impersonate the claimant. In chalknge-response entity authentication, the claimant's secret is not sent to the verifier. The claimant applies a function on the challenge sent by the verifier that includes her secret. In some challenge responsesmethods, the verifier actually knows the clahnants secret, which could be misused by the dishonest verifier. In other methods, the verifier can extract some information about the secret from the claimant by choosing a preplanned set of challenges. In zero-knowledge authentication RR, the claimant does not reveal anything that might cause danger to the confidentiality of the secret. The claimant proves to the verifier that she knows a secret, without revealing it. The interactions are to designed that they can not lead to revealing or guessing the secret. After exchanging messages, the verifier only knows that the claimant does or does not have the secret, nothing more.