Modeling and verification of Fiat-Shamir zero knowledge authentication protocol

Amit K. Maurya, Murari S. Choudhary, P. Ajeyaraj, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Model checking is a multi-purpose, automatic technique for verifying finite-state 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. Fiat-Shamir is one of the many zero-knowledge authentication protocol which is used for security authentication purpose. In this paper, we have proposed a formal model of Fiat-Shamir authentication protocol using Finite State Machine (FSM). Security requirements are represented using Computation Tree Logic (CTL). These security requirements are verified and analyzed using symbolic model checker tool NuSMV. Based on our verification we have identified one of the security flaw of Fiat-Shamir protocol using the NuSMV model checker.

Original languageEnglish
Title of host publicationAdvances in Computer Science and Information Technology
Subtitle of host publicationComputer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings
Pages61-70
Number of pages10
EditionPART 2
DOIs
Publication statusPublished - 01-12-2012
Event2nd International Conference on Computer Science and Information Technology, CCSIT 2012 - Bangalore, India
Duration: 02-01-201204-01-2012

Publication series

NameLecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST
NumberPART 2
Volume85
ISSN (Print)1867-8211

Conference

Conference2nd International Conference on Computer Science and Information Technology, CCSIT 2012
CountryIndia
CityBangalore
Period02-01-1204-01-12

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Modeling and verification of Fiat-Shamir zero knowledge authentication protocol'. Together they form a unique fingerprint.

Cite this