Modeling and verification of Fiat-Shamir zero knowledge authentication protocol

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

doi:10.1007/978-3-642-27308-7_6

Modeling and verification of Fiat-Shamir zero knowledge authentication protocol

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

Department of Information and Communication Technology, Manipal Institute of Technology, Manipal

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Advances in Computer Science and Information Technology
Subtitle of host publication	Computer Science and Engineering - Second International Conference, CCSIT 2012, Proceedings
Pages	61-70
Number of pages	10
Edition	PART 2
DOIs	https://doi.org/10.1007/978-3-642-27308-7_6
Publication status	Published - 01-12-2012
Event	2nd International Conference on Computer Science and Information Technology, CCSIT 2012 - Bangalore, India Duration: 02-01-2012 → 04-01-2012

Publication series

Name	Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering, LNICST
Number	PART 2
Volume	85
ISSN (Print)	1867-8211

Conference

Conference	2nd International Conference on Computer Science and Information Technology, CCSIT 2012
Country/Territory	India
City	Bangalore
Period	02-01-12 → 04-01-12

All Science Journal Classification (ASJC) codes

Computer Networks and Communications

Access to Document

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

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. et al. / 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 = dec,

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",

note = "2nd International Conference on Computer Science and Information Technology, CCSIT 2012 ; Conference date: 02-01-2012 Through 04-01-2012",

}

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. et al.
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 proceeding › Conference 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

AN - SCOPUS:84888419512

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

T2 - 2nd International Conference on Computer Science and Information Technology, CCSIT 2012

Y2 - 2 January 2012 through 4 January 2012

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). doi: 10.1007/978-3-642-27308-7_6

Modeling and verification of Fiat-Shamir zero knowledge authentication protocol

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this