A Formal Security Analysis of ERTMS Train to Trackside Protocols
Joeri de Ruiter, Richard J. Thomas and Tom Chothia
Submitted to International Conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification and Certification (RSSRail 2016)
This paper presents a formal analysis of the train to trackside communication protocols used in the European Rail Traffic Managment (ERTMS) standard, and in particular the EuroRadio protocol. This protocol is used to secure important commands sent between train and trackside, such as movement authority and emergency stop messages. We perform our analysis using the applied pi-calculus and the ProVerif tool. This provides a powerful and expressive framework for protocol analysis and allows us to check a wide range of security properties based on checking correspondence assertions. We show how it is possible to model the protocol’s counter-style timestamps in this framework. We define ProVerif assertions that allow us to check for secrecy of long and short term keys, authenticity of entities, message insertion, deletion, replay and reordering. We find that the protocol provides most of these security features, however it allows undetectable message deletion and the forging of emergency messages. We discuss the relevance of these results and make recommendations to further enhance the security of ERTMS.
The models used in this paper are linked below with their appropriate outputs:
- High Priority Messages: GSM-R_no_timestamps.pi
- Output: GSM-R_no_timestamps.pi.output
- Timestamps: GSM-R_timestamps.pi
- Output: GSM-R_timestamps.pi.output
This paper was presented on Tuesday, 28th June 2016 at Maison de la RATP, Paris.
- Slides: slides.pdf
The paper is available here: rssrail_paper.pdf