Muchas de las aproximaciones de intercambio de clave de sesión basadas en CAN se basan en el esquema de clave de grupo, lo que puede llevar fácilmente a adversarios avanzados a infiltrar todos los ECUs (unidades de control electrónico) en la red si la clave de intercambio se filtra. Para abordar el problema anterior, proponemos un protocolo de distribución de clave de sesión probadamente seguro basado en el protocolo NSSK (clave compartida de Needham-Schroeder) mejorado para la red CAN de vehículos. Aplicamos los mecanismos de autenticación de mensajes y firma digital para corregir los defectos del NSSK original con respecto a su falta de resistencia al ataque de Denning-Sacco. Luego, analizamos la seguridad probada del protocolo propuesto en el modelo de oráculo aleatorio y verificamos los objetivos de seguridad del protocolo utilizando las herramientas de simulación AVISPA y Tamarin Prover; los resultados reflejan que el protocolo cumplió con los requisitos de seguridad para la distribución de claves, como la secrecía de la clave de sesión, el acuerdo inyectivo y la secrecía de la clave conocida. Finalmente, comparamos nuestro nuevo protocolo con otros protocolos de distribución de clave en la comunicación de bus CAN para evaluar el rendimiento del nuevo protocolo en escenarios reales. El resultado muestra que el protocolo es seguro contra muchos ataques basados en carga útil y es práctico para las redes CAN de vehículos.