Title:	Secure Communication Mechanisms for Trustworthy Vehicular Coordination
DNr:	LiU-compute-2021-20
Project Type:	LiU Compute
Principal Investigator:	Mikael Asplund <mikael.asplund@liu.se>
Affiliation:	Linköpings universitet
Duration:	2021-04-26 – 2024-05-01
Classification:	10201
Homepage:	http://www.ida.liu.se/~mikas34/cugs
Keywords:

Abstract

The purpose of this project is to investigate secure communication mechanisms that allow trust to be established between vehicles. Examples of such mechanism are the verification of the physical location of nearby vehicles and also the sharing of that information within the group to enable trust propagation. Key challenges that will be considered include limited and congestion-prone communication channels, lack of ubiquitous communication infrastructure, and the possibility of reputation attacks from malicious entities. An important part of the current phase of the project is formal verification of cryptographic protocols using the Tamarin prover. Verification of such properties means trying to find counterexamples to first-order logic statements about possible runs of a given protocol. If the prover can estalish that no such counterexample exists, then the property has been proven to hold. However, since there are many possible runs of a distributed protocol, the prover must go through all of them for the proof to hold. This requires substantial computational resources.