Formal modeling and model checking of SAV protocol in wireless mobile terminal
Xie Guang-yin · Jisuanji yingyong yanjiu · 2014
For the current public key digital signature scheme,when the verifier is the mobile smart devices which is too weak to calculate,verifier in the verification process need the aid of a powerful server to assist in the verification process.SAV(serveraided verification) protocol is a security protocol of calculation-aid and signature verification with server for wireless mobile terminals.This paper modeled the prover,verifier and server of SAV protocol with the finite state machine and verified possible deception and denial behavior using NuSMV tools.The result showed that the protocol defects were found,then it analyzed the reasons and proposed viable solutions.