- Vivi Padova
- Il Bo
SEMINARIO DI INFORMATICA
Venerdì 11 Settembre 2015 alle ore 13:30 in Aula 1BC50, Alessandro Bruni terrà un seminario dal titolo "Formal Security Analysis of the MaCAN Protocol"
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, and we discuss the limitations of the analysis tool in analysing this case study, showing an extension of the language that overcomes them.