A Cyber-Resilient and Privacy-Preserving Session Protocol for Connected Vehicles in Software-Defined Edge Infrastructure

Co-authored with Ndikuriyo Don Christ Ajax, Dhieu Grace Nyankir Gabriel, and Baseem Al-Athwari at the Department of Smart Computing, Kyungdong University, South Korea.

Connected and software-defined vehicles increasingly interact with edge infrastructure for identity verification, access control, and payment in contexts such as smart parking. Existing systems leave failure modes unaddressed: duplicate billing from repeated payment messages, privacy exposure through plate-payment linkage, and unsafe access decisions from low-confidence ALPR (automatic license plate recognition) readings.

This paper introduces a formally verified, privacy-preserving session protocol for vehicle-to-infrastructure (V2I) parking transactions. The vehicle on-board unit negotiates a pseudonymous session token; the edge/fog node enforces session invariants (no duplicate billing, no post-payment penalty, no active session after verified exit); and the cloud handles registration, payment settlement, and audit. A trust-aware ALPR reliability index routes low-confidence or adversarially suspect readings to dispute review instead of direct penalty, treating AI uncertainty as an infrastructure-control problem rather than a model-only problem.

The protocol is modelled as timed automata in UPPAAL and validated with SUMO and OMNeT++/Veins co-simulation. Formal verification confirms all five safety and liveness properties. The simulation (200 vehicles, 50 bays, injected faults) records correct handling of 83 tokenised entries, 9 low-confidence ALPR cases, 2 duplicate payments, 3 fog-cloud outages, and 2 exit mismatches without breaching any invariant.

My Contribution

Idea refinement and formal modelling -- UPPAAL timed-automata specification of the session state machine and verification of safety and liveness properties.

Key Results

• All UPPAAL safety properties verified: no duplicate billing, no post-payment penalty, no active session after verified exit, bounded receipt generation, deadlock-freedom.
• 9 low-confidence ALPR events correctly routed to EntryDisputeReview; 0 incorrect penalties.
• 2 duplicate payment messages intercepted without incrementing the payment counter.
• 3 fog-cloud outages handled with SyncPending to CloudSynchronized recovery.
• Average trip duration increased 6.8% over baseline (protocol overhead); facility remained functional.

Abstract

Connected and software-defined vehicles are increasingly interacting with edge infrastructure to access, pay for, and verify identities for operation safety. Parking entry and exit points remain weak boundaries of V2I transactions: camera recognition failures, duplicate payment events, cloud outages, or linked plate-payment records can cause financial disputes and privacy exposure. This paper presents a cyber-resilient, privacy-preserving session protocol where the vehicle OBU negotiates a pseudonymous session token, the edge node enforces verified state invariants, and the cloud handles registration, payment confirmation, and audit. Formally modelled as timed automata in UPPAAL and validated with SUMO and OMNeT++/Veins co-simulation. Verification confirms no duplicate billing, no post-payment penalty, synchronisation consistency, deadlock-freedom, and bounded receipt generation. Simulation confirms correct handling of 83 tokenised entries, 9 low-confidence ALPR cases, 2 duplicate payments, 3 outage events, and 2 exit mismatches without breaching any safety property.

Keywords

connected vehicles, software-defined vehicles, vehicular edge computing, smart parking, trustworthy AI, privacy-preserving session management, formal verification, V2I communication, UPPAAL, SUMO, OMNeT++/Veins, ALPR reliability