Umarell – A New Attacker in ITS Communications

As V2X communication becomes increasingly central to Intelligent Transportation Systems (ITS), the need for robust security solutions becomes more critical. Formal verification against a reference attacker model provides one of the strongest security guarantees, for example in the case of communication protocols. Unfortunately, model checkers lack the right primitives for modeling non-Dolev-Yao attackers and non-standard communication channels. In this work, we introduce a new attacker model based on physical proximity, called Umarell, to extend the standard Dolev-Yao adversary. We provide a formalization in ProVerif and show how to model physical channels. Finally, we demonstrate our methodology through an application to a multi-factor/two-channel authentication protocol that combines Non-Line-of-Sight (NLOS) communication for secure data exchange and Line-of-Sight (LOS) communication to verify physical proximity.