Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/ICECCS.2014.11 | ICECCS |
Keywords | Field | DocType |
security protocol analysis,symbolic analysis,anonymity location,electric vehicle charging protocol,privacy,authentication,electrical engineering computing,symbolic verification,cryptographic protocols,secrecy,electric vehicle charing protocol,formal verification,electric vehicles,electric vehicle charing protocol, symbolic verification, secrecy, authentication, anonymity location, privacy,protocols,cryptography | Authentication,Challenge-Handshake Authentication Protocol,Computer security,Computer science,Computer network,Otway–Rees protocol,Cryptographic primitive,Authentication protocol,Symbolic data analysis,Formal verification,Universal composability | Conference |
Citations | PageRank | References |
1 | 0.36 | 20 |
Authors | ||
5 | ||