Symbolic Analysis of an Electric Vehicle Charging Protocol
Li Li, Jun Pang, Yang Liu, Jun Sun, Jin Song Dong · 2014
In this paper, we describe our analysis of a recently proposed electric vehicle charing protocol. The protocol builds on complicated cryptographic primitives such as commitment, zero-knowledge proofs, BBS+ signature and etc. Moreover, interesting properties such as secrecy, authentication, anonymity, and location privacy are claimed on this protocol. It thus presents a challenge for formal verification, as existing tools for security protocol analysis lack support for all the required features. In our analysis, we employ and combine the strength of two state-of-the-art symbolic verifiers, Tamarin and Prove if, to check all important properties of the protocol.