Symbolic analysis of an electric vehicle charging protocol

• Main Authors: LI, Li, PANG, Jun, LIU, Yang, SUN, Jun, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2014
• Subjects: Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4983; https://ink.library.smu.edu.sg/context/sis_research/article/5986/viewcontent/ICECCS14.pdf
• Institution: Singapore Management University

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, zeroknowledge 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 stateof-the-art symbolic verifiers, Tamarin and ProVerif, to check all important properties of the protocol.