## Security Analysis  
### Formal Security Proof  
In this section, we provide a formal proof of the semantic security of the proposed protocol, utilizing the random oracle model. **Definition 1**. : _(Participants): The participants consist of the Vehicle User (VU), RSU and TA. In the i_th instance, the participants are represented as \(IN_{VU}^{i}\), \(IN_{RSU}^{i}\), and \(IN_{TA}^{i}\)_  
**Definition 2**. : _(States): The status of oracle Accept indicates that it received the correct message._  
**Definition 3**. : _(Partnering): If the oracles \(IN_{VU}^{i}\), and \(IN_{RSU}^{i}\)are in the \"Accept\" state and the session keys have been successfully agreed upon, the oracles obtain their respective session identities and participant identities. The oracles can be considered partners if their session keys, session identities, and participant identities are all identical._  
In this model, the adversary \(\mathcal{A}\) has access to the following queries:  
* Queries: The queries simulate the capabilities of attackers, replicating their potential actions and abilities. * \(Execute\left(IN_{VU}^{i},IN_{RSU}^{i},IN_{TA}^{i}\right)\): The adversary \(\mathcal{A}\) has the capability to intercept all the messages exchanged over the wireless channel. * \(Send\left(IN_{VU}^{i},IN_{RSU}^{i},IN_{TA}^{i},m\right)\): \(\mathcal{A}\) has the ability to forge the message m and sends it to \(IN_{VU}^{i}\), \(IN_{RSU}^{i}\), or \(IN_{TA}^{i}\); if the message m is valid, \(IN_{VU}^{i}\), \(IN_{RSU}^{i}\), or \(IN_{TA}^{i}\) will provide a response \(\mathcal{A}\). * \(Reveal\left(IN_{VU}^{i},IN_{RSU}^{i},IN_{TA}^{i}\right)\): \(\mathcal{A}\) can obtain the agreed session keys between \(IN_{VU}^{i}\), \(IN_{RSU}^{i}\), and \(IN_{TA}^{i}\). * \(Test\left(IN_{VU}^{i},IN_{RSU}^{i},IN_{TA}^{i},r\right)\): This query can be executed at most once, generating a random bit \(r\), This query can be executed at most once, generating a random bit \(r\), which returns the real session key if \(r=1\); otherwise, a random number is returned. * \(Corrupt\left(IN_{VU}^{i}\right)\): It simulates a side channel attack on the SC and returns the stored values \(<G,p,P,\varepsilon_{v},C_{v},PPID_{v},h(.),PA_{v}>\). * \(CorruptRSU\left(IN_{RSU}^{i}\right)\): It simulates a side channel attack on the TPD of RSU and returns the stored information \(<C_{r},sk_{r},ID_{r},PD_{r},t_{r}>\). **Definition 4**. : _(Freshness): An instance can be deemed fresh if it fulfills the following conditions:_  
* \(IN_{VU}^{i}\)_,_ \(IN_{RSU}^{i}\)_, and_ \(IN_{TA}^{i}\) _are in Accept._
* _The query Reveal_ \(\left(IN_{VU}^{i},IN_{RSU}^{i},IN_{TA}^{i}\right)\) _has not been executed._* _The queries_ \(Corrupt\left(IN^{i}_{VUI}\right)\) _and_ \(CorruptRSU\left(IN^{i}_{RSU}\right)\) _has been executed at most once._  
**Definition 5**. : _(Semantic security): \(\mathcal{A}\) can only execute \(Test\left(IN^{i}_{VUI},IN^{i}_{RSU},IN^{i}_{TA},r\right)\) at most once and can make multiple additional queries to validate the accuracy of the return value from \(Test\left(IN^{i}_{VUI},IN^{i}_{RSU},IN^{i}_{TA},r\right)\). That is, \(\mathcal{A}\) guesses the random bit \(r\) generated by Test. The possibility is \(Adv^{A}_{P}=\left|2 Pr[suc(A)]-1\right|\), \(Adv^{A}_{P}<\eta\) denotes the protocol is secure, where \(\eta\) is sufficiently small._  
**Theorem 1**. : _The advantage of obtaining the session key in polynomial time by \(\mathcal{A}\) is \(Adv^{A}_{P}\leq\frac{q_{\text{H}}^{2}}{2^{\prime}\mu}+\frac{(q_{\text{S}}+q_{ \text{Q}})^{2}}{u}+\frac{q_{\text{S}}}{2^{\prime}\mu_{\text{Q}}-1}+2q_{\text{S }}Adv^{A}_{PUF}+2 Adv^{A}_{ECDLP}\). Where \(q_{\text{H}}\), \(q_{\text{S}}\) and \(q_{\text{E}}\) denote the numbers of executing Hash, Send and Execute, respectively. \(l_{\text{H}}\), \(n\), and \(l_{\text{bio}}\) are the length of hash, the number of transcripts, and the length of biological key, respectively. The advantage of breaking PUF and ECDLP by \(\mathcal{A}\) are \(Adv^{A}_{PUF}\) and \(Adv^{A}_{ECDLP}\), respectively._  
Proof.