{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T16:17:42Z","timestamp":1790266662754,"version":"4.1.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T00:00:00Z","timestamp":1722470400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T00:00:00Z","timestamp":1722816000000},"content-version":"vor","delay-in-days":4,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007514","name":"Universit\u00e0 di Pisa","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007514","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The widespread use of advanced driver assistance systems in modern vehicles, together with their integration with the Internet and other road nodes, has made vehicle more vulnerable to cyber-attacks. To address these risks, the automotive industry is increasingly focusing on the development of security solutions: formal methods and software verification techniques, which have been successfully applied to a number of safety-critical systems, could be a promising approach in the automotive area. In this work, we concentrate on in-vehicle communications, provided by many Electronic Control Units (ECUs) that work together thanks to serial protocols such as Controller Area Network (CAN). However, increasing connectivity exposes the internal network to a variety of cyber-risks. Our aim is to formally verify the AUTOSAR-based Basic Software module called CINNAMON, designed to ensure confidentiality, integrity, and authentication at the same time for traffic exchanged over CAN protocol. More precisely, it adds confidentiality guarantees to the Secure Onboard Communication (SecOC) module. We formally analyze CINNAMON with the verification tool <jats:sc>Tamarin<\/jats:sc>. Our analysis shows that CINNAMON could be an effective security solution, as it can ensure the desired properties, in particular, confidentiality in a send-receive scenario between two ECUs. Finally, we describe a potential application scenario.<\/jats:p>","DOI":"10.1007\/s10009-024-00759-w","type":"journal-article","created":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T08:02:22Z","timestamp":1722844942000},"page":"495-508","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Formal analysis of an AUTOSAR-based basic software module"],"prefix":"10.1007","volume":"26","author":[{"given":"Chiara","family":"Bodei","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"De\u00a0Vincenzi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilaria","family":"Matteucci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,8,5]]},"reference":[{"key":"759_CR1","unstructured":"Automated vehicles for safety. https:\/\/www.nhtsa.gov\/technology-innovation\/automated-vehicles-safety. Last accessed on May 29, 2024"},{"key":"759_CR2","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1109\/EDCC51268.2020.00026","volume-title":"2020 16th European Dependable Computing Conference (EDCC)","author":"G. Bella","year":"2020","unstructured":"Bella, G., Biondi, P., Costantino, G., Matteucci, I.: Cinnamon: a module for AUTOSAR secure onboard communication. In: 2020 16th European Dependable Computing Conference (EDCC), pp.\u00a0103\u2013110 (2020). https:\/\/doi.org\/10.1109\/EDCC51268.2020.00026"},{"key":"759_CR3","unstructured":"Bella, G., Biondi, P., Costantino, G., Matteucci, I.: TOUCAN: a proTocol tO secUre Controller Area Network. CoRR (2021). https:\/\/arxiv.org\/abs\/2111.10642"},{"key":"759_CR4","doi-asserted-by":"publisher","unstructured":"Bella, G., Biondi, P., Costantino, G., Matteucci, I.: Designing and implementing an AUTOSAR-based Basic Software Module for enhanced security. Comput. Netw. 109377, (2022). https:\/\/doi.org\/10.1016\/j.comnet.2022.109377","DOI":"10.1016\/j.comnet.2022.109377"},{"key":"759_CR5","doi-asserted-by":"publisher","unstructured":"Birkinshaw, C., Rouka, E., Vassilakis, V.G.: Implementing an intrusion detection and prevention system using software-defined networking: Defending against port-scanning and denial-of-service attacks. J. Netw. Comput. Appl., 71\u201385 (2019). https:\/\/doi.org\/10.1016\/j.jnca.2019.03.005","DOI":"10.1016\/j.jnca.2019.03.005"},{"key":"759_CR6","doi-asserted-by":"publisher","first-page":"14","DOI":"10.4204\/eptcs.373.2","volume":"373","author":"B. Blanchet","year":"2022","unstructured":"Blanchet, B.: The security protocol verifier proverif and its horn clause resolution algorithm. Electr. Proc. Theor. Comput. Sci. 373, 14\u201322 (2022). https:\/\/doi.org\/10.4204\/eptcs.373.2","journal-title":"Electr. Proc. Theor. Comput. Sci."},{"key":"759_CR7","doi-asserted-by":"publisher","first-page":"626","DOI":"10.5220\/0011779500003405","volume-title":"Proceedings of the 9th International Conference on Information Systems Security and Privacy, ICISSP 2023","author":"C. Bodei","year":"2023","unstructured":"Bodei, C., Costantino, G., Vincenzi, M.D., Matteucci, I., Monreale, A.: Vehicle data collection: a privacy policy analysis and comparison. In: Mori, P., Lenzini, G., Furnell, S. (eds.) Proceedings of the 9th International Conference on Information Systems Security and Privacy, ICISSP 2023, Lisbon, Portugal, February 22-24, 2023, pp.\u00a0626\u2013633. SciTePress, (2023). https:\/\/doi.org\/10.5220\/0011779500003405"},{"key":"759_CR8","series-title":"Intelligent Systems Reference Library","doi-asserted-by":"publisher","DOI":"10.18420\/sicherheit2020_06","volume-title":"Challenges of Software Verification","author":"C. Bodei","year":"2023","unstructured":"Bodei, C., Ferrari, G.L., Galletta, L., Degano, P.: Risk estimation in IoT systems. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification. Intelligent Systems Reference Library, vol.\u00a0238. Springer, Berlin (2023). https:\/\/doi.org\/10.18420\/sicherheit2020_06"},{"key":"759_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-10181-1_15","volume-title":"Integrated Formal Methods \u2013 IFM 2014","author":"A. Bruni","year":"2014","unstructured":"Bruni, A., Sojka, M., Nielson, F., Nielson, H.R.: Formal security analysis of the macan protocol. In: Albert, E., Sekerinski, E. (eds.) Integrated Formal Methods \u2013 IFM 2014, vol.\u00a08739, pp.\u00a0241\u2013255. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_15"},{"key":"759_CR10","unstructured":"Cancrypt. https:\/\/cancrypt.net\/index.php\/en\/. Last accessed on May 29, 2024"},{"key":"759_CR11","unstructured":"Carmakers strive to stay ahead of hackers. https:\/\/www.nytimes.com\/2021\/03\/18\/business\/hacking-cars-cybersecurity.html. Last accessed on May 29, 2024"},{"key":"759_CR12","volume-title":"Adventures in Automotive Networks and Control Units","author":"C.M. Chris Valasek","year":"2014","unstructured":"Chris Valasek, C.M.: Adventures in Automotive Networks and Control Units (2014). http:\/\/illmatics.com\/car_hacking.pdf"},{"key":"759_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/J.COSE.2023.103133","volume":"128","author":"G. Costa","year":"2023","unstructured":"Costa, G., Degano, P., Galletta, L., Soderi, S.: Formally verifying security protocols built on watermarking and jamming. Comput. Secur. 128, 103133 (2023). https:\/\/doi.org\/10.1016\/J.COSE.2023.103133","journal-title":"Comput. Secur."},{"issue":"1","key":"759_CR14","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1109\/TITS.2022.3217358","volume":"24","author":"G. Costantino","year":"2023","unstructured":"Costantino, G., Vincenzi, M.D., Martinelli, F., Matteucci, I.: A privacy-preserving solution for intelligent transportation systems: private driver DNA. IEEE Trans. Intell. Transp. Syst. 24(1), 258\u2013273 (2023). https:\/\/doi.org\/10.1109\/TITS.2022.3217358","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"2","key":"759_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"key":"759_CR16","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4020-6254-4_14","volume-title":"Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems","author":"T.E. Fuhrman","year":"2007","unstructured":"Fuhrman, T.E.: Role of formal methods in the automobile industry. In: Ramesh, S., Sampath, P. (eds.) Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, pp.\u00a0175\u2013175. Springer, Dordrecht (2007)"},{"key":"759_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10270-023-01124-2","volume":"22","author":"M. Gleirscher","year":"2023","unstructured":"Gleirscher, M., Pol, J., Woodcock, J.: A manifesto for applicable formal methods. Softw. Syst. Model. 22, 1\u201313 (2023). https:\/\/doi.org\/10.1007\/s10270-023-01124-2","journal-title":"Softw. Syst. Model."},{"key":"759_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107233","volume":"174","author":"K. Hofer-Schmitz","year":"2020","unstructured":"Hofer-Schmitz, K., Stojanovi\u0107, B.: Towards formal verification of iot protocols: a review. Comput. Netw. 174, 107233 (2020). https:\/\/doi.org\/10.1016\/j.comnet.2020.107233. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1389128619317116","journal-title":"Comput. Netw."},{"key":"759_CR19","unstructured":"International Organization for Standardization: Road vehicles \u2014 Controller area network (CAN) \u2013 Part 1: Data link layer and physical signalling (2015). https:\/\/www.iso.org\/standard\/63648.html"},{"key":"759_CR20","unstructured":"ISO: Road vehicles \u2014 cybersecurity engineering. Standard ISO\/SAE FDIS 21434:2021 Ed.1, International Organization for Standardization, Geneva, CH (2021). https:\/\/www.iso.org\/standard\/70918.html"},{"key":"759_CR21","doi-asserted-by":"publisher","unstructured":"Krook, J., Selvaraj, Y., Ahrendt, W., Fabian, M.: A formal-methods approach to provide evidence in automated-driving safety cases. CoRR (2022). https:\/\/doi.org\/10.48550\/arXiv.2210.07798","DOI":"10.48550\/arXiv.2210.07798"},{"key":"759_CR22","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/3600160.3600184","volume-title":"Proceedings of the 18th International Conference on Availability, Reliability and Security, ARES 2023","author":"T. Lauser","year":"2023","unstructured":"Lauser, T., Krau\u00df, C.: Formal security analysis of vehicle diagnostic protocols. In: Proceedings of the 18th International Conference on Availability, Reliability and Security, ARES 2023, Benevento, Italy, 29 August 2023\u20131 September 2023, pp.\u00a021:1\u201321:11. ACM, New York (2023). https:\/\/doi.org\/10.1145\/3600160.3600184"},{"key":"759_CR23","doi-asserted-by":"publisher","DOI":"10.1145\/3385958.3430482","volume-title":"Proceedings of the 4th ACM Computer Science in Cars Symposium, CSCS\u201920","author":"T. Lauser","year":"2020","unstructured":"Lauser, T., Zelle, D., Krau\u00df, C.: Security analysis of automotive protocols. In: Proceedings of the 4th ACM Computer Science in Cars Symposium, CSCS\u201920. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3385958.3430482"},{"key":"759_CR24","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1109\/ICSE.2015.85","volume-title":"2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering","author":"D. Matichuk","year":"2015","unstructured":"Matichuk, D., Murray, T., Andronick, J., Jeffery, R., Klein, G., Staples, M.: Empirical study towards a leading indicator for cost of formal software verification. In: 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering, vol.\u00a01, pp.\u00a0722\u2013732 (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.85"},{"key":"759_CR25","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S. Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp.\u00a0696\u2013701. Springer, Berlin (2013)"},{"key":"759_CR26","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-030-03427-6_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"M. Nyberg","year":"2018","unstructured":"Nyberg, M., Gurov, D., Lidstr\u00f6m, C., Rasmusson, A., Westman, J.: Formal verification in automotive industry: enablers and obstacles. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, pp.\u00a0139\u2013158. Springer, Cham (2018)"},{"key":"759_CR27","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-030-75078-7_28","volume-title":"Advanced Information Networking and Applications","author":"L.P. Oliveira","year":"2021","unstructured":"Oliveira, L.P., da Silva, A.W.N., de Azevedo, L.P., da Silva, M.V.L.: Formal methods to analyze energy efficiency and security for iot: a systematic review. In: Barolli, L., Woungang, I., Enokido, T. (eds.) Advanced Information Networking and Applications, pp.\u00a0270\u2013279. Springer, Cham (2021)"},{"key":"759_CR28","unstructured":"OWASP: Stride model (2023). https:\/\/owasp.org\/www-community\/Threat_Modeling_Process. Last accessed on May 29, 2024"},{"key":"759_CR29","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1109\/PDP55904.2022.00047","volume-title":"30th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, PDP 2022","author":"C. Plappert","year":"2022","unstructured":"Plappert, C., Fenzl, F., Rieke, R., Matteucci, I., Costantino, G., De Vincenzi, M.: SECPAT: security patterns for resilient automotive E \/ E architectures. In: Gonz\u00e1lez-Escribano, A., Garc\u00eda, J.D., Torquati, M., Skavhaug, A. (eds.) 30th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, PDP 2022, Valladolid, Spain, March 9\u201311, 2022, pp.\u00a0255\u2013264. IEEE, (2022). https:\/\/doi.org\/10.1109\/PDP55904.2022.00047"},{"key":"759_CR30","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-03427-6_20","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"R. Schlick","year":"2018","unstructured":"Schlick, R., Felderer, M., Majzik, I., Nardone, R., Raschke, A., Snook, C., Vittorini, V.: A proposal of an example and experiments repository to Foster industrial adoption of formal methods. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, pp.\u00a0249\u2013272. Springer, Cham (2018)"},{"key":"759_CR31","unstructured":"Specification of key manager. https:\/\/www.autosar.org\/fileadmin\/standards\/R22-11\/CP\/AUTOSAR_SWS_KeyManager.pdf. Last accessed on May 29, 2024"},{"key":"759_CR32","unstructured":"Tamarin github. https:\/\/tamarin-prover.github.io\/. Last accessed on May 29, 2024"},{"key":"759_CR33","unstructured":"Tamarin manual. https:\/\/tamarin-prover.github.io\/manual\/master\/tex\/tamarin-manual.pdf. Last accessed on August 31, 2023"},{"issue":"1","key":"759_CR34","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s40860-023-00202-y","volume":"10","author":"Z.H. Toman","year":"2024","unstructured":"Toman, Z.H., Hamel, L., Toman, S.H., Graiet, M., Valadares, D.C.G.: Formal verification for security and attacks in IoT physical layer. J. Reliab. Intel. Environ. 10(1), 73\u201391 (2024). https:\/\/doi.org\/10.1007\/s40860-023-00202-y","journal-title":"J. Reliab. Intel. Environ."},{"key":"759_CR35","unstructured":"UNECE: Uniform provisions concerning the approval of vehicles with regards to cyber security and cyber security management system. Regulation Addendum 154 \u2013 UN Regulation No. 155, United Nations Economic Commission for Europe, Geneva, CH (2021). https:\/\/unece.org\/sites\/default\/files\/2021-03\/R155e.pdf"},{"key":"759_CR36","unstructured":"When testing is not enough. Software complexity drives technology leaders to adopt formal methods. https:\/\/issuu.com\/rtcgroup\/docs\/cots-2007-july-web\/s\/10872490. Last accessed on May 29, 2024"},{"key":"759_CR37","doi-asserted-by":"publisher","unstructured":"Yoshizawa, T., Singel\u00e9e, D., Muehlberg, J.T., Delbruel, S., Taherkordi, A., Hughes, D., Preneel, B.: A survey of security and privacy issues in V2X communication systems. ACM Comput. Surv. 55(9) (2023). https:\/\/doi.org\/10.1145\/3558052","DOI":"10.1145\/3558052"},{"key":"759_CR38","series-title":"ARES","doi-asserted-by":"publisher","DOI":"10.1145\/3465481.3465748","volume-title":"Analyzing and Securing SOME\/IP Automotive Services with Formal and Practical Methods","author":"D. Zelle","year":"2021","unstructured":"Zelle, D., Lauser, T., Kern, D., Krau\u00df, C.: Analyzing and Securing SOME\/IP Automotive Services with Formal and Practical Methods. ARES, vol.\u00a021. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3465481.3465748"},{"key":"759_CR39","doi-asserted-by":"publisher","first-page":"79","DOI":"10.18420\/sicherheit2020_06","volume-title":"SICHERHEIT 2020","author":"T. Zimmermann","year":"2020","unstructured":"Zimmermann, T., Bauer, J., Aschenbruck, N.: CryptoCAN \u2013 ensuring confidentiality in controller area networks for agriculture. In: Reinhardt, D., Langweg, H., Witt, B.C., Fischer, M. (eds.) SICHERHEIT 2020, pp.\u00a079\u201390. Gesellschaft f\u00fcr Informatik e.V, Bonn (2020). https:\/\/doi.org\/10.18420\/sicherheit2020_06"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00759-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00759-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00759-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:04:50Z","timestamp":1725530690000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00759-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,8]]}},"alternative-id":["759"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00759-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8]]},"assertion":[{"value":"16 July 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}