## 7 Heuristic Security Analysis
### Formal Security Analysis Using ProVerif  
ProVerif [27] is an automated tool used to analyze and verify the security of cryptographic protocols. It can check properties such as confidentiality, authentication, and resistance to various attacks by formalizing protocols and using logical reasoning. It supports a wide range of protocols, including those based on symmetric and asymmetric encryption. In this section, we utilize ProVerif to evaluate the security of our proposed scheme. The initial part of the analysis involves the declaration of elements related to our scheme. This includes channels for message transmission, constants, variables, functions, and events, as depicted in Figure 5. Here, we define a public communication channel, ch1,for vehicle-RSU node interactions. Additionally, we establish constants, variables, a hash function \(h(\cdot)\), various connection functions, and XOR and ECC operations. The attacker model and associated events are illustrated primarily in Figure 6.  
In the next part of the analysis, the focus shifts to the role of vehicles in the authentication process, shown in Figure 7. This process involves vehicles accessing SC-stored data, transmitting an authentication message to the RSU, and formulating a session key based on the information provided by the RSU. The RSU's role is detailed in Figure 8, which includes decrypting messages using its private key, verifying vehicle identities using the TA's public key, generating temporary identities and session keys, and securely transmitting these to the vehicle. free chn1:channel. type Vehicle. type RSU. type TA. type nonce. type timestamp. (*-The basic variables.-*)  
free IDi:bitstring [private]. (*-The identify of Vehicle.-*)  
free PWi:bitstring [private]. (*-The password of Vehicle.-*)  
free y:bitstring [private]. (*-The secret key of TA.-*)  
free Y:bitstring. (*-The public key of TA.-*)  
free sj:bitstring [private]. (*-The secret key of RSUj.-*)  
free SKv:bitstring [private]. (*-The session key of Vehicle.-*)  
free SKrsu:bitstring [private]. (*-The session key of RSUj.-*)  
free IDj:bitstring. (*- The identify of RSU.-*)  
free P:bitstring. (*- The base point -*)  
free Pj:bitstring. (*-The public key of RSUj.-*)  
free k:bitstring [private]. (*- The share secret of RSUj and TA-*)  
free vehicle:Vehicle. free rsu:RSU. fun Hash(bitstring):bitstring. fun bit.timestamp(timestamp):bitstring. fun bit.nonce(nonce):bitstring. fun XOR(bitstring,bitstring):bitstring. equation forall x1:bitstring,y1:bitstring;  
XOR(XOR(x1,y1),y1)=x1. fun Con(bitstring,bitstring):bitstring. reduce forall x2:bitstring,y2:bitstring;  
Split(Con(x2,y2))=(x2,y2). fun Enc(bitstring,bitstring):bitstring. fun Dec(bitstring,bitstring):bitstring. fun EncMul(bitstring,bitstring):bitstring. fun EccSub(bitstring,bitstring):bitstring. fun Add(bitstring,bitstring):bitstring. fun Mul(bitstring,bitstring):bitstring. fun checktimesampfresh(bitstring,bool):bool  
reduc forall T:bitstring;  
checktimesampfresh(T,true)=true  
otherwise forall T:bitstring;  
checktimesampfresh(T,false)=false. Figure 5: Definition and function declaration. (*-events-*) event VLoginPhase(Vehicle). event VAuthenticationPhase(Vehicle). event VehicleSessionKey(Vehicle). event RSUAuthentication(RSU). event RSUSessionKey(RSU). (*-queries-*) query attacker(SKrsu). query attacker(SKv). query attacker(y). query attacker(PWi). query inj-event(VAuthenticationPhase(vehicle))== inj-event(VLoginPhase(vehicle)). query inj-event(RSUAuthentication(rsu))== inj-event(VAuthenticationPhase(vehicle)). query inj-event(VehicleSessionKey(vehicle))== inj-event(RSUAuthentication(rsu)). query inj-event(RSUsessionKey(rsu))== inj-event(VehicleSessionKey(vehicle)). Figure 6. Events and queries. Figure 7. Vehicle authentication process. Figure 9 presents the results obtained from ProVerif's analysis of our scheme. The findings confirm that adversaries are unable to obtain the critical parameters necessary for session key computation, thereby establishing the security robustness of our proposed scheme.