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

Fingerprint

Authentication
Network protocols
Model checking
Finite automata
Computer hardware
Defects
Industry

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications

Cite this

Maurya, A. K., Choudhary, M. S., Ajeyaraj, P., & Singh, S. (2012). Modeling and verification of Fiat-Shamir zero knowledge authentication protocol. In Advances in Computer Science and Information Technology: Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings (PART 2 ed., pp. 61-70). (Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST; Vol. 85, No. PART 2). https://doi.org/10.1007/978-3-642-27308-7_6
Maurya, Amit K. ; Choudhary, Murari S. ; Ajeyaraj, P. ; Singh, Sanjay. / Modeling and verification of Fiat-Shamir zero knowledge authentication protocol. Advances in Computer Science and Information Technology: Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings. PART 2. ed. 2012. pp. 61-70 (Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST; PART 2).
@inproceedings{5cba71415515435d80bcc501a8443bf1,
title = "Modeling and verification of Fiat-Shamir zero knowledge authentication protocol",
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.",
author = "Maurya, {Amit K.} and Choudhary, {Murari S.} and P. Ajeyaraj and Sanjay Singh",
year = "2012",
month = "12",
day = "1",
doi = "10.1007/978-3-642-27308-7_6",
language = "English",
isbn = "9783642273070",
series = "Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST",
number = "PART 2",
pages = "61--70",
booktitle = "Advances in Computer Science and Information Technology",
edition = "PART 2",

}

Maurya, AK, Choudhary, MS, Ajeyaraj, P & Singh, S 2012, Modeling and verification of Fiat-Shamir zero knowledge authentication protocol. in Advances in Computer Science and Information Technology: Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings. PART 2 edn, Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST, no. PART 2, vol. 85, pp. 61-70, 2nd International Conference on Computer Science and Information Technology, CCSIT 2012, Bangalore, India, 02-01-12. https://doi.org/10.1007/978-3-642-27308-7_6

Modeling and verification of Fiat-Shamir zero knowledge authentication protocol. / Maurya, Amit K.; Choudhary, Murari S.; Ajeyaraj, P.; Singh, Sanjay.

Advances in Computer Science and Information Technology: Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings. PART 2. ed. 2012. p. 61-70 (Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST; Vol. 85, No. PART 2).

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

TY - GEN

T1 - Modeling and verification of Fiat-Shamir zero knowledge authentication protocol

AU - Maurya, Amit K.

AU - Choudhary, Murari S.

AU - Ajeyaraj, P.

AU - Singh, Sanjay

PY - 2012/12/1

Y1 - 2012/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84888419512&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84888419512&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-27308-7_6

DO - 10.1007/978-3-642-27308-7_6

M3 - Conference contribution

SN - 9783642273070

T3 - Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST

SP - 61

EP - 70

BT - Advances in Computer Science and Information Technology

ER -

Maurya AK, Choudhary MS, Ajeyaraj P, Singh S. Modeling and verification of Fiat-Shamir zero knowledge authentication protocol. In Advances in Computer Science and Information Technology: Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings. PART 2 ed. 2012. p. 61-70. (Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST; PART 2). https://doi.org/10.1007/978-3-642-27308-7_6