Efficient and Timely Revocation of V2X Credentials

Efficient and Timely Revocation of V2X Credentials

Speakers: Gianluca Scopelliti

Conference: NDSS Symposium

YouTube: https://www.youtube.com/watch?v=5KwlnQEqeJU

Overview

In the rapidly evolving landscape of Intelligent Transport Systems (ITS), the security and trustworthiness of Vehicle-to-Everything (V2X) communication are paramount for ensuring road safety and enabling advanced functionalities like autonomous driving and platooning. A fundamental pillar of this security is the ability to efficiently and promptly revoke cryptographic credentials belonging to misbehaving or malicious vehicles. However, existing V2X standards often provide ambiguous guidance on revocation mechanisms, and current implementations frequently struggle with scalability, reactivity, or both, leaving critical windows during which malicious actors can cause harm.

This talk, presented by Gianluca Scopelliti at the NDSS Symposium, introduces a novel and robust self-revocation scheme designed to address these long-standing challenges. The core problem tackled is how to identify and neutralize faulty or malicious network participants—such as vehicles reporting inaccurate data—by ensuring their credentials are revoked in a timely and unbypassable manner. The proposed solution leverages Trusted Components (TCs) embedded within vehicles for secure credential management, building upon decentralized self-revocation principles.

The research makes several significant contributions: it designs a secure self-revocation scheme guaranteeing revocation within a predictable upper time bound, critically without relying on a trusted time source within the TCs themselves; it formally verifies this design using the TAMARIN prover, demonstrating strong security guarantees against realistic adversaries; and it evaluates the scheme's performance and scalability, showcasing prompt revocation and low resource utilization even under adverse network conditions and a high number of attackers. Furthermore, the scheme's compatibility with state-of-the-art V2X protocols, including EU and US standards (ETSI, SCMS) and Direct Anonymous Attestation (DAA), positions it as a vital advancement for future secure transportation systems.

Background

▶ Watch: Introduction: critical need for timely V2X credential revocation (0:00)

The demanding requirements of modern ITS and advanced V2X use cases, such as vehicle platooning, necessitate robust security protocols. These environments can feature high connection densities, supporting thousands of cars per square kilometer, with message rates up to 50 messages per second and end-to-end latencies as low as 5 to 20 milliseconds. Within this context, key security requirements include verifying message authenticity, guaranteeing unlinkability for privacy, minimizing the repercussions of central trust compromise, and, crucially, enabling the timely revocation of misbehaving vehicles.

V2X participants typically manage two types of cryptographic credentials: long-term credentials used for authenticating with infrastructure, and pseudonymous credentials for privacy-preserving peer-to-peer communication (V2V, V2I, V2P). Pseudonyms are generally short-lived, with lifetimes of up to several weeks, and are regularly rotated to prevent vehicle tracking.

Traditional approaches to revocation fall into two main categories:

1. Active Revocation: Employed by the US SCMS (Security Credential Management System), this method involves distributing Certificate Revocation Lists (CRLs) to all vehicles in real-time. While effective in providing immediate revocation, CRLs grow large over time, leading to substantial computational and communication overheads that make them impractical for real-time, high-density V2X environments. Although optimizations exist, surveys indicate they remain far from ideal. SCMS also utilizes linkage values to reduce CRL size, but this increases the decision delay for revocation.
2. Passive Revocation: Adopted by ETSI (European Telecommunications Standards Institute), this approach relies on the natural expiration of short-lived pseudonym certificates. Malicious vehicles can continue to operate and cause harm until their current pseudonym expires, creating a non-negligible window of vulnerability. To mitigate this, pseudonym lifetimes would need to be drastically shortened, which would, in turn, significantly increase network traffic and heighten the risk of Sybil attacks.

A more novel concept, self-revocation, has emerged in some DAA protocols. In this model, the vehicle itself cooperates in its revocation. A Revocation Authority (RA) broadcasts an Order for Self-Revocation (OSR) containing the identifier of the pseudonym to be revoked. The targeted vehicle's Trusted Component (TC), upon receiving the OSR, is designed to delete the corresponding credentials, thereby preventing the generation of further malicious messages. This approach eliminates the need for large CRLs or extremely short pseudonym lifetimes, offering potential performance and scalability advantages.

However, existing self-revocation schemes often operate under idealized assumptions. They typically do not account for OSR delays or drops in a realistic network, and implicitly rely on the availability of a securely synchronized trusted time source within the TCs. Such a trusted time source is not securely available in current TC implementations. This lack of robust guarantees against a powerful, realistic adversary, particularly concerning network conditions and the absence of trusted time, served as a key motivation for the presented work.

Key Findings

▶ Watch: Analyzing limitations of active and passive V2X revocation (2:40)

The research presents a robust and formally verified self-revocation scheme that significantly advances V2X security. The key findings and contributions can be summarized as follows:

1. Guaranteed Revocation with Predictable Upper Bound: The designed scheme ensures that a misbehaving vehicle's credentials are effectively revoked within a fixed, predictable upper time bound, denoted as Teff. Crucially, this guarantee is achieved without relying on a trusted time source within the vehicle's Trusted Component (TC), a common and often unrealistic assumption in prior work. This predictability provides a strong security assurance that is lacking in many existing active and passive revocation schemes.
2. Formal Verification for Strong Security Guarantees: The entire design was rigorously formally verified using the TAMARIN prover, a symbolic verification tool capable of modeling powerful Dolev-Yao adversaries. This formal analysis demonstrated strong guarantees regarding the scheme's security properties, including the unbypassability of revocation, even in the presence of sophisticated attackers who control the network stack and can manipulate messages.
3. Demonstrated Performance and Scalability: Extensive evaluation through a prototype implementation in a simulated V2X network (Kubernetes-based) confirmed the scheme's efficiency and scalability. The results showed prompt revocation times, often in the order of seconds, significantly outperforming passive revocation. Furthermore, the scheme demonstrated low resource utilization, both in terms of network bandwidth (a few kilobits per second for heartbeats) and computational overhead, even under network malfunctions and a high number of attackers. The Pending Revocation List (PRL) size remained small and manageable, confirming scalability.
4. High Compatibility with Existing V2X Standards and Protocols: The proposed scheme is highly compatible with current standardization efforts. It can significantly improve revocation times and reduce network overhead for ETSI ITS by replacing passive revocation (though requiring TCs). For the US SCMS, it offers a viable alternative to large CRLs, reducing network utilization and nullifying verification overhead. Even DAA protocols that already use self-revocation can benefit from stronger, formally verified guarantees on revocation time and resilience against network issues.
5. Generalizability: The principles and design of this revocation scheme are not limited to V2X. It is applicable to any scenario requiring fast, reliable credential revocation with privacy-preserving pseudonyms, such as smart cities, industrial IoT, or direct mobile-to-mobile communication.

Technical Deep Dive

▶ Watch: Self-revocation concept and existing scheme challenges (3:25)

The core of the proposed solution lies in its robust system design, a realistic attacker model, and a novel approach to managing time and revocation within a Trusted Component (TC).

System Model and Attacker Model

The System Model focuses on V2X participants, primarily vehicles, which are envisioned as integrated systems comprising Electronic Control Units (ECUs) and an On-Board Unit (OBU) responsible for network message processing. Crucially, each vehicle incorporates a Trusted Component (TC), analogous to those used in DAA protocols. The TC is a passive, tamper-resistant hardware module (e.g., a TPM, ARM TrustZone, or TEE) that manages cryptographic credentials and operations, exposing a secure interface to the OBU for tasks like enrollment, pseudonym generation, and message signing. All sensitive operations and cryptographic keys are confined within the TC, preventing direct OBU access.

The Attacker Model assumes a powerful Dolev-Yao style adversary. This adversary has full control over the network stack, capable of tampering with, rearranging, re-sending, and stalling network messages. Furthermore, the attacker has full control over all vehicle hardware and software except the TC itself. This critical assumption implies that the TC cannot rely on a local trusted time source, as any timing components would be part of the untrusted host. Therefore, the design relies on trusted timestamps, or epochs, distributed by the ITS infrastructure to the TCs.

Vehicle Lifecycle and Effective Revocation

The V2X vehicle lifecycle comprises four phases:

1. Enrollment: The vehicle authenticates its TC to the infrastructure to receive a long-term credential.
2. Pseudonym Generation: The TC uses its long-term credential to obtain new pseudonym certificates, either online or offline. Only non-revoked vehicles should be able to obtain new pseudonyms.
3. Operation: Pseudonyms are used to authenticate V2V messages, which are integrity-protected, authenticated, and timestamped by the TC using its internal now variable. Receiving TCs must verify signatures and discard messages older than now - Tv, where Tv is a validity window.
4. Revocation: The RA detects misbehavior and revokes credentials. Only non-revoked vehicles can re-enroll.

Effective revocation is defined as a vehicle being unable to generate valid and fresh V2V messages, either because all its pseudonyms are unusable or its TC is permanently de-synchronized.

Design of the Self-Revocation Scheme

The proposed design addresses the challenges of trusted time and OSR reliability:

1. Heartbeats (HBs) and Pending Revocation List (PRL): The RA periodically distributes authenticated heartbeats (HBs). Each HB contains a Pending Revocation List (PRL) of pseudonyms pending revocation and a timestamp thb.
2. TC Processing of HBs: Upon receiving an HB, the TC first verifies the RA's digital signature. It then checks the freshness of the HB: thb = now - Tv. If valid, the TC synchronizes its internal time: now := max(now, thb).
3. Self-Revocation: The TC then performs self-revocation if any of its currently held pseudonyms appear in the PRL. This puts the TC into a revoked state, denying any subsequent signature requests.
4. Automatic Revocation for De-synchronization: This is a crucial mechanism to counter malicious OBUs. If a revoked vehicle's OBU attempts to evade revocation by dropping HBs, its TC's internal now variable will eventually stand still and become de-synchronized from the network's actual time. Consequently, other vehicles will discard its V2V messages as outdated (due to tmsg > now - Tv). To make this de-synchronization permanent and ensure effective revocation, the design introduces automatic revocation: if a received message's timestamp tmsg is much greater than the TC's now (tmsg > now + Tv), the TC automatically self-revokes. This ensures that attackers cannot postpone revocation indefinitely by simply manipulating HBs.

This design guarantees two key properties:

• If a pseudonym is revoked by the RA, the vehicle will be effectively revoked within a fixed time period Teff.
• Each pseudonym can be removed from the PRL after a fixed time period Tprl since its insertion.

The research derives Teff = 2Tv and Tprl = Tv, where Tv is the validity window for messages.

Formal Verification with TAMARIN Prover

To rigorously prove the correctness and security properties of the design, especially Teff and Tprl, the authors employed the TAMARIN prover 34. TAMARIN is a symbolic verification tool that uses multi-set rewriting rules and first-order logic, incorporating a powerful Dolev-Yao adversary model.

The revocation scheme was modeled in TAMARIN, including the RA, the TC, and a generic V2X message receiver. A significant challenge was modeling the notion of time, as TAMARIN lacks native support for time progression. This was overcome by modeling time as a logical counter, representing discrete time steps, using TAMARIN's multiset built-in. An advance_time rule incremented this counter, and an IsLatestTime restriction ensured the most recent time value was always used. Time steps, timeouts, the PRL, and pseudonyms were all modeled using persistent facts. The parameter Tv was modeled as an arbitrary value to prove properties for any positive Tv.

Three types of lemmas were defined: sanity lemmas (model correctness), functional lemmas (design implementation accuracy), and proof lemmas (verifying Teff and Tprl). A custom Python script (an oracle) was used to guide TAMARIN, preventing infinite loops during time-related proofs.

Key proof lemmas include:

• effective_revocation: Proves that no V2V message signed by a revoked pseudonym will be accepted by another entity whose internal time is t_rev + Tv or higher, directly supporting Teff = 2Tv.
• no_heartbeats_processed_after_tolerance: Demonstrates that a revoked TC cannot process HBs whose timestamp is greater than t_rev + Tv, ensuring pseudonyms can be safely removed from the PRL after Tprl = Tv.

Extensions

The paper also explores extensions: if TCs had access to a trusted time source, their internal time could advance automatically, simplifying the design. Security enhancements include encrypting HBs with a pre-shared symmetric key to prevent malicious OBUs from selectively dropping HBs, and using the PRL as a lightweight CRL for active revocation during message verification, further reducing average revocation time.

Demo / Proof of Concept

▶ Watch: System and attacker models for V2X revocation (4:00)

To validate the design in a practical setting, a full prototype was implemented and evaluated within a simulated V2X network.

Implementation Details

The prototype was deployed on a Kubernetes cluster with 8 worker nodes, simulating 400 vehicles operating within a single edge area, divided into 20 distinct groups. A custom V2X protocol, based on existing work, was developed, utilizing a group symmetric key for V2V message signing and verification. TCs autonomously generated pseudonyms, which were randomized identifiers appended as metadata to messages. The protocol satisfied all defined functional requirements.

The infrastructure was centralized, with an RA handling enrollment and revocation. Within each edge area, a Road-Side Unit (RSU) fetched the latest HB from the RA and broadcast it to local vehicles. Vehicles communicated V2V messages only with neighbors in the same group. The TC exposed a defined API for operations like JOIN, CREATE, SIGN, VERIFY, and HEARTBEAT. Revocation was triggered by a reporter component that inspected V2X traffic and periodically reported a randomly selected pseudonym for revocation to the RA, which then added it to the PRL.

Attacker Levels

Three main attacker levels were simulated for the OBU's behavior regarding HBs:

1. Honest: The OBU faithfully relayed HBs to the TC immediately upon reception.
2. Smart: The OBU actively dropped HBs that contained any of its own pseudonyms, attempting to evade revocation.
3. Blind: HBs were encrypted, preventing the OBU from inspecting their content. The blind attacker made a guess, relaying only one HB every Tv to maintain minimal clock synchronization and prevent automatic revocation, while still trying to avoid specific revocations.

Experimental Setup

The simulation parameters were carefully chosen to reflect realistic V2X conditions and test the scheme's resilience:

• Vehicles: 400 simulated vehicles, with 10% designated as malicious. Each vehicle maintained two concurrent pseudonyms.
• HB/V2V Frequency: HBs were generated every second by the RA. V2V messages were also generated every second.
• Network Malfunctions: The RSU simulated network malfunctions by dropping or delaying HBs with a 0.4 probability.
• Malicious Behavior: Malicious vehicles replayed messages with a 0.3 probability.
• Revocation Rate: A pseudonym was reported and revoked every 10 seconds.
• Key Parameters: Tv (validity window) was set to 30 seconds, leading to a theoretical Teff of 60 seconds and Tprl of 30 seconds.

PRL Size Evaluation

To assess the scalability of the Pending Revocation List (PRL), the process of adding and removing pseudonyms was modeled as a finite state Markov chain. States represented possible PRL sizes. Probabilities of gaining (Gi,k) and losing (Li,k) pseudonyms were calculated using binomial distributions and combined into a Markov matrix. The stationary distribution was then computed to determine the expected average PRL size. Two baseline scenarios were considered: honest pseudonym revocation (1% per day) and attacker behavior (75% chance of revocation every 30 minutes).

Defensive Implications

▶ Watch: Proposed mechanism: authenticated heartbeats and Pending Revocation List (5:45)

The presented self-revocation scheme offers significant improvements for V2X security and provides clear implications for defenders. Its robust design, formal verification, and practical evaluation offer a pathway to more secure and resilient intelligent transport systems.

Key Benefits for Defenders

1. Deterministic Upper Bound on Revocation Time: The most critical defensive advantage is the guaranteed Teff = 2Tv. This provides a predictable maximum time window during which a misbehaving vehicle can operate. Unlike active revocation with its unpredictable CRL update delays or passive revocation with its reliance on arbitrary pseudonym expiration, defenders know the maximum exposure time. In the simulated environment, with Tv = 30 seconds, Teff was 60 seconds, and actual median revocation times were often much lower (17-32 seconds).
2. Low Overhead and High Scalability: The scheme requires minimal network bandwidth for Heartbeats (around 12 KBit/s in worst-case scenarios), a substantial improvement over large, growing CRLs. Computational overhead is also low, as HB distribution scales with the number of edge areas, not individual vehicles. The PRL size remains small (typically <17 pseudonyms even under heavy attack), ensuring the system scales well to large numbers of revocations without becoming a bottleneck.
3. Resilience to Network Malfunctions and Smart Attackers: The "automatic revocation" mechanism effectively counters attackers who attempt to evade revocation by dropping HBs. Even with a 0.4 probability of HB loss, the system ensures timely revocation by de-synchronizing the TC. Encrypting HBs (blind attacker scenario) further enhances this, leading to more frequent automatic revocations.
4. Compatibility and Generalizability: The scheme can be integrated with existing V2X standards (ETSI, SCMS) to significantly enhance their revocation capabilities. This means defenders don't necessarily need to overhaul their entire V2X infrastructure but can augment it with this more robust mechanism. Its generalizability extends its applicability to other critical infrastructure scenarios requiring fast credential revocation.

Actionable Advice for Defenders

• Prioritize TC Integration: For organizations deploying V2X systems, prioritizing the inclusion of Trusted Components (TCs) that support secure credential management and the proposed self-revocation logic is paramount. TCs are the cornerstone of this scheme's security.
• Implement Robust HB Distribution: Ensure the V2X infrastructure reliably distributes Heartbeats (HBs) from the Revocation Authority (RA) to all Road-Side Units (RSUs) and subsequently to vehicles. While the scheme is resilient to some HB loss, consistent delivery aids faster revocation.
• Consider Encrypted HBs: To further deter sophisticated attackers who might attempt to selectively filter HBs, implementing encrypted HBs with a pre-shared symmetric key is a valuable security enhancement. This limits the OBU's ability to identify and drop relevant revocation messages.
• Leverage PRL as a Lightweight CRL: The Pending Revocation List (PRL), due to its small size, can be optionally used as a lightweight CRL for active revocation checks during message verification. This can further reduce average revocation times without incurring significant overhead, especially in high-risk scenarios.
• Careful Selection of Tv: The choice of the validity window Tv is a crucial trade-off. A smaller Tv leads to shorter Teff and thus a safer system, but increases HB frequency and resource utilization. A larger Tv improves resilience and efficiency but slows revocation. Defenders must balance these factors based on the specific criticality and operational environment of their V2X deployment. Even Teff values of 30 minutes are a significant improvement over passive revocation.

Limitations and Future Considerations

Defenders should also be aware of the scheme's limitations:

• Vehicles Powered Off: Vehicles that are powered off cannot process HBs and may miss revocations. Persisting the last_thb value in the TC helps for short offline periods, but for longer periods, re-enrollment and explicit revocation status checks are necessary.
• TC Self-Identification of Pseudonyms: The assumption that TCs can identify their own pseudonyms within the PRL might be challenged if pseudonyms are frequently rotated or cryptographically derived. More efficient cryptographic tokens might be needed here.
• Denial-of-Service (DoS) Attacks: Jamming attacks could de-synchronize vehicles, preventing HB processing. However, such attacks would likely disrupt V2X communication regardless of the revocation mechanism, so this scheme does not introduce additional vulnerability to DoS.
• Privacy vs. Re-enrollment Prevention: While the design preserves privacy for credential management, Requirement 6 (revoked vehicles must not re-enroll) necessitates mapping pseudonyms back to canonical identities for denial-listing. This compromises data minimization, especially for DAA approaches that derive pseudonyms autonomously. This is a fundamental conundrum in V2X security that requires further research into privacy-preserving solutions for blocking malicious actors from re-joining networks without impacting well-behaved actors.

Key Takeaways

• Timely Revocation is Critical but Challenging: Existing V2X credential revocation schemes (active, passive) suffer from scalability issues, high overhead, and significant time windows for malicious activity, posing a risk to road safety.
• Self-Revocation with TCs Offers a Superior Approach: Leveraging Trusted Components (TCs) for decentralized self-revocation provides a highly scalable and efficient alternative to traditional methods, minimizing network and computational overhead.
• Formally Verified Guarantees on Revocation Time: The scheme provides a unique, formally verified guarantee of effective revocation within a predictable upper time bound (Teff = 2Tv), crucially achieved without requiring a trusted time source within the TC itself.
• Resilience Against Sophisticated Attackers: The design, particularly its automatic revocation mechanism, is resilient to smart attackers attempting to evade revocation by manipulating Heartbeats (HBs) and can even benefit from encrypted HBs.
• High Compatibility and Broad Applicability: The proposed scheme is compatible with major V2X standards (ETSI, SCMS) and DAA protocols, offering a generalizable solution for fast, reliable credential revocation in various privacy-preserving, low-latency communication scenarios beyond V2X.
• Strategic Trade-offs and Future Privacy Challenges: The choice of the validity window (Tv) involves a trade-off between security (shorter Teff) and resource efficiency. Furthermore, balancing privacy with the need to prevent re-enrollment of revoked entities remains a complex challenge for future research.

About the Speaker(s)

Gianluca Scopelliti presented this research on "Efficient and Timely Revocation of V2X Credentials" at the NDSS Symposium. The transcript provides no further specific biographical details such as his title or company affiliation. His presentation focused on the technical aspects and contributions of the work.