Abstract
Embedded real-time network protocols such as the CAN bus cannot rely on off-the-shelf schemes for authentication, because of the bandwidth limitations imposed by the network. As a result, both academia and industry have proposed custom protocols that meet such constraints, with solutions that may be deemed insecure if considered out of context. MaCAN is one such compatible authentication protocol, proposed by Volkswagen Research and a strong candidate for being adopted by the automotive industry.
In this work we formally analyse MaCAN with ProVerif, an automated protocol verifier. Our formal analysis identifies two flaws in the original protocol: one creates unavailability concerns during key establishment, and the other allows re-using authenticated signals for different purposes. We propose and analyse a modification that improves its behaviour while fitting the constraints of CAN bus. Although the revised scheme improves the situation, it is still not completely secure. We argue that the modified protocol makes a good compromise between the desire to secure automotive systems and the limitations of CAN networks.
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
Preview
Unable to display preview. Download preview PDF.
References
Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: Verification of Stateful Processes. In: 2011 IEEE 24th Computer Security Foundations, pp. 33–47 (2011)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE workshop on Computer Security Foundations, pp. 82–96. IEEE Computer Society (2001)
Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)
Blanchet, B., Smyth, B.: Proverif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial (2013)
Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S., Koscher, K., Czeskis, A., Roesner, F., Kohno, T.: Comprehensive experimental analyses of automotive attack surfaces. In: Proceedings of the 20th USENIX Conference on Security (2011)
Davis, R.I., Burns, A., Bril, R.J., Lukkien, J.J.: Controller area network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Systems 35(3), 239–272 (2007)
Dworkin, M.J.: SP 800-38B. recommendation for block cipher modes of operation: the CMAC mode for authentication (2005)
FlexRay Consortium, et al.: FlexRay communications system-protocol specification. Version, 2(1):198–207 (2005)
Robert Bosch GmbH. Road vehicles – Controller area network (CAN) – Part 1: Data link layer and physical signalling (1991)
Groza, B., Murvay, S., Van Herrewege, A., Verbauwhede, I.: LiBrA-CAN: a Lightweight Broadcast Authentication protocol for Controller Area Networks (2012)
Hartkopp, O., Reuber, C., Schilling, R.: MaCAN - message authenticated CAN. In: Proceedings of the 10th Escar Conference on Embedded Security in Cars (2012)
Koscher, K., Czeskis, A., Roesner, F., Patel, S., Kohno, T., Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S.: Experimental Security Analysis of a Modern Automobile. In: 2010 IEEE Symposium on Security and Privacy, pp. 447–462 (2010)
Hartwich, F.: CAN with Flexible Data-Rate (2005)
Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th Computer Security Foundations Workshop, pp. 31–43. IEEE (1997)
Mödersheim, S.A.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 351–360. ACM (2010)
Schweppe, H., Roudier, Y., Weyl, B., Apvrille, L., Scheuermann, D.: Car2x communication: securing the last meter-a cost-effective approach for ensuring trust in car2x applications using in-vehicle symmetric cryptography. In: Vehicular Technology Conference (VTC Fall), pp. 1–5. IEEE (2011)
Van Herrewege, A., Singelee, D., Verbauwhede, I.: CANAuth — a simple, backward compatible broadcast authentication protocol for CAN bus. In: ECRYPT Workshop on Lightweight Cryptography 2011 (2011)
Ziermann, T., Wildermann, S., Teich, J.: CAN+: A new backward-compatible Controller Area Network (CAN) protocol with up to 16× higher data rates. In: Design, Automation & Test in Europe Conference & Exhibition, pp. 1088–1093. IEEE (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bruni, A., Sojka, M., Nielson, F., Riis Nielson, H. (2014). Formal Security Analysis of the MaCAN Protocol. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)