CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Short Paper: Formal Verification of an Authorization Protocol for Remote Vehicle Diagnostics

Pierre Kleberger (Institutionen för data- och informationsteknik, Nätverk och system (Chalmers) ) ; Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
IEEE Vehicular Networking Conference (VNC), Proceedings. Boston, 16-18 Dec. 2013 (2157-9865). p. 202-205. (2013)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: remote diagnostics; formal verification; authorization protocol; connected car.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-02-18. Senast ändrad 2014-04-17.
CPL Pubid: 193882

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)