Abstract
This paper presents a formal analysis of the train to trackside communication protocols used in the European Railway Traffic Management System (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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
A collection of such studies can be found at http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif-users.html.
- 3.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Symposium on Principles of Programming Languages (POPL) (2001)
Ansaldo STS Group. Product portfolio and ERTMS/RTCS projects of Ansaldo Segnalamento Ferroviario (2008). http://old.fel.zcu.cz/Data/documents/sem_de_2008/AnsaldoSTS_08.pdf
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pp. 107–121 (2010)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82–96. IEEE (2001)
Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial (2013)
Bloomfield, R., Bloomfield, R., Gashi, I., Stroud, R.: How secure Is ERTMS? In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP Workshops 2012. LNCS, vol. 7613, pp. 247–258. Springer, Heidelberg (2012)
Cheval, V., Cortier, V.: Timing attacks in security protocols: symbolic framework and proof techniques. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 280–299. Springer, Heidelberg (2015)
Chothia, T., Garcia, F.D., de Ruiter, J., van den Breekel, J., Thompson, M.: Relay cost bounding for contactless EMV payments. In: Böhme, R., Okamoto, T. (eds.) FC 2015. LNCS, vol. 8975, pp. 189–206. Springer, Heidelberg (2015)
ERA: SUBSET-026: System requirements specification, version 3.5.0. Technical report (2015)
Esposito, R., Lazzaro, A., Marmo, P., Sanseviero, A.: Formal verification of ERTMS EuroRadio safety critical protocol. In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003) (2003)
Franekova, M., Rastocny, K., Janota, A., Chrtiansky, P.: Safety analysis of cryptography mechanisms used in GSM for railway. Int. J. Eng. 11(1), 207–212 (2011). http://annals.fih.upt.ro/pdf-full/2011/ANNALS-2011-1-34.pdf
GSM-R Functional Group: EIRENE Functional Requirements Specification, version 7.4.0. Technical report (2014)
GSM-R Functional Group: EIRENE System Requirements Specification, version 15.4.0. Technical report (2014)
Hongjie, L., Lijie, C., Bin, N.: Petrinet based analysis of the safety communication protocol. TELKOMNIKA Indonesian J. Electr. Eng. 11(10), 6034–6041 (2013)
Li, L., Sun, J., Liu, Y., Sun, M., Dong, J.S.: A formal specification and verification framework for timed security protocols. TSE (2015, in submission)
RSSB: GSM-R User Procedures, issue 7.1. Technical report (2015)
UNISIG: SUBSET-037 - EuroRadio FIS, version 3.2.0. Technical report (2015)
Zhang, Y., Tang, T., Li, K., Mera, J.M., Zhu, L., Zhao, L., Xu, T.: Formal verification of safety protocol in train control system. Sci. China Technol. Sci. 54(11), 3078–3090 (2011)
Acknowledgements
We would like to thank Maria Vigliotti and Florent Pepin from the UK’s Rail Safety and Standards Board (RSSB) for helpful discussion regarding the security of ERTMS. Funding for this paper was provided by the UK’s Centre for the Protection of National Infrastructure (CPNI) and Engineering and Physical Sciences Research Council (EPSRC) via the SCEPTICS: A SystematiC Evaluation Process for Threats to Industrial Control Systems project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
de Ruiter, J., Thomas, R.J., Chothia, T. (2016). A Formal Security Analysis of ERTMS Train to Trackside Protocols. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2016. Lecture Notes in Computer Science(), vol 9707. Springer, Cham. https://doi.org/10.1007/978-3-319-33951-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-33951-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33950-4
Online ISBN: 978-3-319-33951-1
eBook Packages: Computer ScienceComputer Science (R0)