CARBUROS: A Formally Verified Authentication Protocol for V2X Communications

The growing adoption of Vehicle-to-Everything (V2X) communications in Intelligent Transportation Systems (ITS) demands robust authentication protocols to ensure secure and reliable interaction among road actors. In this context, Multi-Factor Authentication (MFA) can serve as an important building block; however, integrating MFA into vehicular environments remains nontrivial. Traditional MFA verifies digital credentials but typically does not confirm physical presence. In ITS, authentication often requires binding digital identities to a vehicle's actual position and timing. To address this gap, this work presents CARBUROS, an MFA protocol specifically designed for ITS scenarios. It introduces a dual-channel mechanism that combines a standard digital communication channel with a physical proximity-based channel, ensuring that authentication reflects real-world co-location in space and time. This approach strengthens security by linking digital credentials to physical context. CARBUROS was formally modeled and verified using ProVerif, an automatic cryptographic protocol verifier. The analysis shows that the protocol withstands threats such as unauthorized access, identity spoofing, and functional disruption. The results confirm that CARBUROS preserves authentication and confidentiality under the modeled adversarial conditions while maintaining lightweight communication and computational overhead suitable for deployment in ITS environments.