Formal Analysis of V2X Revocation Protocols

摘要: Research on vehicular networking (V2X) security has produced a range of securitymechanisms and protocols tailored for this domain, addressing both privacy. Typically, the analysis these proposals largely been informal. However, formal can be used to expose flaws ultimately provide higher level assurance in protocols. This paper focusses particular element mechanisms V2X found many proposals, that is revocation malicious or misbehaving vehicles from system by invalidating their credentials. needs performed an unlinkable way vehicle privacy even context regularly changing pseudonyms. The Rewire scheme Forster et al. its subschemes Plain R-token aim solve challenge means cryptographic solutions trusted hardware. Formal using Tamarin prover identifies two flaws: one previously reported lierature concerned with functional correctness protocol, unknown flaw concerning authentication property scheme. In response we propose Obscure Token (O-token), extension enable preserving manner. Our approach addresses properties introducing additional key-pair, which offers stronger verifiable guarantee successful without resolving long-term identity. Moreover O-token first protocol co-designed model.