关键词: 认证与密钥交换协议, 形式化分析, 快速登录, ROR模型, Proverif

Abstract: In the Internet of vehicles system, vehicles need to achieve communications of vehicle to vehicle(V2V), which needs strong security, low latency, user anonymity and other security characteristics. Authentication and key exchange protocol(AKE) is based on cryptographic algorithms, aiming to complete session key negotiation for subsequent information exchange between communication parties. It is an important means to ensure the security of vehicle networking. However, the existing protocol registration phase requires offline secure channels, which is inconsistent with reality. Also the authentication phase is mostly based on third parties and requires multiple rounds of information exchange, increasing the complexity of the protocol interactions. In this paper, a lightweight V2V protocol is designed for public channels, which does not rely on the third party and only requires two rounds of information exchange during login and authentication phases. At the same time, a fast login phase is added to solve the delay of information exchange caused by sudden network interruptions. Theoretical analysis and formal verification results show that the designed protocol satisfied security properties such as authentication and confidentiality.

Key words: authentication and key exchange protocol, formal analysis, fast login, ROR(real or random) model, Proverif