Formal Security Analysis of the MaCAN Protocol.

Research output: Research - peer-reviewArticle in proceedings – Annual report year: 2014

View graph of relations

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.
Original languageEnglish
Title of host publicationProceedings of the 11th International Conference on Integrated Formal Methods, IFM 2014
EditorsElvira Albert, Emil Sekerinski
PublisherSpringer
Publication date2014
Pages241-255
ISBN (Print)978-3-319-10180-4
ISBN (Electronic)978-3-319-10181-1
DOIs
StatePublished - 2014
Event11th International Conference on Integrated Formal Methods, IFM 2014 - Bertinoro, Italy
Duration: 9 Sep 201411 Sep 2014
Conference number: 11
http://ifm2014.cs.unibo.it/

Conference

Conference11th International Conference on Integrated Formal Methods, IFM 2014
Number11
CountryItaly
CityBertinoro
Period09/09/201411/09/2014
Internet address
SeriesLecture Notes in Computer Science
Volume8739
ISSN0302-9743
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • protocol verification, embedded systems, Controller Area Network
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 101180521