Formal verification of privacy properties in electric vehicle charging

Abstract

Electric vehicles are an up-and-coming technology that provides significant environmental benefits. A major challenge of these vehicles is their somewhat limited range, requiring the deployment of many charging stations. To effectively deliver electricity to vehicles and guarantee payment, a protocol was developed as part of the ISO 15118 standardization effort. A privacy-preserving variant of this protocol, POPCORN, has been proposed in recent work, claiming to provide significant privacy for the user, while maintaining functionality. In this paper, we outline our approach for the verification of privacy properties of the protocol. We provide a formal model of the expected privacy properties in the applied Pi-Calculus and use ProVerif to check them. We identify weaknesses in the protocol and suggest improvements to address them.