| 1. |
- Kleberger, Pierre, 1978, et al.
(författare)
-
Formal Verification of an Authorization Protocol for Remote Vehicle Diagnostics
- 2013
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Remote diagnostics protocols have generally only considered correct authentication to be enough to grant access to vehicles. However, as diagnostics equipment or their keys can be stolen or copied, these devices can not be trusted. Thus, authentication alone is not enough to prevent unauthorized access to vehicles. In previous work, we proposed an authorization protocol to prevent unauthorized access to vehicles.In the automotive industrywhere lives are at risk and a certain liability is exacted on the manufacturer, their vehicles and its software, it is critical that such a protocol has no flaws. Thus, using formal methods to prove the correctness of protocol designs is an important step.In this paper, we formally prove that the proposed authorization protocol provides mutual authentication between the diagnostics equipment and the vehicle, and that it guarantees both secrecy of the distributed session key and freshness of the distributed authorization information. Our formal analysis is conducted using both the Burrows-Abadi-Needham (BAN) Logic and the ProVerif automated verification tool.To the authors' best knowledge, this is the first formally verified authorization protocol for remote vehicular diagnostics.
|
|
| 2. |
- Kleberger, Pierre, 1978, et al.
(författare)
-
Protecting Vehicles Against Unauthorised Diagnostics Sessions Using Trusted Third Parties
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642407925 ; Lecture Notes in Computer Science:8153, s. 70-81
-
Konferensbidrag (refereegranskat)abstract
- Wireless vehicle diagnostics is expected to provide great improvements to the maintenance of future cars. By using certificates, vehicles can identify diagnostics equipment for a diagnostics session, even over long distances. However, since the diagnostics equipment contains authentication keys used to authenticate such sessions, it is critical that neither the keys nor the equipment is lost. Such a loss can give unauthorised access to any vehicle accepting these keys until the theft is detected and the certificates are revoked. In this paper, we propose a method to protect vehicles against unauthorised diagnostics sessions. A trusted third party is introduced to authorise sessions, thus we do not rely solely on proper identification and authentication of diagnostics equipment. Our approach enables vehicles to verify the validity of diagnostics requests. It is transparent to the diagnostics protocol being used, supports different levels of trust, and can control what commands are permitted during diagnostics sessions.
|
|
| 3. |
- Kleberger, Pierre, 1978, et al.
(författare)
-
Short Paper: Formal Verification of an Authorization Protocol for Remote Vehicle Diagnostics
- 2013
-
Ingår i: IEEE Vehicular Networking Conference, VNC. - 2157-9865 .- 2157-9857. - 9781479926879 ; , s. 202-205
-
Konferensbidrag (refereegranskat)abstract
- Remote diagnostics protocols have generally only considered correct authentication to be enough to grant access to vehicles. However, as diagnostics equipment or their keys can be stolen or copied, these devices can not be trusted. Thus, authentication alone is not enough to prevent unauthorized access to vehicles. In previous work, we proposed an authorization protocol to prevent unauthorized access to vehicles. In this paper, we formally prove that the proposed authorization protocol provides mutual authentication between the diagnostics equipment and the vehicle, and that it guarantees both secrecy of the distributed session key and freshness of the distributed authorization information. Our formal analysis is conducted using both the Burrows-Abadi-Needham (BAN) Logic and the PROVERIF automated verification tool.
|
|
