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. © 2011 Springer-Verlag Berlin Heidelberg.