Symbolic Analysis of an Electric Vehicle Charging Protocol

In this paper, we describe our analysis of a recently proposed electric vehicle charing protocol. The protocol builds on complex 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 no single existing tool for security protocol analysis 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 ProVerif, to check all important properties of the protocol.