Modeling and verification of server aided verification protocol using NuSMV

Vikram Saralaya, J. K. Kishore, Sateesh Reddy, Sanjay Singh

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

Abstract

Cryptographic algorithms are useful for signing and verifying the authenticity of sender of the message. The verifier may not have the required computational ability and relies on a powerful server to aid the verification process. The server and the illegitimate prover/signer may collaborate and try to cheat the verifier. A legitimate prover can also repudiate the message sent by himself. In this paper we model the scenario where the legitimate, cheating or repudiating prover sign's the message. The verifier then authenticates the message via an untrusted server. Specifications are written using CTL(Computational-Tree Logic). NuSMV(extension of Symbolic Model Verifier) is the tool used to verify the specifications.

Original languageEnglish
Title of host publicationTrends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings
Pages486-495
Number of pages10
DOIs
Publication statusPublished - 28-10-2011
Event1st International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011 - Tirunelveli, Tamil Nadu, India
Duration: 23-09-201125-09-2011

Publication series

NameCommunications in Computer and Information Science
Volume204 CCIS
ISSN (Print)1865-0929

Conference

Conference1st International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011
CountryIndia
CityTirunelveli, Tamil Nadu
Period23-09-1125-09-11

Fingerprint

Protocol Verification
Servers
Server
Network protocols
Computer simulation
Modeling
Specification
Specifications
Logic
Verify
Scenarios
Model

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)

Cite this

Saralaya, V., Kishore, J. K., Reddy, S., & Singh, S. (2011). Modeling and verification of server aided verification protocol using NuSMV. In Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings (pp. 486-495). (Communications in Computer and Information Science; Vol. 204 CCIS). https://doi.org/10.1007/978-3-642-24043-0_49
Saralaya, Vikram ; Kishore, J. K. ; Reddy, Sateesh ; Singh, Sanjay. / Modeling and verification of server aided verification protocol using NuSMV. Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings. 2011. pp. 486-495 (Communications in Computer and Information Science).
@inproceedings{b8b73ac0491546a0be4ee477b0162e9e,
title = "Modeling and verification of server aided verification protocol using NuSMV",
abstract = "Cryptographic algorithms are useful for signing and verifying the authenticity of sender of the message. The verifier may not have the required computational ability and relies on a powerful server to aid the verification process. The server and the illegitimate prover/signer may collaborate and try to cheat the verifier. A legitimate prover can also repudiate the message sent by himself. In this paper we model the scenario where the legitimate, cheating or repudiating prover sign's the message. The verifier then authenticates the message via an untrusted server. Specifications are written using CTL(Computational-Tree Logic). NuSMV(extension of Symbolic Model Verifier) is the tool used to verify the specifications.",
author = "Vikram Saralaya and Kishore, {J. K.} and Sateesh Reddy and Sanjay Singh",
year = "2011",
month = "10",
day = "28",
doi = "10.1007/978-3-642-24043-0_49",
language = "English",
isbn = "9783642240423",
series = "Communications in Computer and Information Science",
pages = "486--495",
booktitle = "Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings",

}

Saralaya, V, Kishore, JK, Reddy, S & Singh, S 2011, Modeling and verification of server aided verification protocol using NuSMV. in Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings. Communications in Computer and Information Science, vol. 204 CCIS, pp. 486-495, 1st International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Tirunelveli, Tamil Nadu, India, 23-09-11. https://doi.org/10.1007/978-3-642-24043-0_49

Modeling and verification of server aided verification protocol using NuSMV. / Saralaya, Vikram; Kishore, J. K.; Reddy, Sateesh; Singh, Sanjay.

Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings. 2011. p. 486-495 (Communications in Computer and Information Science; Vol. 204 CCIS).

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

TY - GEN

T1 - Modeling and verification of server aided verification protocol using NuSMV

AU - Saralaya, Vikram

AU - Kishore, J. K.

AU - Reddy, Sateesh

AU - Singh, Sanjay

PY - 2011/10/28

Y1 - 2011/10/28

N2 - Cryptographic algorithms are useful for signing and verifying the authenticity of sender of the message. The verifier may not have the required computational ability and relies on a powerful server to aid the verification process. The server and the illegitimate prover/signer may collaborate and try to cheat the verifier. A legitimate prover can also repudiate the message sent by himself. In this paper we model the scenario where the legitimate, cheating or repudiating prover sign's the message. The verifier then authenticates the message via an untrusted server. Specifications are written using CTL(Computational-Tree Logic). NuSMV(extension of Symbolic Model Verifier) is the tool used to verify the specifications.

AB - Cryptographic algorithms are useful for signing and verifying the authenticity of sender of the message. The verifier may not have the required computational ability and relies on a powerful server to aid the verification process. The server and the illegitimate prover/signer may collaborate and try to cheat the verifier. A legitimate prover can also repudiate the message sent by himself. In this paper we model the scenario where the legitimate, cheating or repudiating prover sign's the message. The verifier then authenticates the message via an untrusted server. Specifications are written using CTL(Computational-Tree Logic). NuSMV(extension of Symbolic Model Verifier) is the tool used to verify the specifications.

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

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

U2 - 10.1007/978-3-642-24043-0_49

DO - 10.1007/978-3-642-24043-0_49

M3 - Conference contribution

SN - 9783642240423

T3 - Communications in Computer and Information Science

SP - 486

EP - 495

BT - Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings

ER -

Saralaya V, Kishore JK, Reddy S, Singh S. Modeling and verification of server aided verification protocol using NuSMV. In Trends in Computer Science, Engineering and Information Technology - First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Proceedings. 2011. p. 486-495. (Communications in Computer and Information Science). https://doi.org/10.1007/978-3-642-24043-0_49