{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:53:16Z","timestamp":1725857596136},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319339504"},{"type":"electronic","value":"9783319339511"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33951-1_4","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"53-68","source":"Crossref","is-referenced-by-count":6,"title":["A Formal Security Analysis of ERTMS Train to Trackside Protocols"],"prefix":"10.1007","author":[{"given":"Joeri","family":"de Ruiter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard J.","family":"Thomas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Chothia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Symposium on Principles of Programming Languages (POPL) (2001)","DOI":"10.1145\/360204.360213"},{"key":"4_CR2","unstructured":"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"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013121 (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82\u201396. IEEE (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"4_CR5","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial (2013)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-642-33675-1_22","volume-title":"Computer Safety, Reliability, and Security","author":"R Bloomfield","year":"2012","unstructured":"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\u2013258. Springer, Heidelberg (2012)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-662-46666-7_15","volume-title":"Principles of Security and Trust","author":"V Cheval","year":"2015","unstructured":"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\u2013299. Springer, Heidelberg (2015)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-662-47854-7_11","volume-title":"Financial Cryptography and Data Security","author":"T Chothia","year":"2015","unstructured":"Chothia, T., Garcia, F.D., de Ruiter, J., van den Breekel, J., Thompson, M.: Relay cost bounding for contactless EMV payments. In: B\u00f6hme, R., Okamoto, T. (eds.) FC 2015. LNCS, vol. 8975, pp. 189\u2013206. Springer, Heidelberg (2015)"},{"key":"4_CR9","unstructured":"ERA: SUBSET-026: System requirements specification, version 3.5.0. Technical report (2015)"},{"key":"4_CR10","unstructured":"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)"},{"issue":"1","key":"4_CR11","first-page":"207","volume":"11","author":"M Franekova","year":"2011","unstructured":"Franekova, M., Rastocny, K., Janota, A., Chrtiansky, P.: Safety analysis of cryptography mechanisms used in GSM for railway. Int. J. Eng. 11(1), 207\u2013212 (2011). http:\/\/annals.fih.upt.ro\/pdf-full\/2011\/ANNALS-2011-1-34.pdf","journal-title":"Int. J. Eng."},{"key":"4_CR12","unstructured":"GSM-R Functional Group: EIRENE Functional Requirements Specification, version 7.4.0. Technical report (2014)"},{"key":"4_CR13","unstructured":"GSM-R Functional Group: EIRENE System Requirements Specification, version 15.4.0. Technical report (2014)"},{"issue":"10","key":"4_CR14","first-page":"6034","volume":"11","author":"L Hongjie","year":"2013","unstructured":"Hongjie, L., Lijie, C., Bin, N.: Petrinet based analysis of the safety communication protocol. TELKOMNIKA Indonesian J. Electr. Eng. 11(10), 6034\u20136041 (2013)","journal-title":"TELKOMNIKA Indonesian J. Electr. Eng."},{"key":"4_CR15","unstructured":"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)"},{"key":"4_CR16","unstructured":"RSSB: GSM-R User Procedures, issue 7.1. Technical report (2015)"},{"key":"4_CR17","unstructured":"UNISIG: SUBSET-037 - EuroRadio FIS, version 3.2.0. Technical report (2015)"},{"issue":"11","key":"4_CR18","doi-asserted-by":"crossref","first-page":"3078","DOI":"10.1007\/s11431-011-4562-2","volume":"54","author":"Y Zhang","year":"2011","unstructured":"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\u20133090 (2011)","journal-title":"Sci. China Technol. Sci."}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:20:14Z","timestamp":1498321214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}