一种车联网V2V认证与密钥交换协议设计与验证  

Design and Verification of V2V Authentication and Key Exchange Protocol for Internet of Vehicles

作　　者：王秀珍 徐鹏 陈美荣[1,2] 王丹琛 徐扬[1,4] Wang Xiuzhen;Xu Peng;Chen Meirong;Wang Danchen;and Xu Yang(National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 611756;Chengdu Textile College,Chengdu 611731;Sichuan Digital Economy Research Center,Chengdu 610021;School of Mathematics,Southwest Jiaotong University,Chengdu 611756)

机构地区：[1]系统可信性自动验证国家地方联合工程实验室,成都611756 [2]成都纺织高等专科学校,成都611731 [3]四川省数字经济研究中心,成都610021 [4]西南交通大学数学学院,成都611756

出　　处：《信息安全研究》2025年第5期465-472,共8页Journal of Information Security Research

基　　金：中央高校基本科研业务费专项资金项目(2682021GF012)。

摘　　要：车联网系统中,车辆行驶过程需与其他车辆通信以实现信息交换,要求必须具备高安全、低延迟、用户匿名性等安全特性.认证与密钥交换协议以密码算法为基础旨在完成会话密钥协商,用于通信双方后续信息交换,是保证车联网通信安全的重要手段.现有协议注册阶段需在线下安全信道中进行,与实际不符,且认证阶段多基于第三方并需多轮信息交互,增加了过程复杂度.因此设计了一种基于公共信道的V2V(vehicle to vehicle)协议,协议交互过程不需依赖第三方,仅需进行2轮信息交换,同时添加快速登录阶段以解决网络突然中断造成的信息交换延迟问题,理论分析与形式化验证结果表明协议满足认证性与保密性等安全性质.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.

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

分 类 号：TP309.02[自动化与计算机技术—计算机系统结构]